@Test public void testNormal() { final ExprAction action = mock(ExprAction.class); doReturn(Eq(Prime(x.getRef()), Add(x.getRef(), Int(1)))).when(action).toExpr(); when(action.nextIndexing()).thenReturn(VarIndexing.all(1)); final Collection<? extends ExplState> succStates = transFunc.getSuccStates(state, action, prec); Assert.assertEquals(1, succStates.size()); Assert.assertEquals(ExplState.of(ImmutableValuation.builder().put(x, Int(2)).build()), succStates.iterator().next()); }
@Override public Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action, final ExplPrec prec) { checkNotNull(state); checkNotNull(action); checkNotNull(prec); final Collection<ExplState> succStates = ExprStates.createStatesForExpr(solver, BoolExprs.And(state.toExpr(), action.toExpr()), 0, prec::createState, action.nextIndexing()); return succStates.isEmpty() ? Collections.singleton(ExplState.bottom()) : succStates; }
ExplTransFunc implements TransFunc<ExplState, ExprAction, ExplPrec> { @Override public Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action, final ExplPrec prec) { checkNotNull(state); checkNotNull(action); checkNotNull(prec); final Collection<ExplState> succStates = ExprStates.createStatesForExpr(solver, BoolExprs.And(state.toExpr(), action.toExpr()), 0, prec::createState, action.nextIndexing()); return succStates.isEmpty() ? Collections.singleton(ExplState.bottom()) : succStates; } }
ExplTransFunc implements TransFunc<ExplState, ExprAction, ExplPrec> { @Override public Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action, final ExplPrec prec) { checkNotNull(state); checkNotNull(action); checkNotNull(prec); final Collection<ExplState> succStates = ExprStates.createStatesForExpr(solver, BoolExprs.And(state.toExpr(), action.toExpr()), 0, prec::createState, action.nextIndexing()); return succStates.isEmpty() ? Collections.singleton(ExplState.bottom()) : succStates; } private  ExplTransFunc(final Solver solver); }
ExplTransFunc implements TransFunc<ExplState, ExprAction, ExplPrec> { @Override public Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action, final ExplPrec prec) { checkNotNull(state); checkNotNull(action); checkNotNull(prec); final Collection<ExplState> succStates = ExprStates.createStatesForExpr(solver, BoolExprs.And(state.toExpr(), action.toExpr()), 0, prec::createState, action.nextIndexing()); return succStates.isEmpty() ? Collections.singleton(ExplState.bottom()) : succStates; } private  ExplTransFunc(final Solver solver); static ExplTransFunc create(final Solver solver); @Override Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action,
														 final ExplPrec prec); }
ExplTransFunc implements TransFunc<ExplState, ExprAction, ExplPrec> { @Override public Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action, final ExplPrec prec) { checkNotNull(state); checkNotNull(action); checkNotNull(prec); final Collection<ExplState> succStates = ExprStates.createStatesForExpr(solver, BoolExprs.And(state.toExpr(), action.toExpr()), 0, prec::createState, action.nextIndexing()); return succStates.isEmpty() ? Collections.singleton(ExplState.bottom()) : succStates; } private  ExplTransFunc(final Solver solver); static ExplTransFunc create(final Solver solver); @Override Collection<? extends ExplState> getSuccStates(final ExplState state, final ExprAction action,
														 final ExplPrec prec);  }