<NME> Tool.java <BEF> // Copyright (c) 2003 Compaq Corporation. All rights reserved. // Portions Copyright (c) 2003 Microsoft Corporation. All rights reserved. // Copyright (c) 2022, Oracle and/or its affiliates. // Last modified on Wed 12 Jul 2017 at 16:10:00 PST by ian morris nieves // modified on Thu 2 Aug 2007 at 10:25:48 PST by lamport // modified on Fri Jan 4 22:46:57 PST 2002 by yuanyu package tlc2.tool.impl; import java.io.File; import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.function.Supplier; import tla2sany.parser.SyntaxTreeNode; import tla2sany.semantic.APSubstInNode; import tla2sany.semantic.ExprNode; import tla2sany.semantic.ExprOrOpArgNode; import tla2sany.semantic.ExternalModuleTable; import tla2sany.semantic.FormalParamNode; import tla2sany.semantic.LabelNode; import tla2sany.semantic.LetInNode; import tla2sany.semantic.LevelConstants; import tla2sany.semantic.LevelNode; import tla2sany.semantic.OpApplNode; import tla2sany.semantic.OpArgNode; import tla2sany.semantic.OpDeclNode; import tla2sany.semantic.OpDefNode; import tla2sany.semantic.OpDefOrDeclNode; import tla2sany.semantic.SemanticNode; import tla2sany.semantic.Subst; import tla2sany.semantic.SubstInNode; import tla2sany.semantic.SymbolNode; import tla2sany.semantic.ThmOrAssumpDefNode; import tlc2.TLCGlobals; import tlc2.output.EC; import tlc2.output.MP; import tlc2.tool.Action; import tlc2.tool.BuiltInOPs; import tlc2.tool.EvalControl; import tlc2.tool.EvalException; import tlc2.tool.IActionItemList; import tlc2.tool.IContextEnumerator; import tlc2.tool.INextStateFunctor; import tlc2.tool.IStateFunctor; import tlc2.tool.ITool; import tlc2.tool.StateVec; import tlc2.tool.TLCState; import tlc2.tool.TLCStateFun; import tlc2.tool.TLCStateInfo; import tlc2.tool.TLCStateMut; import tlc2.tool.TLCStateMutExt; import tlc2.tool.ToolGlobals; import tlc2.tool.coverage.CostModel; import tlc2.util.Context; import tlc2.util.ExpectInlined; import tlc2.util.IdThread; import tlc2.util.RandomGenerator; import tlc2.util.Vect; import tlc2.value.IFcnLambdaValue; import tlc2.value.IMVPerm; import tlc2.value.IValue; import tlc2.value.ValueConstants; import tlc2.value.Values; import tlc2.value.impl.Applicable; import tlc2.value.impl.BoolValue; import tlc2.value.impl.Enumerable; import tlc2.value.impl.Enumerable.Ordering; import tlc2.value.impl.EvaluatingValue; import tlc2.value.impl.FcnLambdaValue; import tlc2.value.impl.FcnParams; import tlc2.value.impl.FcnRcdValue; import tlc2.value.impl.LazySupplierValue; import tlc2.value.impl.LazyValue; import tlc2.value.impl.MVPerm; import tlc2.value.impl.MVPerms; import tlc2.value.impl.MethodValue; import tlc2.value.impl.ModelValue; import tlc2.value.impl.OpLambdaValue; import tlc2.value.impl.OpValue; import tlc2.value.impl.RecordValue; import tlc2.value.impl.Reducible; import tlc2.value.impl.SetCapValue; import tlc2.value.impl.SetCupValue; import tlc2.value.impl.SetDiffValue; import tlc2.value.impl.SetEnumValue; import tlc2.value.impl.SetOfFcnsValue; import tlc2.value.impl.SetOfRcdsValue; import tlc2.value.impl.SetOfTuplesValue; import tlc2.value.impl.SetPredValue; import tlc2.value.impl.StringValue; import tlc2.value.impl.SubsetValue; import tlc2.value.impl.TupleValue; import tlc2.value.impl.UnionValue; import tlc2.value.impl.Value; import tlc2.value.impl.ValueEnumeration; import tlc2.value.impl.ValueExcept; import tlc2.value.impl.ValueVec; import util.Assert; import util.Assert.TLCRuntimeException; import util.FilenameToStream; import util.TLAConstants; import util.UniqueString; /** * This class provides useful methods for tools like model checker * and simulator. * * It's instance serves as a spec handle * This is one of two places in TLC, where not all messages are retrieved from the message printer, * but constructed just here in the code. */ public abstract class Tool extends Spec implements ValueConstants, ToolGlobals, ITool { public static final String PROBABLISTIC_KEY = Tool.class.getName() + ".probabilistic"; /* * Prototype, do *not* activate when checking safety or liveness!!!: * For simulation that is not meant as a substitute of exhaustive checking for too * large models, it can be useful to generate behaviors as quickly as possible, * i.e. without checking all successor states along the states of the behavior. * This flag activates the code path that efficiently generate only a single * successor state during simulation. It does not let the user parameterize * the code with a particular distribution, but instead draws from the uniform * distribution. * * In its current form, it only handles non-determinism expressed with opcode * OPCODE_be (bounded exist), i.e. (which simply happened to be the primary * expression that we encountered in the SWIM spec during this work): * * VARIABLE x * \E n \in S: x' = n * * Activate with: -Dtlc2.tool.impl.Tool.probabilistic=true */ private static final boolean PROBABLISTIC = Boolean.getBoolean(PROBABLISTIC_KEY); public enum Mode { Simulation, MC, MC_DEBUG, Executor; } public static final Value[] EmptyArgs = new Value[0]; protected final Action[] actions; // the list of TLA actions. private Vect<Action> actionVec = new Vect<>(10); protected final Mode toolMode; /** * Creates a new tool handle */ public Tool(String specFile, String configFile) { this(new File(specFile), specFile, configFile, null); } public Tool(String specFile, String configFile, FilenameToStream resolver) { this(new File(specFile), specFile, configFile, resolver); } public Tool(String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params) { this(new File(specFile), specFile, configFile, resolver, params); } public Tool(String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params) { this(new File(specFile), specFile, configFile, resolver, mode, params); } private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver) { this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, new HashMap<>()); } private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params) { this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, params); } private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params) { this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, mode, params); } public Tool(String specDir, String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params) { this(specDir, specFile, configFile, resolver, Mode.MC, params); } public Tool(String specDir, String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params) { super(specDir, specFile, configFile, resolver, mode, params); this.toolMode = mode; // set variables to the static filed in the state if (mode == Mode.Simulation || mode == Mode.Executor || mode == Mode.MC_DEBUG) { assert TLCState.Empty instanceof TLCStateMutExt; TLCStateMutExt.setTool(this); } else { // Initialize state. assert TLCState.Empty instanceof TLCStateMut; TLCStateMut.setTool(this); } Action next = this.getNextStateSpec(); if (next == null) { this.actions = new Action[0]; } else { this.getActions(next); int sz = this.actionVec.size(); this.actions = new Action[sz]; for (int i = 0; i < sz; i++) { this.actions[i] = (Action) this.actionVec.elementAt(i); } } // Tag the initial predicates and next-state actions. final Vect<Action> initAndNext = getInitStateSpec().concat(actionVec); for (int i = 0; i < initAndNext.size(); i++) { initAndNext.elementAt(i).setId(i); } } Tool(Tool other) { super(other); this.actions = other.actions; this.actionVec = other.actionVec; this.toolMode = other.toolMode; } @Override public Mode getMode() { return this.toolMode; } /** * This method returns the set of all possible actions of the * spec, and sets the actions field of this object. In fact, we * could simply treat the next predicate as one "giant" action. * But for efficiency, we preprocess the next state predicate by * splitting it into a set of actions for the maximum prefix * of disjunction and existential quantification. */ @Override public final Action[] getActions() { return this.actions; } private final void getActions(final Action next) { this.getActions(next.pred, next.con, next.getOpDef(), next.cm); } private final void getActions(SemanticNode next, Context con, final OpDefNode opDefNode, CostModel cm) { switch (next.getKind()) { case OpApplKind: { OpApplNode next1 = (OpApplNode)next; this.getActionsAppl(next1, con, opDefNode, cm); return; } case LetInKind: { LetInNode next1 = (LetInNode)next; this.getActions(next1.getBody(), con, opDefNode, cm); return; } case SubstInKind: { SubstInNode next1 = (SubstInNode)next; Subst[] substs = next1.getSubsts(); if (substs.length == 0) { this.getActions(next1.getBody(), con, opDefNode, cm); } else { Action action = new Action(next1, con, opDefNode); this.actionVec.addElement(action); } return; } // Added by LL on 13 Nov 2009 to handle theorem and assumption names. case APSubstInKind: { APSubstInNode next1 = (APSubstInNode)next; Subst[] substs = next1.getSubsts(); if (substs.length == 0) { this.getActions(next1.getBody(), con, opDefNode, cm); } else { Action action = new Action(next1, con, opDefNode); this.actionVec.addElement(action); } return; } /*********************************************************************** * LabelKind class added by LL on 13 Jun 2007. * ***********************************************************************/ case LabelKind: { LabelNode next1 = (LabelNode)next; this.getActions(next1.getBody(), con, opDefNode, cm); return; } default: { Assert.fail("The next state relation is not a boolean expression.\n" + next, next, con); } } } private final void getActionsAppl(OpApplNode next, Context con, final OpDefNode actionName, CostModel cm) { ExprOrOpArgNode[] args = next.getArgs(); SymbolNode opNode = next.getOperator(); int opcode = BuiltInOPs.getOpCode(opNode.getName()); if (opcode == 0) { Object val = this.lookup(opNode, con, false); if (val instanceof OpDefNode) { OpDefNode opDef = (OpDefNode)val; opcode = BuiltInOPs.getOpCode(opDef.getName()); if (opcode == 0) { try { FormalParamNode[] formals = opDef.getParams(); int alen = args.length; int argLevel = 0; for (int i = 0; i < alen; i++) { argLevel = args[i].getLevel(); if (argLevel != 0) break; } if (argLevel == 0) { Context con1 = con; for (int i = 0; i < alen; i++) { IValue aval = this.eval(args[i], con, TLCState.Empty, cm); con1 = con1.cons(formals[i], aval); } this.getActions(opDef.getBody(), con1, opDef, cm); return; } } catch (Throwable e) { /*SKIP*/ } } } if (opcode == 0) { Action action = new Action(next, con, (OpDefNode) opNode); this.actionVec.addElement(action); return; } } switch (opcode) { case OPCODE_be: // BoundedExists { final int cnt = this.actionVec.size(); try { ContextEnumerator Enum = this.contexts(next, con, TLCState.Empty, TLCState.Empty, EvalControl.Clear, cm); if (Enum.isDone()) { // No exception and no actions created implies Enum was empty: // \E i \in {} : ... // \E i \in Nat: FALSE // ... this.actionVec.addElement(new Action(next, con, actionName)); return; } Context econ; while ((econ = Enum.nextElement()) != null) { this.getActions(args[0], econ, actionName, cm); } assert (cnt < this.actionVec.size()) : "AssertionError when creating Actions. This case should have been handled by Enum.isDone conditional above!"; } catch (Throwable e) { Action action = new Action(next, con, actionName); this.actionVec.removeAll(cnt); this.actionVec.addElement(action); } return; } case OPCODE_dl: // DisjList case OPCODE_lor: { for (int i = 0; i < args.length; i++) { this.getActions(args[i], con, actionName, cm); } return; } default: { // We handle all the other builtin operators here. Action action = new Action(next, con, actionName); this.actionVec.addElement(action); return; } } } /* * This method returns the set of possible initial states that * satisfies the initial state predicate. Initial state predicate * can be under-specified. Too many possible initial states will * probably make tools like TLC useless. */ @Override public final StateVec getInitStates() { final StateVec initStates = new StateVec(0); getInitStates(initStates); return initStates; } @Override public final void getInitStates(IStateFunctor functor) { Vect<Action> init = this.getInitStateSpec(); ActionItemList acts = ActionItemListExt.Empty; // MAK 09/11/2018: Tail to head iteration order cause the first elem added with // acts.cons to be acts tail. This fixes the bug/funny behavior that the init // predicate Init == A /\ B /\ C /\ D was evaluated in the order A, D, C, B (A // doesn't get added to acts at all). for (int i = (init.size() - 1); i > 0; i--) { Action elem = (Action)init.elementAt(i); acts = (ActionItemList) acts.cons(elem, IActionItemList.PRED); } if (init.size() != 0) { Action elem = (Action)init.elementAt(0); TLCState ps = TLCState.Empty.createEmpty(); if (acts.isEmpty()) { acts.setAction(elem); } this.getInitStates(elem.pred, acts, elem.con, ps, functor, elem.cm); } } /* Create the state specified by pred. */ @Override public final TLCState makeState(SemanticNode pred) { ActionItemList acts = ActionItemList.Empty; TLCState ps = TLCState.Empty.createEmpty(); StateVec states = new StateVec(0); this.getInitStates(pred, acts, Context.Empty, ps, states, acts.cm); if (states.size() != 1) { Assert.fail("The predicate does not specify a unique state." + pred, pred); } TLCState state = states.elementAt(0); if (!this.isGoodState(state)) { Assert.fail("The state specified by the predicate is not complete." + pred, pred); } return state; } protected void getInitStates(SemanticNode init, ActionItemList acts, Context c, TLCState ps, IStateFunctor states, CostModel cm) { switch (init.getKind()) { case OpApplKind: { OpApplNode init1 = (OpApplNode)init; this.getInitStatesAppl(init1, acts, c, ps, states, cm); return; } case LetInKind: { LetInNode init1 = (LetInNode)init; this.getInitStates(init1.getBody(), acts, c, ps, states, cm); return; } case SubstInKind: { SubstInNode init1 = (SubstInNode)init; Subst[] subs = init1.getSubsts(); Context c1 = c; for (int i = 0; i < subs.length; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, coverage ? sub.getCM() : cm, toolId)); } this.getInitStates(init1.getBody(), acts, c1, ps, states, cm); return; } // Added by LL on 13 Nov 2009 to handle theorem and assumption names. case APSubstInKind: { APSubstInNode init1 = (APSubstInNode)init; Subst[] subs = init1.getSubsts(); Context c1 = c; for (int i = 0; i < subs.length; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, cm, toolId)); } this.getInitStates(init1.getBody(), acts, c1, ps, states, cm); return; } // LabelKind class added by LL on 13 Jun 2007 case LabelKind: { LabelNode init1 = (LabelNode)init; this.getInitStates(init1.getBody(), acts, c, ps, states, cm); return; } default: { Assert.fail("The init state relation is not a boolean expression.\n" + init, init, c); } } } protected void getInitStates(ActionItemList acts, TLCState ps, IStateFunctor states, CostModel cm) { if (acts.isEmpty()) { if (coverage) { cm.incInvocations(); cm.getRoot().incInvocations(); } states.addElement(ps.copy().setAction(acts.getAction())); return; } else if (ps.allAssigned()) { // MAK 05/25/2018: If all values of the initial state have already been // assigned, there is no point in further trying to assign values. Instead, all // remaining statements (ActionItemList) can just be evaluated for their boolean // value. // This optimization is especially useful to check inductive invariants which // require TLC to generate a very large set of initial states. while (!acts.isEmpty()) { final Value bval = this.eval(acts.carPred(), acts.carContext(), ps, TLCState.Empty, EvalControl.Init, acts.cm); if (!(bval instanceof BoolValue)) { //TODO Choose more fitting error message. Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "initial states", "boolean", bval.toString(), acts.pred.toString() }, acts.carPred(), acts.carContext()); } if (!((BoolValue) bval).val) { if (coverage) { // Increase "states found". cm.getRoot().incSecondary(); } return; } // Move on to the next action in the ActionItemList. acts = acts.cdr(); } if (coverage) { cm.incInvocations(); cm.getRoot().incInvocations(); } states.addElement(ps.copy().setAction(acts.getAction())); return; } // Assert.check(act.kind > 0 || act.kind == -1); ActionItemList acts1 = acts.cdr(); this.getInitStates(acts.carPred(), acts1, acts.carContext(), ps, states, acts.cm); } protected void getInitStatesAppl(OpApplNode init, ActionItemList acts, Context c, TLCState ps, IStateFunctor states, CostModel cm) { if (coverage) {cm = cm.get(init);} ExprOrOpArgNode[] args = init.getArgs(); int alen = args.length; SymbolNode opNode = init.getOperator(); int opcode = BuiltInOPs.getOpCode(opNode.getName()); if (opcode == 0) { // This is a user-defined operator with one exception: it may // be substed by a builtin operator. This special case occurs // when the lookup returns an OpDef with opcode # 0. Object val = this.lookup(opNode, c, ps, false); if (val instanceof OpDefNode) { OpDefNode opDef = (OpDefNode)val; opcode = BuiltInOPs.getOpCode(opDef.getName()); if (opcode == 0) { // Context c1 = this.getOpContext(opDef, args, c, false); Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId); this.getInitStates(opDef.getBody(), acts, c1, ps, states, cm); return; } } // Added 13 Nov 2009 by LL to fix Yuan's fix. /********************************************************************* * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode * * imported with parameterized instantiation. * *********************************************************************/ if (val instanceof ThmOrAssumpDefNode) { ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode)val; opcode = BuiltInOPs.getOpCode(opDef.getName()); Context c1 = this.getOpContext(opDef, args, c, true); this.getInitStates(opDef.getBody(), acts, c1, ps, states, cm); return; } if (val instanceof LazyValue) { LazyValue lv = (LazyValue)val; if (lv.getValue() == null || lv.isUncachable()) { this.getInitStates(lv.expr, acts, lv.con, ps, states, cm); return; } val = lv.getValue(); } Object bval = val; if (alen == 0) { if (val instanceof MethodValue) { bval = ((MethodValue)val).apply(EmptyArgs, EvalControl.Init); } else if (val instanceof EvaluatingValue) { // Allow EvaluatingValue overwrites to have zero arity. bval = ((EvaluatingValue) val).eval(this, args, c, ps, TLCState.Empty, EvalControl.Init, cm); } } else { if (val instanceof OpValue) { bval = ((OpValue) val).eval(this, args, c, ps, TLCState.Empty, EvalControl.Init, cm); } } if (opcode == 0) { if (!(bval instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "initial states", "boolean", bval.toString(), init.toString() }, init, c); } if (((BoolValue) bval).val) { this.getInitStates(acts, ps, states, cm); } return; } } switch (opcode) { case OPCODE_dl: // DisjList case OPCODE_lor: { for (int i = 0; i < alen; i++) { this.getInitStates(args[i], acts, c, ps, states, cm); } return; } case OPCODE_cl: // ConjList case OPCODE_land: { for (int i = alen-1; i > 0; i--) { acts = (ActionItemList) acts.cons(args[i], c, cm, i); } this.getInitStates(args[0], acts, c, ps, states, cm); return; } case OPCODE_be: // BoundedExists { SemanticNode body = args[0]; ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init, cm); Context c1; while ((c1 = Enum.nextElement()) != null) { this.getInitStates(body, acts, c1, ps, states, cm); } return; } case OPCODE_bf: // BoundedForall { SemanticNode body = args[0]; ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init, cm); Context c1 = Enum.nextElement(); if (c1 == null) { this.getInitStates(acts, ps, states, cm); } else { ActionItemList acts1 = acts; Context c2; while ((c2 = Enum.nextElement()) != null) { acts1 = (ActionItemList) acts1.cons(body, c2, cm, IActionItemList.PRED); } this.getInitStates(body, acts1, c1, ps, states, cm); } return; } case OPCODE_ite: // IfThenElse { Value guard = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm); if (!(guard instanceof BoolValue)) { Assert.fail("In computing initial states, a non-boolean expression (" + guard.getKindString() + ") was used as the condition " + "of an IF.\n" + init, init, c); } int idx = (((BoolValue)guard).val) ? 1 : 2; this.getInitStates(args[idx], acts, c, ps, states, cm); return; } case OPCODE_case: // Case { SemanticNode other = null; for (int i = 0; i < alen; i++) { OpApplNode pair = (OpApplNode)args[i]; ExprOrOpArgNode[] pairArgs = pair.getArgs(); if (pairArgs[0] == null) { other = pairArgs[1]; } else { Value bval = this.eval(pairArgs[0], c, ps, TLCState.Empty, EvalControl.Init, cm); if (!(bval instanceof BoolValue)) { Assert.fail("In computing initial states, a non-boolean expression (" + bval.getKindString() + ") was used as a guard condition" + " of a CASE.\n" + pairArgs[1], pairArgs[1], c); } if (((BoolValue)bval).val) { this.getInitStates(pairArgs[1], acts, c, ps, states, cm); return; } } } if (other == null) { Assert.fail("In computing initial states, TLC encountered a CASE with no" + " conditions true.\n" + init, init, c); } this.getInitStates(other, acts, c, ps, states, cm); return; } case OPCODE_fa: // FcnApply { Value fval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm); if (fval instanceof FcnLambdaValue) { FcnLambdaValue fcn = (FcnLambdaValue)fval; if (fcn.fcnRcd == null) { Context c1 = this.getFcnContext(fcn, args, c, ps, TLCState.Empty, EvalControl.Init, cm); this.getInitStates(fcn.body, acts, c1, ps, states, cm); return; } fval = fcn.fcnRcd; } else if (!(fval instanceof Applicable)) { Assert.fail("In computing initial states, a non-function (" + fval.getKindString() + ") was applied as a function.\n" + init, init, c); } Applicable fcn = (Applicable) fval; Value argVal = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm); Value bval = fcn.apply(argVal, EvalControl.Init); if (!(bval instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "initial states", "boolean", init.toString() }, args[1], c); } if (((BoolValue)bval).val) { this.getInitStates(acts, ps, states, cm); } return; } case OPCODE_eq: { SymbolNode var = this.getVar(args[0], c, false, toolId); if (var == null || var.getName().getVarLoc() < 0) { Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm); if (!((BoolValue)bval).val) { return; } } else { UniqueString varName = var.getName(); IValue lval = ps.lookup(varName); Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm); if (lval == null) { ps = ps.bind(varName, rval); this.getInitStates(acts, ps, states, cm); ps.unbind(varName); return; } else { if (!lval.equals(rval)) { return; } } } this.getInitStates(acts, ps, states, cm); return; } case OPCODE_in: { SymbolNode var = this.getVar(args[0], c, false, toolId); if (var == null || var.getName().getVarLoc() < 0) { Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm); if (!((BoolValue)bval).val) { return; } } else { UniqueString varName = var.getName(); Value lval = (Value) ps.lookup(varName); Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm); if (lval == null) { if (!(rval instanceof Enumerable)) { Assert.fail("In computing initial states, the right side of \\IN" + " is not enumerable.\n" + init, init, c); } ValueEnumeration Enum = ((Enumerable)rval).elements(); Value elem; while ((elem = Enum.nextElement()) != null) { ps.bind(varName, elem); this.getInitStates(acts, ps, states, cm); ps.unbind(varName); } return; } else { if (!rval.member(lval)) { return; } } } this.getInitStates(acts, ps, states, cm); return; } case OPCODE_implies: { Value lval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm); if (!(lval instanceof BoolValue)) { Assert.fail("In computing initial states of a predicate of form" + " P => Q, P was " + lval.getKindString() + "\n." + init, init, c); } if (((BoolValue)lval).val) { this.getInitStates(args[1], acts, c, ps, states, cm); } @Override public final boolean getNextStates(final INextStateFunctor functor, final TLCState state) { for (int i = 0; i < actions.length; i++) { final Action action = actions[i]; this.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state, TLCState.Empty.createEmpty(), case OPCODE_nop: { this.getInitStates(args[0], acts, c, ps, states, cm); return; } default: { // For all the other builtin operators, simply evaluate: Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm); if (!(bval instanceof BoolValue)) { Assert.fail("In computing initial states, TLC expected a boolean expression," + "\nbut instead found " + bval + ".\n" + init, init, c); } if (((BoolValue)bval).val) { this.getInitStates(acts, ps, states, cm); } return; } } } /** * This method returns the set of next states when taking the action * in the given state. */ @Override public final StateVec getNextStates(Action action, TLCState state) { return getNextStates(action, action.con, state); } public final StateVec getNextStates(final Action action, final Context ctx, final TLCState state) { ActionItemList acts = ActionItemList.Empty; TLCState s1 = TLCState.Empty.createEmpty(); StateVec nss = new StateVec(0); this.getNextStates(action, action.pred, acts, ctx, state, s1.setPredecessor(state).setAction(action), nss, action.cm); if (coverage) { action.cm.incInvocations(nss.size()); } if (PROBABLISTIC && nss.size() > 1) {System.err.println("Simulator generated more than one next state");} return nss; } @Override public boolean getNextStates(final INextStateFunctor functor, final TLCState state) { for (int i = 0; i < actions.length; i++) { this.getNextStates(functor, state, actions[i]); } return false; } public boolean getNextStates(final INextStateFunctor functor, final TLCState state, final Action action) { this.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state, TLCState.Empty.createEmpty().setPredecessor(state).setAction(action), functor, action.cm); return false; } protected abstract TLCState getNextStates(final Action action, SemanticNode pred, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm); protected final TLCState getNextStatesImpl(final Action action, SemanticNode pred, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm) { switch (pred.getKind()) { case OpApplKind: { OpApplNode pred1 = (OpApplNode)pred; if (coverage) {cm = cm.get(pred);} return this.getNextStatesAppl(action, pred1, acts, c, s0, s1, nss, cm); } case LetInKind: { LetInNode pred1 = (LetInNode)pred; return this.getNextStates(action, pred1.getBody(), acts, c, s0, s1, nss, cm); } case SubstInKind: { return getNextStatesImplSubstInKind(action, (SubstInNode) pred, acts, c, s0, s1, nss, cm); } // Added by LL on 13 Nov 2009 to handle theorem and assumption names. case APSubstInKind: { return getNextStatesImplApSubstInKind(action, (APSubstInNode) pred, acts, c, s0, s1, nss, cm); } // LabelKind class added by LL on 13 Jun 2007 case LabelKind: { LabelNode pred1 = (LabelNode)pred; return this.getNextStates(action, pred1.getBody(), acts, c, s0, s1, nss, cm); } default: { Assert.fail("The next state relation is not a boolean expression.\n" + pred, pred, c); } } return s1; } @ExpectInlined private final TLCState getNextStatesImplSubstInKind(final Action action, SubstInNode pred1, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm) { Subst[] subs = pred1.getSubsts(); int slen = subs.length; Context c1 = c; for (int i = 0; i < slen; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, coverage ? sub.getCM() : cm, toolId)); } return this.getNextStates(action, pred1.getBody(), acts, c1, s0, s1, nss, cm); } @ExpectInlined private final TLCState getNextStatesImplApSubstInKind(final Action action, APSubstInNode pred1, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm) { Subst[] subs = pred1.getSubsts(); int slen = subs.length; Context c1 = c; for (int i = 0; i < slen; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, cm, toolId)); } return this.getNextStates(action, pred1.getBody(), acts, c1, s0, s1, nss, cm); } @ExpectInlined private final TLCState getNextStates(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1, final INextStateFunctor nss, CostModel cm) { final TLCState copy = getNextStates0(action, acts, s0, s1, nss, cm); if (coverage && copy != s1) { cm.incInvocations(); } return copy; } @ExpectInlined private final TLCState getNextStates0(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1, final INextStateFunctor nss, CostModel cm) { if (acts.isEmpty()) { nss.addElement(s0, action, s1); return s1.copy(); } else if (TLCGlobals.warn && s1.allAssigned()) { // If all variables have been assigned and warnings are turned off, Tool can // execute the fast-path that avoids generating known successor states, but // doesn't trigger a warning in cases like: // ---- MODULE F ---- // VARIABLES x // Init == x = 0 // Next == x' = 42 /\ UNCHANGED x \* UNCHANGED and changed! // ==== // => "Warning: The variable x was changed while it is specified as UNCHANGED" return getNextStatesAllAssigned(action, acts, s0, s1, nss, cm); } final int kind = acts.carKind(); SemanticNode pred = acts.carPred(); Context c = acts.carContext(); ActionItemList acts1 = acts.cdr(); cm = acts.cm; if (kind > 0) { return this.getNextStates(action, pred, acts1, c, s0, s1, nss, cm); } else if (kind == -1) { return this.getNextStates(action, pred, acts1, c, s0, s1, nss, cm); } else if (kind == -2) { return this.processUnchanged(action, pred, acts1, c, s0, s1, nss, cm); } else { IValue v1 = this.eval(pred, c, s0, cm); IValue v2 = this.eval(pred, c, s1, cm); if (!v1.equals(v2)) { if (coverage) { return this.getNextStates(action, acts1, s0, s1, nss, cm); } else { return this.getNextStates0(action, acts1, s0, s1, nss, cm); } } } return s1; } private final TLCState getNextStatesAllAssigned(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) { int kind = acts.carKind(); SemanticNode pred = acts.carPred(); Context c = acts.carContext(); CostModel cm2 = acts.cm; while (!acts.isEmpty()) { if (kind > 0 || kind == -1) { final Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm2); if (!(bval instanceof BoolValue)) { // TODO Choose more fitting error message. Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "next states", "boolean", bval.toString(), acts.pred.toString() }, pred, c); } if (!((BoolValue) bval).val) { return s1; } } else if (kind == -2) { // Identical to default handling below (line 876). Ignored during this optimization. return this.processUnchanged(action, pred, acts.cdr(), c, s0, s1, nss, cm2); } else { final IValue v1 = this.eval(pred, c, s0, cm2); final IValue v2 = this.eval(pred, c, s1, cm2); if (v1.equals(v2)) { return s1; } } // Move on to the next action in the ActionItemList. acts = acts.cdr(); pred = acts.carPred(); c = acts.carContext(); kind = acts.carKind(); cm2 = acts.cm; } nss.addElement(s0, action, s1); return s1.copy(); } /* getNextStatesAppl */ @ExpectInlined protected abstract TLCState getNextStatesAppl(final Action action, OpApplNode pred, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm); protected final TLCState getNextStatesApplImpl(final Action action, final OpApplNode pred, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) { final ExprOrOpArgNode[] args = pred.getArgs(); final int alen = args.length; final SymbolNode opNode = pred.getOperator(); int opcode = BuiltInOPs.getOpCode(opNode.getName()); if (opcode == 0) { // This is a user-defined operator with one exception: it may // be substed by a builtin operator. This special case occurs // when the lookup returns an OpDef with opcode # 0. Object val = this.lookup(opNode, c, s0, false); if (val instanceof OpDefNode) { final OpDefNode opDef = (OpDefNode) val; opcode = BuiltInOPs.getOpCode(opDef.getName()); if (opcode == 0) { return this.getNextStates(action, opDef.getBody(), acts, this.getOpContext(opDef, args, c, true, cm, toolId), s0, s1, nss, cm); } } // Added by LL 13 Nov 2009 to fix Yuan's fix /********************************************************************* * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode * * imported with parameterized instantiation. * *********************************************************************/ if (val instanceof ThmOrAssumpDefNode) { final ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode)val; return this.getNextStates(action, opDef.getBody(), acts, this.getOpContext(opDef, args, c, true), s0, s1, nss, cm); } if (val instanceof LazyValue) { final LazyValue lv = (LazyValue)val; if (lv.getValue() == null || lv.isUncachable()) { return this.getNextStates(action, lv.expr, acts, lv.con, s0, s1, nss, lv.cm); } val = lv.getValue(); } //TODO If all eval/apply in getNextStatesApplEvalAppl would be side-effect free (ie. not mutate args, c, s0,...), // this call could be moved into the if(opcode==0) branch below. However, opcode!=0 will only be the case if // OpDefNode above has been substed with a built-in operator. In other words, a user defines an operator Op1, // and re-defines Op1 with a TLA+ built-in one in a TLC model (not assumed to be common). => No point in trying // to move this call into if(opcode==0) because this will be the case most of the time anyway. final Object bval = getNextStatesApplEvalAppl(alen, args, c, s0, s1, cm, val); // opcode == 0 is a user-defined operator. if (opcode == 0) { return getNextStatesApplUsrDefOp(action, pred, acts, s0, s1, nss, cm, bval); } } return getNextStatesApplSwitch(action, pred, acts, c, s0, s1, nss, cm, args, alen, opcode); } private final Object getNextStatesApplEvalAppl(final int alen, final ExprOrOpArgNode[] args, final Context c, final TLCState s0, final TLCState s1, final CostModel cm, final Object val) { if (alen == 0) { if (val instanceof MethodValue) { return ((MethodValue)val).apply(EmptyArgs, EvalControl.Clear); } else if (val instanceof EvaluatingValue) { return ((EvaluatingValue)val).eval(this, args, c, s0, s1, EvalControl.Clear, cm); } } else { if (val instanceof OpValue) { // EvaluatingValue sub-class of OpValue! return ((OpValue) val).eval(this, args, c, s0, s1, EvalControl.Clear, cm); } } return val; } private final TLCState getNextStatesApplUsrDefOp(final Action action, final OpApplNode pred, final ActionItemList acts, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm, final Object bval) { if (!(bval instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "next states", "boolean", bval.toString(), pred.toString() }, pred); } if (((BoolValue) bval).val) { if (coverage) { return this.getNextStates(action, acts, s0, s1, nss, cm); } else { return this.getNextStates0(action, acts, s0, s1, nss, cm); } } return s1; } private final TLCState getNextStatesApplSwitch(final Action action, final OpApplNode pred, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm, final ExprOrOpArgNode[] args, final int alen, final int opcode) { TLCState resState = s1; switch (opcode) { case OPCODE_cl: // ConjList case OPCODE_land: { ActionItemList acts1 = acts; for (int i = alen - 1; i > 0; i--) { acts1 = (ActionItemList) acts1.cons(args[i], c, cm, i); } return this.getNextStates(action, args[0], acts1, c, s0, s1, nss, cm); } case OPCODE_dl: // DisjList case OPCODE_lor: { if (PROBABLISTIC) { // probabilistic (return after a state has been generated, ordered is randomized) final RandomGenerator rng = TLCGlobals.simulator.getRNG(); int index = (int) Math.floor(rng.nextDouble() * alen); final int p = rng.nextPrime(); for (int i = 0; i < alen; i++) { resState = this.getNextStates(action, args[index], acts, c, s0, resState, nss, cm); if (nss.hasStates()) { return resState; } index = (index + p) % alen; } } else { for (int i = 0; i < alen; i++) { resState = this.getNextStates(action, args[i], acts, c, s0, resState, nss, cm); } } return resState; } case OPCODE_be: // BoundedExists { SemanticNode body = args[0]; if (PROBABLISTIC) { // probabilistic (return after a state has been generated, ordered is randomized) final ContextEnumerator Enum = this.contexts(Ordering.RANDOMIZED, pred, c, s0, s1, EvalControl.Clear, cm); Context c1; while ((c1 = Enum.nextElement()) != null) { resState = this.getNextStates(action, body, acts, c1, s0, resState, nss, cm); if (nss.hasStates()) { return resState; } } } else { // non-deterministically generate successor states (potentially many) ContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Clear, cm); Context c1; while ((c1 = Enum.nextElement()) != null) { resState = this.getNextStates(action, body, acts, c1, s0, resState, nss, cm); } } return resState; } case OPCODE_bf: // BoundedForall { SemanticNode body = args[0]; ContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Clear, cm); Context c1 = Enum.nextElement(); if (c1 == null) { resState = this.getNextStates(action, acts, s0, s1, nss, cm); } else { ActionItemList acts1 = acts; Context c2; while ((c2 = Enum.nextElement()) != null) { acts1 = (ActionItemList) acts1.cons(body, c2, cm, IActionItemList.PRED); } resState = this.getNextStates(action, body, acts1, c1, s0, s1, nss, cm); } return resState; } case OPCODE_fa: // FcnApply { Value fval = this.eval(args[0], c, s0, s1, EvalControl.KeepLazy, cm); if (fval instanceof FcnLambdaValue) { FcnLambdaValue fcn = (FcnLambdaValue)fval; if (fcn.fcnRcd == null) { Context c1 = this.getFcnContext(fcn, args, c, s0, s1, EvalControl.Clear, cm); return this.getNextStates(action, fcn.body, acts, c1, s0, s1, nss, fcn.cm); } fval = fcn.fcnRcd; } if (!(fval instanceof Applicable)) { Assert.fail("In computing next states, a non-function (" + fval.getKindString() + ") was applied as a function.\n" + pred, pred, c); } Applicable fcn = (Applicable)fval; Value argVal = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm); Value bval = fcn.apply(argVal, EvalControl.Clear); if (!(bval instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "next states", "boolean", pred.toString() }, args[1], c); } if (((BoolValue)bval).val) { return this.getNextStates(action, acts, s0, s1, nss, cm); } return resState; } case OPCODE_aa: // AngleAct <A>_e { ActionItemList acts1 = (ActionItemList) acts.cons(args[1], c, cm, IActionItemList.CHANGED); return this.getNextStates(action, args[0], acts1, c, s0, s1, nss, cm); } case OPCODE_sa: // [A]_e { /* The following two lines of code did not work, and were changed by * YuanYu to mimic the way \/ works. Change made * 11 Mar 2009, with LL sitting next to him. */ // this.getNextStates(action, args[0], acts, c, s0, s1, nss); // return this.processUnchanged(args[1], acts, c, s0, s1, nss); resState = this.getNextStates(action, args[0], acts, c, s0, resState, nss, cm); return this.processUnchanged(action, args[1], acts, c, s0, resState, nss, cm); } case OPCODE_ite: // IfThenElse { Value guard = this.eval(args[0], c, s0, s1, EvalControl.Clear, cm); if (!(guard instanceof BoolValue)) { Assert.fail("In computing next states, a non-boolean expression (" + guard.getKindString() + ") was used as the condition of" + " an IF." + pred, pred, c); } if (((BoolValue)guard).val) { return this.getNextStates(action, args[1], acts, c, s0, s1, nss, cm); } else { return this.getNextStates(action, args[2], acts, c, s0, s1, nss, cm); } } case OPCODE_case: // Case { SemanticNode other = null; if (PROBABLISTIC) { // See Bounded exists above! throw new UnsupportedOperationException( "Probabilistic evaluation of next-state relation not implemented for CASE yet."); } for (int i = 0; i < alen; i++) { OpApplNode pair = (OpApplNode)args[i]; ExprOrOpArgNode[] pairArgs = pair.getArgs(); if (pairArgs[0] == null) { other = pairArgs[1]; } else { Value bval = this.eval(pairArgs[0], c, s0, s1, EvalControl.Clear, coverage ? cm.get(args[i]) : cm); if (!(bval instanceof BoolValue)) { Assert.fail("In computing next states, a non-boolean expression (" + bval.getKindString() + ") was used as a guard condition" + " of a CASE.\n" + pairArgs[1], pairArgs[1], c); } if (((BoolValue)bval).val) { return this.getNextStates(action, pairArgs[1], acts, c, s0, s1, nss, coverage ? cm.get(args[i]) : cm); } } } if (other == null) { Assert.fail("In computing next states, TLC encountered a CASE with no" + " conditions true.\n" + pred, pred, c); } return this.getNextStates(action, other, acts, c, s0, s1, nss, coverage ? cm.get(args[alen - 1]) : cm); } case OPCODE_eq: { SymbolNode var = this.getPrimedVar(args[0], c, false); // Assert.check(var.getName().getVarLoc() >= 0); if (var == null) { Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm); if (!((BoolValue)bval).val) { return resState; } } else { UniqueString varName = var.getName(); IValue lval = s1.lookup(varName); Value rval = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm); if (lval == null) { resState.bind(varName, rval); resState = this.getNextStates(action, acts, s0, resState, nss, cm); resState.unbind(varName); return resState; } else if (!lval.equals(rval)) { return resState; } } return this.getNextStates(action, acts, s0, s1, nss, cm); } case OPCODE_in: { SymbolNode var = this.getPrimedVar(args[0], c, false); // Assert.check(var.getName().getVarLoc() >= 0); if (var == null) { Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm); if (!((BoolValue)bval).val) { return resState; } } else { UniqueString varName = var.getName(); Value lval = (Value) s1.lookup(varName); Value rval = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm); if (lval == null) { if (!(rval instanceof Enumerable)) { Assert.fail("In computing next states, the right side of \\IN" + " is not enumerable.\n" + pred, pred, c); } if (PROBABLISTIC) { final ValueEnumeration Enum = ((Enumerable)rval).elements(Ordering.RANDOMIZED); Value elem; while ((elem = Enum.nextElement()) != null) { resState.bind(varName, elem); resState = this.getNextStates(action, acts, s0, resState, nss, cm); resState.unbind(varName); if (nss.hasStates()) { return resState; } } } ValueEnumeration Enum = ((Enumerable)rval).elements(); Value elem; while ((elem = Enum.nextElement()) != null) { resState.bind(varName, elem); resState = this.getNextStates(action, acts, s0, resState, nss, cm); resState.unbind(varName); } return resState; } else if (!rval.member(lval)) { return resState; } } return this.getNextStates(action, acts, s0, s1, nss, cm); } case OPCODE_implies: { Value bval = this.eval(args[0], c, s0, s1, EvalControl.Clear, cm); if (!(bval instanceof BoolValue)) { Assert.fail("In computing next states of a predicate of the form" + " P => Q, P was\n" + bval.getKindString() + ".\n" + pred, pred, c); } if (((BoolValue)bval).val) { return this.getNextStates(action, args[1], acts, c, s0, s1, nss, cm); } else { return this.getNextStates(action, acts, s0, s1, nss, cm); } } case OPCODE_unchanged: { return this.processUnchanged(action, args[0], acts, c, s0, s1, nss, cm); } case OPCODE_cdot: { Assert.fail("The current version of TLC does not support action composition.", pred, c); /*** TLCState s01 = TLCStateFun.Empty; StateVec iss = new StateVec(0); this.getNextStates(action, args[0], ActionItemList.Empty, c, s0, s01, iss); int sz = iss.size(); for (int i = 0; i < sz; i++) { s01 = iss.elementAt(i); this.getNextStates(action, args[1], acts, c, s01, s1, nss); } ***/ return s1; } // The following case added by LL on 13 Nov 2009 to handle subexpression names. case OPCODE_nop: { return this.getNextStates(action, args[0], acts, c, s0, s1, nss, cm); } default: { // We handle all the other builtin operators here. Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm); if (!(bval instanceof BoolValue)) { Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "next states", "boolean", bval.toString(), pred.toString() }, pred, c); } if (((BoolValue)bval).val) { resState = this.getNextStates(action, acts, s0, s1, nss, cm); } return resState; } } } /* processUnchanged */ @ExpectInlined protected abstract TLCState processUnchanged(final Action action, SemanticNode expr, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm); protected final TLCState processUnchangedImpl(final Action action, SemanticNode expr, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm) { if (coverage){cm = cm.get(expr);} SymbolNode var = this.getVar(expr, c, false, toolId); TLCState resState = s1; if (var != null) { return processUnchangedImplVar(action, expr, acts, s0, s1, nss, var, cm); } if (expr instanceof OpApplNode) { OpApplNode expr1 = (OpApplNode)expr; ExprOrOpArgNode[] args = expr1.getArgs(); int alen = args.length; SymbolNode opNode = expr1.getOperator(); UniqueString opName = opNode.getName(); int opcode = BuiltInOPs.getOpCode(opName); if (opcode == OPCODE_tup) { return processUnchangedImplTuple(action, acts, c, s0, s1, nss, args, alen, cm, coverage ? cm.get(expr1) : cm); } if (opcode == 0 && alen == 0) { // a 0-arity operator: return processUnchangedImpl0Arity(action, expr, acts, c, s0, s1, nss, cm, opNode, opName); } } return verifyUnchanged(action, expr, acts, c, s0, s1, nss, cm); } @ExpectInlined private final TLCState processUnchangedImpl0Arity(final Action action, final SemanticNode expr, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm, final SymbolNode opNode, final UniqueString opName) { final Object val = this.lookup(opNode, c, false); if (val instanceof OpDefNode) { return this.processUnchanged(action, ((OpDefNode)val).getBody(), acts, c, s0, s1, nss, cm); } else if (val instanceof LazyValue) { final LazyValue lv = (LazyValue)val; return this.processUnchanged(action, lv.expr, acts, lv.con, s0, s1, nss, cm); } return verifyUnchanged(action, expr, acts, c, s0, s1, nss, cm); } /** * Check that <code>expr</code> is unchanged without attempting to synthesize values for variables in the * successor state. */ private TLCState verifyUnchanged(final Action action, final SemanticNode expr, final ActionItemList acts, final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) { TLCState resState = s1; IValue v0 = this.eval(expr, c, s0, cm); IValue v1 = this.eval(expr, c, s1, TLCState.Null, EvalControl.Clear, cm); if (v0.equals(v1)) { resState = this.getNextStates(action, acts, s0, s1, nss, cm); } return resState; } @Override public IValue eval(SemanticNode expr, Context c, TLCState s0) { return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD); } @Override public IValue eval(SemanticNode expr, Context c) { return this.eval(expr, c, TLCState.Empty); } @Override public IValue eval(SemanticNode expr) { return this.eval(expr, Context.Empty); } @ExpectInlined private final TLCState processUnchangedImplTuple(final Action action, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, ExprOrOpArgNode[] args, int alen, CostModel cm, CostModel cmNested) { // a tuple: if (alen != 0) { ActionItemList acts1 = acts; for (int i = alen-1; i > 0; i--) { acts1 = (ActionItemList) acts1.cons(args[i], c, cmNested, IActionItemList.UNCHANGED); } return this.processUnchanged(action, args[0], acts1, c, s0, s1, nss, cmNested); } return this.getNextStates(action, acts, s0, s1, nss, cm); } @ExpectInlined private final TLCState processUnchangedImplVar(final Action action, SemanticNode expr, ActionItemList acts, TLCState s0, TLCState s1, INextStateFunctor nss, SymbolNode var, final CostModel cm) { TLCState resState = s1; // expr is a state variable: final UniqueString varName = var.getName(); final IValue val0 = s0.lookup(varName); final IValue val1 = s1.lookup(varName); if (val1 == null) { resState.bind(varName, val0); if (coverage) { resState = this.getNextStates(action, acts, s0, resState, nss, cm); } else { resState = this.getNextStates0(action, acts, s0, resState, nss, cm); } resState.unbind(varName); } else if (val0.equals(val1)) { if (coverage) { resState = this.getNextStates(action, acts, s0, s1, nss, cm); } else { resState = this.getNextStates0(action, acts, s0, s1, nss, cm); } } else { MP.printWarning(EC.TLC_UNCHANGED_VARIABLE_CHANGED, new String[]{varName.toString(), expr.toString()}); } return resState; } /* eval */ public TLCState evalAlias(TLCState current, TLCState successor) { if ("".equals(this.config.getAlias())) { return current; } // see getState(..) IdThread.setCurrentState(current); // See asserts in tlc2.debug.TLCActionStackFrame.TLCActionStackFrame(TLCStackFrame, SemanticNode, Context, Tool, TLCState, Action, TLCState, RuntimeException) if (successor.getLevel() != current.getLevel()) { // Calling setPrecessor when the levels are equal would increase the level of // successor. successor.setPredecessor(current); } try { final TLCState alias = eval(getAliasSpec(), Context.Empty, current, successor, EvalControl.Clear).toState(); if (alias != null) { return alias; } } catch (EvalException | TLCRuntimeException e) { // Fall back to original state if eval fails. return current; } return current; } @Override public TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor) { if (!hasAlias()) { return current; } return evalAlias(current, successor, Context.Empty); } @Override public TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor, Supplier<List<TLCStateInfo>> prefix) { if (!hasAlias()) { return current; } final ExternalModuleTable emt = getSpecProcessor().getSpecObj().getExternalModuleTable(); final tla2sany.semantic.Context tlcExt = emt.getContext(UniqueString.of("TLCExt")); if (tlcExt == null) { // tlcExt is null if the TLCExt module is not extended or instantiated. Thus, // Trace cannot appear in the spec. return evalAlias(current, successor, Context.Empty); } final SymbolNode tlcExtTrace = tlcExt.getSymbol(UniqueString.of("Trace")); return evalAlias(current, successor, Context.Empty.cons(tlcExtTrace, new LazySupplierValue(tlcExtTrace, (Supplier<Value>) () -> { return new TupleValue( prefix.get().stream().map(si -> new RecordValue(si.state)).toArray(Value[]::new)); }))); } private TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor, Context ctxt) { // see getState(..) IdThread.setCurrentState(current.state); // See asserts in // tlc2.debug.TLCActionStackFrame.TLCActionStackFrame(TLCStackFrame, // SemanticNode, Context, Tool, TLCState, Action, TLCState, RuntimeException) if (successor.getLevel() != current.state.getLevel()) { // Calling setPrecessor when the levels are equal would increase the level of // successor. successor.setPredecessor(current); } try { final TLCState alias = eval(getAliasSpec(), ctxt, current.state, successor, EvalControl.Clear).toState(); if (alias != null) { return new AliasTLCStateInfo(alias, current); } } catch (EvalException | TLCRuntimeException e) { // Fall back to original state if eval fails. return current; // TODO We have to somehow communicate this exception back to the user. // Unfortunately, the alias cannot be validated by SpecProcess (unless pure // constant expression who are too simple to be used in trace expressions). // Throwing the exception would be possible, but pretty annoying if TLC fails // to print an error trace because of a bogus alias after hours of model // checking (this is the very reason why the code falls back to return the // original/current state). Printing the exception to stdout/stderr here // would mess with the Toolbox's parsing that reads stdout back in. It would // also look bad because we would print the error on every evaluation of the // alias and it's conceivable that -in most cases- evaluation would fail for // all evaluations. This suggests that we have to defer reporting of evaluation // and runtime exception until after the error-trace has been printed. If // evaluation only failed for some invocations of evalAlias, the user will // be able to figure out the ones that failed by looking at the trace. This // state should not be kept in Tool, because it doesn't know how to group // sequences of evalAlias invocations. // We could avoid keeping state entirely, if the exception was attached as an // "auxiliary" variable to the TLCStateInfo and printed as part of the error // trace. The error trace would look strange, but it appears to be the best // compromise, especially if only some of the evaluations fail. } return current; } /* Special version of eval for state expressions. */ @Override public IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) { return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm); } @Override public final IValue eval(SemanticNode expr, Context c, TLCState s0, TLCState s1, final int control) { return eval(expr, c, s0, s1, control, CostModel.DO_NOT_RECORD); } public Value evalPure(final OpDefNode opDef, final ExprOrOpArgNode[] args, final Context c, final TLCState s0, final TLCState s1, final int control, final CostModel cm) { final Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId); return this.eval(opDef.getBody(), c1, s0, s1, control, cm); } /* * This method evaluates the expression expr in the given context, * current state, and partial next state. */ public abstract Value eval(SemanticNode expr, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm); @ExpectInlined protected Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0, final TLCState s1, final int control, CostModel cm) { switch (expr.getKind()) { /*********************************************************************** * LabelKind class added by LL on 13 Jun 2007. * ***********************************************************************/ case LabelKind: { LabelNode expr1 = (LabelNode) expr; return this.eval(expr1.getBody(), c, s0, s1, control, cm); } case OpApplKind: { OpApplNode expr1 = (OpApplNode)expr; if (coverage) {cm = cm.get(expr);} return this.evalAppl(expr1, c, s0, s1, control, cm); } case LetInKind: { return evalImplLetInKind((LetInNode) expr, c, s0, s1, control, cm); } case SubstInKind: { return evalImplSubstInKind((SubstInNode) expr, c, s0, s1, control, cm); } // Added by LL on 13 Nov 2009 to handle theorem and assumption names. case APSubstInKind: { return evalImplApSubstInKind((APSubstInNode) expr, c, s0, s1, control, cm); } case NumeralKind: case DecimalKind: case StringKind: { return (Value) WorkerValue.mux(expr.getToolObject(toolId)); } case AtNodeKind: { return (Value)c.lookup(EXCEPT_AT); } case OpArgKind: { return evalImplOpArgKind((OpArgNode) expr, c, s0, s1, cm); } default: { Assert.fail("Attempted to evaluate an expression that cannot be evaluated.\n" + expr, expr, c); return null; // make compiler happy } } } @ExpectInlined private final Value evalImplLetInKind(LetInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) { OpDefNode[] letDefs = expr1.getLets(); int letLen = letDefs.length; Context c1 = c; for (int i = 0; i < letLen; i++) { OpDefNode opDef = letDefs[i]; if (opDef.getArity() == 0) { Value rhs = new LazyValue(opDef.getBody(), c1, cm); c1 = c1.cons(opDef, rhs); } } return this.eval(expr1.getBody(), c1, s0, s1, control, cm); } @ExpectInlined private final Value evalImplSubstInKind(SubstInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) { Subst[] subs = expr1.getSubsts(); int slen = subs.length; Context c1 = c; for (int i = 0; i < slen; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, true, coverage ? sub.getCM() : cm, toolId)); } return this.eval(expr1.getBody(), c1, s0, s1, control, cm); } @ExpectInlined private final Value evalImplApSubstInKind(APSubstInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) { Subst[] subs = expr1.getSubsts(); int slen = subs.length; Context c1 = c; for (int i = 0; i < slen; i++) { Subst sub = subs[i]; c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, true, cm, toolId)); } return this.eval(expr1.getBody(), c1, s0, s1, control, cm); } @ExpectInlined private final Value evalImplOpArgKind(OpArgNode expr1, Context c, TLCState s0, TLCState s1, final CostModel cm) { SymbolNode opNode = expr1.getOp(); Object val = this.lookup(opNode, c, false); if (val instanceof OpDefNode) { return setSource(expr1, new OpLambdaValue((OpDefNode)val, this, c, s0, s1, cm)); } return (Value)val; } /* evalAppl */ @ExpectInlined protected abstract Value evalAppl(final OpApplNode expr, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm); protected final Value evalApplImpl(final OpApplNode expr, Context c, TLCState s0, TLCState s1, final int control, CostModel cm) { if (coverage){ cm = cm.getAndIncrement(expr); } ExprOrOpArgNode[] args = expr.getArgs(); SymbolNode opNode = expr.getOperator(); int opcode = BuiltInOPs.getOpCode(opNode.getName()); if (opcode == 0) { // This is a user-defined operator with one exception: it may // be substed by a builtin operator. This special case occurs // when the lookup returns an OpDef with opcode # 0. Object val = this.lookup(opNode, c, s0, EvalControl.isPrimed(control)); // if (val instanceof Supplier) { // val = ((Supplier) val).get(); // } // First, unlazy if it is a lazy value. We cannot use the cached // value when s1 == null or isEnabled(control). if (val instanceof LazyValue) { final LazyValue lv = (LazyValue) val; if (s1 == null) { val = this.eval(lv.expr, lv.con, s0, TLCState.Null, control, lv.getCostModel()); } else if (lv.isUncachable() || EvalControl.isEnabled(control)) { // Never use cached LazyValues in an ENABLED expression. This is why all // this.enabled* methods pass EvalControl.Enabled (the only exception being the // call on line line 2799 which passes EvalControl.Primed). This is why we can // be sure that ENALBED expressions are not affected by the caching bug tracked // in Github issue 113 (see below). val = this.eval(lv.expr, lv.con, s0, s1, control, lv.getCostModel()); } else { val = lv.getValue(); if (val == null) { final Value res = this.eval(lv.expr, lv.con, s0, s1, control, lv.getCostModel()); // This check has been suggested by Yuan Yu on 01/15/2018: // // If init-states are being generated, level has to be <= ConstantLevel for // caching/LazyValue to be allowed. If next-states are being generated, level // has to be <= VariableLevel. The level indicates if the expression to be // evaluated contains only constants, constants & variables, constants & // variables and primed variables (thus action) or is a temporal formula. // // This restriction is in place to fix Github issue 113 // (https://github.com/tlaplus/tlaplus/issues/113) - // TLC can generate invalid sets of init or next-states caused by broken // LazyValue evaluation. The related tests are AssignmentInit* and // AssignmentNext*. Without this fix TLC essentially reuses a stale lv.val when // it needs to re-evaluate res because the actual operands to eval changed. // Below is Leslie's formal description of the bug: // // The possible initial values of some variable var are specified by a subformula // // F(..., var, ...) // // in the initial predicate, for some operator F such that expanding the // definition of F results in a formula containing more than one occurrence of // var , not all occurring in separate disjuncts of that formula. // // The possible next values of some variable var are specified by a subformula // // F(..., var', ...) // // in the next-state relation, for some operator F such that expanding the // definition of F results in a formula containing more than one occurrence of // var' , not all occurring in separate disjuncts of that formula. // // An example of the first case is an initial predicate Init defined as follows: // // VARIABLES x, ... // F(var) == \/ var \in 0..99 /\ var % 2 = 0 // \/ var = -1 // Init == /\ F(x) // /\ ... // // The error would not appear if F were defined by: // // F(var) == \/ var \in {i \in 0..99 : i % 2 = 0} // \/ var = -1 // // or if the definition of F(x) were expanded in
{'commit': 'diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/IDebugTarget.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/IDebugTarget.java\nindex e00eb2a3a..7c0a1e390 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/debug/IDebugTarget.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/IDebugTarget.java\n@@ -41,11 +41,19 @@ public interface IDebugTarget {\n \t\n \tIDebugTarget popFrame(Tool tool, Value v, SemanticNode expr, Context c, int control);\n \n-\tIDebugTarget popFrame(Tool tool, SemanticNode expr, Context c, TLCState ps);\n+\tIDebugTarget popFrame(Tool tool, SemanticNode expr, Context c, TLCState state);\n \n-\tIDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c, TLCState ps);\n+\tIDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c, TLCState state);\n+\n+\tIDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c, TLCState predecessor, TLCState state);\n+\n+\tIDebugTarget popFrame(Tool tool, SemanticNode expr, Context c, TLCState predecessor, TLCState state);\n \n \tIDebugTarget pushFrame(TLCState state);\n \t\n \tIDebugTarget popFrame(TLCState state);\n+\n+\tIDebugTarget pushFrame(TLCState predecessor, TLCState state);\n+\t\n+\tIDebugTarget popFrame(TLCState predecessor, TLCState state);\n }\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCDebugger.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCDebugger.java\nindex 7c6eacedc..3a53610e4 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCDebugger.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCDebugger.java\n@@ -283,6 +283,14 @@ public abstract class TLCDebugger extends AbstractDebugger implements IDebugTarg\n \t\treturn this;\n \t}\n \n+\t@Override\n+\tpublic IDebugTarget pushFrame(Tool tool, SemanticNode expr, Context c, TLCState predecessor, TLCState ps) {\n+\t\tfinal int level = this.stack.size();\n+\t\tstack.push(new TLCNextStackFrame(expr, c, tool, predecessor, ps));\n+\t\thaltExecution(expr, level);\n+\t\treturn this;\n+\t}\n+\n \t@Override\n \tpublic IDebugTarget pushFrame(TLCState state) {\n \t\tTLCStackFrame f = this.stack.peek();\n@@ -290,12 +298,23 @@ public abstract class TLCDebugger extends AbstractDebugger implements IDebugTarg\n \t\treturn this;\n \t}\n \n+\t@Override\n+\tpublic IDebugTarget pushFrame(TLCState predecessor, TLCState state) {\n+\t\tTLCStackFrame f = this.stack.peek();\n+\t\treturn pushFrame(f.getTool(), f.getNode(), f.getContext(), state);\n+\t}\n+\n \t@Override\n \tpublic IDebugTarget popFrame(TLCState state) {\n \t\tTLCStackFrame f = this.stack.peek();\n \t\treturn popFrame(f.getTool(), f.getNode(), f.getContext(), state);\n \t}\n \n+\t@Override\n+\tpublic IDebugTarget popFrame(TLCState predecessor, TLCState state) {\n+\t\treturn popFrame(state);\n+\t}\n+\n \t@Override\n \tpublic IDebugTarget popFrame(Tool tool, Value v, SemanticNode expr, Context c, int control) {\n \t\tSystem.out.printf("%s Call popFrame: [%s], level: %s\\n",\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCNextStackFrame.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCNextStackFrame.java\nnew file mode 100644\nindex 000000000..3762d3b00\n--- /dev/null\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCNextStackFrame.java\n@@ -0,0 +1,93 @@\n+/*******************************************************************************\n+ * Copyright (c) 2020 Microsoft Research. All rights reserved. \n+ *\n+ * The MIT License (MIT)\n+ * \n+ * Permission is hereby granted, free of charge, to any person obtaining a copy \n+ * of this software and associated documentation files (the "Software"), to deal\n+ * in the Software without restriction, including without limitation the rights\n+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies\n+ * of the Software, and to permit persons to whom the Software is furnished to do\n+ * so, subject to the following conditions:\n+ *\n+ * The above copyright notice and this permission notice shall be included in all\n+ * copies or substantial portions of the Software. \n+ * \n+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\n+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS\n+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR\n+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN\n+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION\n+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.\n+ *\n+ * Contributors:\n+ *   Markus Alexander Kuppe - initial API and implementation\n+ ******************************************************************************/\n+package tlc2.debug;\n+\n+import java.util.ArrayList;\n+import java.util.Arrays;\n+import java.util.List;\n+import java.util.Map;\n+import java.util.Map.Entry;\n+\n+import org.eclipse.lsp4j.debug.Scope;\n+import org.eclipse.lsp4j.debug.Variable;\n+\n+import tla2sany.semantic.SemanticNode;\n+import tlc2.tool.TLCState;\n+import tlc2.tool.impl.Tool;\n+import tlc2.util.Context;\n+import tlc2.value.IValue;\n+import util.UniqueString;\n+\n+public class TLCNextStackFrame extends TLCInitStackFrame {\n+\n+\tprivate final TLCState predecessor;\n+\tprivate final int predId;\n+\n+\tpublic TLCNextStackFrame(SemanticNode expr, Context c, Tool tool, TLCState predecessor, TLCState ps) {\n+\t\tsuper(expr, c , tool, ps);\n+\t\tthis.predecessor = predecessor;\n+\t\t\n+\t\t// Tempting to use state.fingerprint/hashCode, but would normalize all values as a side effect.\n+\t\tthis.predId = rnd.nextInt(Integer.MAX_VALUE - 1) + 1;\n+\t}\n+\n+\t@Override\n+\tpublic Variable[] getVariables(int vr) {\n+\t\tif (vr == predId) {\n+\t\t\tfinal List<Variable> vars = new ArrayList<>();\n+\t\t\tfinal Map<UniqueString, IValue> vals = predecessor.getVals();\n+\t\t\tfor (final Entry<UniqueString, IValue> e : vals.entrySet()) {\n+\t\t\t\tfinal UniqueString key = e.getKey();\n+\t\t\t\tfinal IValue value = e.getValue();\n+\t\t\t\tfinal DebugTLCVariable variable;\n+\t\t\t\tif (value == null) {\n+\t\t\t\t\tvariable = new DebugTLCVariable(key.toString());\n+\t\t\t\t\tvariable.setValue("null");\n+\t\t\t\t} else {\n+\t\t\t\t\tvariable = (DebugTLCVariable) value\n+\t\t\t\t\t\t\t.toTLCVariable(new DebugTLCVariable(key.toString()), rnd);\n+\t\t\t\t\tnestedVariables.put(variable.getVariablesReference(), variable);\n+\t\t\t\t}\n+\t\t\t\tvars.add(variable);\n+\t\t\t}\n+\t\t\treturn vars.toArray(new Variable[vars.size()]);\n+\t\t}\n+\t\treturn super.getVariables(vr);\n+\t}\n+\n+\t@Override\n+\tpublic Scope[] getScopes() {\n+\t\tfinal List<Scope> scopes = new ArrayList<>();\n+\t\tscopes.addAll(Arrays.asList(super.getScopes()));\n+\t\t\n+\t\tfinal Scope scope = new Scope();\n+\t\tscope.setName("Predecessor");\n+\t\tscope.setVariablesReference(predId);\n+\t\tscopes.add(scope);\n+\t\t\n+\t\treturn scopes.toArray(new Scope[scopes.size()]);\n+\t}\n+}\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\nindex 9f5bf55f7..30ab06dcb 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/DebugTool.java\n@@ -126,7 +126,10 @@ public class DebugTool extends Tool {\n \t@Override\n \tprotected final TLCState getNextStatesAppl(final Action action, final OpApplNode pred, final ActionItemList acts,\n \t\t\tfinal Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) {\n-\t\treturn getNextStatesApplImpl(action, pred, acts, c, s0, s1, nss, cm);\n+\t\ttarget.pushFrame(this, pred, c, s0, s1);\n+\t\tTLCState s = getNextStatesApplImpl(action, pred, acts, c, s0, s1, nss, cm);\n+\t\ttarget.popFrame(this, pred, c, s0, s1);\n+\t\treturn s;\n \t}\n \n \t@Override\n@@ -155,10 +158,19 @@ public class DebugTool extends Tool {\n \t\tsuper.getInitStatesAppl(init, acts, c, ps, states, cm);\n \t\ttarget.popFrame(this, init, c, ps);\n \t}\n+\n+\t@Override\n+\tpublic boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n+\t\tif (functor instanceof WrapperNextStateFunctor) {\n+\t\t\treturn super.getNextStates(functor, state);\n+\t\t} else {\n+\t\t\treturn super.getNextStates(new WrapperNextStateFunctor(functor, target), state);\n+\t\t}\n+\t}\n \t\n \tprivate static class WrapperStateFunctor implements IStateFunctor {\n-\t\tprivate final IStateFunctor functor;\n-\t\tprivate final IDebugTarget target;\n+\t\tprotected final IStateFunctor functor;\n+\t\tprotected final IDebugTarget target;\n \n \t\tWrapperStateFunctor(IStateFunctor functor, IDebugTarget target) {\n \t\t\tthis.functor = functor;\n@@ -173,4 +185,19 @@ public class DebugTool extends Tool {\n \t\t\treturn addElement;\n \t\t}\n \t}\n+\n+\tprivate static class WrapperNextStateFunctor extends WrapperStateFunctor implements INextStateFunctor {\n+\n+\t\tWrapperNextStateFunctor(INextStateFunctor functor, IDebugTarget target) {\n+\t\t\tsuper(functor, target);\n+\t\t}\n+\n+\t\t@Override\n+\t\tpublic Object addElement(TLCState predecessor, Action a, TLCState state) {\n+\t\t\ttarget.pushFrame(predecessor, state);\n+\t\t\tObject addElement = ((INextStateFunctor) functor).addElement(predecessor, a, state);\n+\t\t\ttarget.popFrame(predecessor, state);\n+\t\t\treturn addElement;\n+\t\t}\n+\t}\n }\ndiff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\nindex d232c374f..97e385421 100644\n--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\n+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java\n@@ -815,7 +815,7 @@ public abstract class Tool\n   }\n   \n   @Override\n-  public final boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n+  public boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n \t  for (int i = 0; i < actions.length; i++) {\n \t\t\tfinal Action action = actions[i];\n \t\t\tthis.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state, TLCState.Empty.createEmpty(),\n', 'commit_subject': 'Debug the next-state relation.', 'repo_name': 'tlaplus/tlaplus', 'committer': {'name': 'Markus Alexander Kuppe', 'email': '82b77c4221e60124667659f5857eb35e1ec57936@lemmster.de', 'time_sec': '1617337227', 'tz_offset': '-420', 'date': {'seconds': '1617337227'}}, 'commit_tree': '959456d0fa1e4c04a1a8943b6b6c461c34da2bf3', 'commit_message': 'Debug the next-state relation.\n\n[Feature][Debugger]\n', 'language_name': 'R', 'license': 'mit', 'hunks': '@@ -815,7 +815,7 @@ public abstract class Tool\n   }\n   \n   @Override\n-  public final boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n+  public boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n \t  for (int i = 0; i < actions.length; i++) {\n \t\t\tfinal Action action = actions[i];\n \t\t\tthis.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state, TLCState.Empty.createEmpty(),\n', 'addition_count': 1, 'deletion_count': 1, 'src_file': 'a/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java', 'tgt_file': 'b/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java', 'file_extension': '.java', 'before_file': '// Copyright (c) 2003 Compaq Corporation.  All rights reserved.\n// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.\n// Copyright (c) 2022, Oracle and/or its affiliates.\n// Last modified on Wed 12 Jul 2017 at 16:10:00 PST by ian morris nieves\n//      modified on Thu  2 Aug 2007 at 10:25:48 PST by lamport\n//      modified on Fri Jan  4 22:46:57 PST 2002 by yuanyu\n\npackage tlc2.tool.impl;\n\nimport java.io.File;\nimport java.util.HashMap;\nimport java.util.HashSet;\nimport java.util.List;\nimport java.util.Map;\nimport java.util.function.Supplier;\n\nimport tla2sany.parser.SyntaxTreeNode;\nimport tla2sany.semantic.APSubstInNode;\nimport tla2sany.semantic.ExprNode;\nimport tla2sany.semantic.ExprOrOpArgNode;\nimport tla2sany.semantic.ExternalModuleTable;\nimport tla2sany.semantic.FormalParamNode;\nimport tla2sany.semantic.LabelNode;\nimport tla2sany.semantic.LetInNode;\nimport tla2sany.semantic.LevelConstants;\nimport tla2sany.semantic.LevelNode;\nimport tla2sany.semantic.OpApplNode;\nimport tla2sany.semantic.OpArgNode;\nimport tla2sany.semantic.OpDeclNode;\nimport tla2sany.semantic.OpDefNode;\nimport tla2sany.semantic.OpDefOrDeclNode;\nimport tla2sany.semantic.SemanticNode;\nimport tla2sany.semantic.Subst;\nimport tla2sany.semantic.SubstInNode;\nimport tla2sany.semantic.SymbolNode;\nimport tla2sany.semantic.ThmOrAssumpDefNode;\nimport tlc2.TLCGlobals;\nimport tlc2.output.EC;\nimport tlc2.output.MP;\nimport tlc2.tool.Action;\nimport tlc2.tool.BuiltInOPs;\nimport tlc2.tool.EvalControl;\nimport tlc2.tool.EvalException;\nimport tlc2.tool.IActionItemList;\nimport tlc2.tool.IContextEnumerator;\nimport tlc2.tool.INextStateFunctor;\nimport tlc2.tool.IStateFunctor;\nimport tlc2.tool.ITool;\nimport tlc2.tool.StateVec;\nimport tlc2.tool.TLCState;\nimport tlc2.tool.TLCStateFun;\nimport tlc2.tool.TLCStateInfo;\nimport tlc2.tool.TLCStateMut;\nimport tlc2.tool.TLCStateMutExt;\nimport tlc2.tool.ToolGlobals;\nimport tlc2.tool.coverage.CostModel;\nimport tlc2.util.Context;\nimport tlc2.util.ExpectInlined;\nimport tlc2.util.IdThread;\nimport tlc2.util.RandomGenerator;\nimport tlc2.util.Vect;\nimport tlc2.value.IFcnLambdaValue;\nimport tlc2.value.IMVPerm;\nimport tlc2.value.IValue;\nimport tlc2.value.ValueConstants;\nimport tlc2.value.Values;\nimport tlc2.value.impl.Applicable;\nimport tlc2.value.impl.BoolValue;\nimport tlc2.value.impl.Enumerable;\nimport tlc2.value.impl.Enumerable.Ordering;\nimport tlc2.value.impl.EvaluatingValue;\nimport tlc2.value.impl.FcnLambdaValue;\nimport tlc2.value.impl.FcnParams;\nimport tlc2.value.impl.FcnRcdValue;\nimport tlc2.value.impl.LazySupplierValue;\nimport tlc2.value.impl.LazyValue;\nimport tlc2.value.impl.MVPerm;\nimport tlc2.value.impl.MVPerms;\nimport tlc2.value.impl.MethodValue;\nimport tlc2.value.impl.ModelValue;\nimport tlc2.value.impl.OpLambdaValue;\nimport tlc2.value.impl.OpValue;\nimport tlc2.value.impl.RecordValue;\nimport tlc2.value.impl.Reducible;\nimport tlc2.value.impl.SetCapValue;\nimport tlc2.value.impl.SetCupValue;\nimport tlc2.value.impl.SetDiffValue;\nimport tlc2.value.impl.SetEnumValue;\nimport tlc2.value.impl.SetOfFcnsValue;\nimport tlc2.value.impl.SetOfRcdsValue;\nimport tlc2.value.impl.SetOfTuplesValue;\nimport tlc2.value.impl.SetPredValue;\nimport tlc2.value.impl.StringValue;\nimport tlc2.value.impl.SubsetValue;\nimport tlc2.value.impl.TupleValue;\nimport tlc2.value.impl.UnionValue;\nimport tlc2.value.impl.Value;\nimport tlc2.value.impl.ValueEnumeration;\nimport tlc2.value.impl.ValueExcept;\nimport tlc2.value.impl.ValueVec;\nimport util.Assert;\nimport util.Assert.TLCRuntimeException;\nimport util.FilenameToStream;\nimport util.TLAConstants;\nimport util.UniqueString;\n\n/**\n * This class provides useful methods for tools like model checker\n * and simulator.\n *\n * It\'s instance serves as a spec handle\n * This is one of two places in TLC, where not all messages are retrieved from the message printer,\n * but constructed just here in the code.\n */\npublic abstract class Tool\n    extends Spec\n    implements ValueConstants, ToolGlobals, ITool\n{\n\n  \tpublic static final String PROBABLISTIC_KEY = Tool.class.getName() + ".probabilistic";\n    /*\n\t * Prototype, do *not* activate when checking safety or liveness!!!:\n\t * For simulation that is not meant as a substitute of exhaustive checking for too\n\t * large models, it can be useful to generate behaviors as quickly as possible,\n\t * i.e. without checking all successor states along the states of the behavior.\n\t * This flag activates the code path that efficiently generate only a single \n\t * successor state during simulation.  It does not let the user parameterize\n\t * the code with a particular distribution, but instead draws from the uniform\n\t * distribution.  \n\t * \n\t * In its current form, it only handles non-determinism expressed with opcode\n\t * OPCODE_be (bounded exist), i.e. (which simply happened to be the primary\n\t * expression that we encountered in the SWIM spec during this work):\n\t * \n\t * VARIABLE x\n\t * \\E n \\in S: x\' = n\n\t * \n\t * Activate with: -Dtlc2.tool.impl.Tool.probabilistic=true\n\t */\n  private static final boolean PROBABLISTIC = Boolean.getBoolean(PROBABLISTIC_KEY);\n\n  public enum Mode {\n\t  Simulation, MC, MC_DEBUG, Executor;\n  }\n\t\n  public static final Value[] EmptyArgs = new Value[0];\n\n  protected final Action[] actions;     // the list of TLA actions.\n  private Vect<Action> actionVec = new Vect<>(10);\n  protected final Mode toolMode;\n\n  /**\n   * Creates a new tool handle\n   */\n  public Tool(String specFile, String configFile) {\n\t  this(new File(specFile), specFile, configFile, null);\n  }\n  \n  public Tool(String specFile, String configFile, FilenameToStream resolver) {\n\t  this(new File(specFile), specFile, configFile, resolver);\n  }\n  \n  public Tool(String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params) {\n\t  this(new File(specFile), specFile, configFile, resolver, params);\n  }\n\n  public Tool(String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params) {\n\t  this(new File(specFile), specFile, configFile, resolver, mode, params);\n  }\n  \n  private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver)\n  {\n\t  this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, new HashMap<>());\n  }\n  \n  private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params)\n  {\n\t  this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, params);\n  }\n  \n  private Tool(File specDir, String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params)\n  {\n\t  this(specDir.isAbsolute() ? specDir.getParent() : "", specFile, configFile, resolver, mode, params);\n  }\n  \n  public Tool(String specDir, String specFile, String configFile, FilenameToStream resolver, final Map<String, Object> params)\n  {\n\t  this(specDir, specFile, configFile, resolver, Mode.MC, params);\n  }\n  \n  public Tool(String specDir, String specFile, String configFile, FilenameToStream resolver, Mode mode, final Map<String, Object> params)\n  {\n      super(specDir, specFile, configFile, resolver, mode, params);\n\n      this.toolMode = mode;\n\t\t// set variables to the static filed in the state\n\t\tif (mode == Mode.Simulation || mode == Mode.Executor || mode == Mode.MC_DEBUG) {\n\t\t\tassert TLCState.Empty instanceof TLCStateMutExt;\n\t\t\tTLCStateMutExt.setTool(this);\n\t\t} else {\n\t\t\t// Initialize state.\n\t\t\tassert TLCState.Empty instanceof TLCStateMut;\n\t\t\tTLCStateMut.setTool(this);\n\t\t}\n      \n\t\tAction next = this.getNextStateSpec();\n\t\tif (next == null) {\n\t\t\tthis.actions = new Action[0];\n\t\t} else {\n\t\t\tthis.getActions(next);\n\t\t\tint sz = this.actionVec.size();\n\t\t\tthis.actions = new Action[sz];\n\t\t\tfor (int i = 0; i < sz; i++) {\n\t\t\t\tthis.actions[i] = (Action) this.actionVec.elementAt(i);\n\t\t\t}\n\t\t}\n\t\t\n\t\t// Tag the initial predicates and next-state actions.\n\t\tfinal Vect<Action> initAndNext = getInitStateSpec().concat(actionVec);\n\t\tfor (int i = 0; i < initAndNext.size(); i++) {\n\t\t\tinitAndNext.elementAt(i).setId(i);\n\t\t}\n  }\n\n  Tool(Tool other) {\n\t  super(other);\n\t  this.actions = other.actions;\n\t  this.actionVec = other.actionVec;\n\t  this.toolMode = other.toolMode;\n  }\n\n  @Override\n  public Mode getMode() {\n\t  return this.toolMode;\n  }\n  \n\t/**\n   * This method returns the set of all possible actions of the\n   * spec, and sets the actions field of this object. In fact, we\n   * could simply treat the next predicate as one "giant" action.\n   * But for efficiency, we preprocess the next state predicate by\n   * splitting it into a set of actions for the maximum prefix\n   * of disjunction and existential quantification.\n   */\n  @Override\n  public final Action[] getActions() {\n    return this.actions;\n  }\n\n\tprivate final void getActions(final Action next) {\n\t\tthis.getActions(next.pred, next.con, next.getOpDef(), next.cm);\n\t}\n\n  private final void getActions(SemanticNode next, Context con, final OpDefNode opDefNode, CostModel cm) {\n    switch (next.getKind()) {\n    case OpApplKind:\n      {\n        OpApplNode next1 = (OpApplNode)next;\n        this.getActionsAppl(next1, con, opDefNode, cm);\n        return;\n      }\n    case LetInKind:\n      {\n        LetInNode next1 = (LetInNode)next;\n        this.getActions(next1.getBody(), con, opDefNode, cm);\n        return;\n      }\n    case SubstInKind:\n      {\n        SubstInNode next1 = (SubstInNode)next;\n        Subst[] substs = next1.getSubsts();\n        if (substs.length == 0) {\n          this.getActions(next1.getBody(), con, opDefNode, cm);\n        }\n        else {\n          Action action = new Action(next1, con, opDefNode);\n          this.actionVec.addElement(action);\n        }\n        return;\n      }\n\n      // Added by LL on 13 Nov 2009 to handle theorem and assumption names.\n      case APSubstInKind:\n        {\n          APSubstInNode next1 = (APSubstInNode)next;\n          Subst[] substs = next1.getSubsts();\n          if (substs.length == 0) {\n            this.getActions(next1.getBody(), con, opDefNode, cm);\n          }\n          else {\n            Action action = new Action(next1, con, opDefNode);\n            this.actionVec.addElement(action);\n          }\n          return;\n        }\n\n    /***********************************************************************\n    * LabelKind class added by LL on 13 Jun 2007.                          *\n    ***********************************************************************/\n    case LabelKind:\n      {\n        LabelNode next1 = (LabelNode)next;\n        this.getActions(next1.getBody(), con, opDefNode, cm);\n        return;\n      }\n    default:\n      {\n        Assert.fail("The next state relation is not a boolean expression.\\n" + next, next, con);\n      }\n    }\n  }\n\n  private final void getActionsAppl(OpApplNode next, Context con, final OpDefNode actionName, CostModel cm) {\n    ExprOrOpArgNode[] args = next.getArgs();\n    SymbolNode opNode = next.getOperator();\n    int opcode = BuiltInOPs.getOpCode(opNode.getName());\n\n    if (opcode == 0) {\n      Object val = this.lookup(opNode, con, false);\n\n      if (val instanceof OpDefNode) {\n        OpDefNode opDef = (OpDefNode)val;\n        opcode = BuiltInOPs.getOpCode(opDef.getName());\n        if (opcode == 0) {\n          try {\n            FormalParamNode[] formals = opDef.getParams();\n            int alen = args.length;\n            int argLevel = 0;\n            for (int i = 0; i < alen; i++) {\n              argLevel = args[i].getLevel();\n              if (argLevel != 0) break;\n            }\n            if (argLevel == 0) {\n              Context con1 = con;\n              for (int i = 0; i < alen; i++) {\n                IValue aval = this.eval(args[i], con, TLCState.Empty, cm);\n                con1 = con1.cons(formals[i], aval);\n              }\n              this.getActions(opDef.getBody(), con1, opDef, cm);\n              return;\n            }\n          }\n          catch (Throwable e) { /*SKIP*/ }\n        }\n      }\n      if (opcode == 0) {\n        Action action = new Action(next, con, (OpDefNode) opNode);\n        this.actionVec.addElement(action);\n        return;\n      }\n    }\n\n    switch (opcode) {\n    case OPCODE_be:     // BoundedExists\n      {\n        final int cnt = this.actionVec.size();\n        try {\n          ContextEnumerator Enum =\n            this.contexts(next, con, TLCState.Empty, TLCState.Empty, EvalControl.Clear, cm);\n          if (Enum.isDone()) {\n        \t  // No exception and no actions created implies Enum was empty:\n        \t  // \\E i \\in {} : ...\n        \t  // \\E i \\in Nat: FALSE\n        \t  // ...\n        \t  this.actionVec.addElement(new Action(next, con, actionName));\n        \t  return;\n          }\n          Context econ;\n          while ((econ = Enum.nextElement()) != null) {\n            this.getActions(args[0], econ, actionName, cm);\n          }\n\t\t\tassert (cnt < this.actionVec.size())\n\t\t\t\t\t: "AssertionError when creating Actions. This case should have been handled by Enum.isDone conditional above!";\n        }\n        catch (Throwable e) {\n          Action action = new Action(next, con, actionName);\n          this.actionVec.removeAll(cnt);\n          this.actionVec.addElement(action);\n        }\n        return;\n      }\n    case OPCODE_dl:     // DisjList\n    case OPCODE_lor:\n      {\n        for (int i = 0; i < args.length; i++) {\n          this.getActions(args[i], con, actionName, cm);\n        }\n        return;\n      }\n    default:\n      {\n        // We handle all the other builtin operators here.\n        Action action = new Action(next, con, actionName);\n        this.actionVec.addElement(action);\n        return;\n      }\n    }\n  }\n\n  /*\n   * This method returns the set of possible initial states that\n   * satisfies the initial state predicate. Initial state predicate\n   * can be under-specified.  Too many possible initial states will\n   * probably make tools like TLC useless.\n   */\n  @Override\n  public final StateVec getInitStates() {\n\t  final StateVec initStates = new StateVec(0);\n\t  getInitStates(initStates);\n\t  return initStates;\n  }\n\n  @Override\n  public final void getInitStates(IStateFunctor functor) {\n\t  Vect<Action> init = this.getInitStateSpec();\n\t  ActionItemList acts = ActionItemListExt.Empty;\n      // MAK 09/11/2018: Tail to head iteration order cause the first elem added with\n      // acts.cons to be acts tail. This fixes the bug/funny behavior that the init\n      // predicate Init == A /\\ B /\\ C /\\ D was evaluated in the order A, D, C, B (A\n      // doesn\'t get added to acts at all).\n\t  for (int i = (init.size() - 1); i > 0; i--) {\n\t\t  Action elem = (Action)init.elementAt(i);\n\t\t  acts = (ActionItemList) acts.cons(elem, IActionItemList.PRED);\n\t  }\n\t  if (init.size() != 0) {\n\t\t  Action elem = (Action)init.elementAt(0);\n\t\t  TLCState ps = TLCState.Empty.createEmpty();\n\t\t  if (acts.isEmpty()) {\n\t\t\t  acts.setAction(elem);\n\t\t  }\n\t\t  this.getInitStates(elem.pred, acts, elem.con, ps, functor, elem.cm);\n\t  }\n  }\n\n  /* Create the state specified by pred.  */\n  @Override\n  public final TLCState makeState(SemanticNode pred) {\n    ActionItemList acts = ActionItemList.Empty;\n    TLCState ps = TLCState.Empty.createEmpty();\n    StateVec states = new StateVec(0);\n    this.getInitStates(pred, acts, Context.Empty, ps, states, acts.cm);\n    if (states.size() != 1) {\n      Assert.fail("The predicate does not specify a unique state." + pred, pred);\n    }\n    TLCState state = states.elementAt(0);\n    if (!this.isGoodState(state)) {\n      Assert.fail("The state specified by the predicate is not complete." + pred, pred);\n    }\n    return state;\n  }\n\n  protected void getInitStates(SemanticNode init, ActionItemList acts,\n                                   Context c, TLCState ps, IStateFunctor states, CostModel cm) {\n        switch (init.getKind()) {\n        case OpApplKind:\n          {\n            OpApplNode init1 = (OpApplNode)init;\n            this.getInitStatesAppl(init1, acts, c, ps, states, cm);\n            return;\n          }\n        case LetInKind:\n          {\n            LetInNode init1 = (LetInNode)init;\n            this.getInitStates(init1.getBody(), acts, c, ps, states, cm);\n            return;\n          }\n        case SubstInKind:\n          {\n            SubstInNode init1 = (SubstInNode)init;\n            Subst[] subs = init1.getSubsts();\n            Context c1 = c;\n            for (int i = 0; i < subs.length; i++) {\n              Subst sub = subs[i];\n              c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, coverage ? sub.getCM() : cm, toolId));\n            }\n            this.getInitStates(init1.getBody(), acts, c1, ps, states, cm);\n            return;\n          }\n        // Added by LL on 13 Nov 2009 to handle theorem and assumption names.\n        case APSubstInKind:\n          {\n            APSubstInNode init1 = (APSubstInNode)init;\n            Subst[] subs = init1.getSubsts();\n            Context c1 = c;\n            for (int i = 0; i < subs.length; i++) {\n              Subst sub = subs[i];\n              c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, cm, toolId));\n            }\n            this.getInitStates(init1.getBody(), acts, c1, ps, states, cm);\n            return;\n          }\n        // LabelKind class added by LL on 13 Jun 2007\n        case LabelKind:\n          {\n            LabelNode init1 = (LabelNode)init;\n            this.getInitStates(init1.getBody(), acts, c, ps, states, cm);\n            return;\n          }\n        default:\n          {\n            Assert.fail("The init state relation is not a boolean expression.\\n" + init, init, c);\n          }\n        }\n  }\n\n  protected void getInitStates(ActionItemList acts, TLCState ps, IStateFunctor states, CostModel cm) {\n\t\tif (acts.isEmpty()) {\n\t\t\tif (coverage) {\n\t\t\t\tcm.incInvocations();\n\t\t\t\tcm.getRoot().incInvocations();\n\t\t\t}\n\t\t\tstates.addElement(ps.copy().setAction(acts.getAction()));\n\t\t\treturn;\n\t\t} else if (ps.allAssigned()) {\n\t\t\t// MAK 05/25/2018: If all values of the initial state have already been\n\t\t\t// assigned, there is no point in further trying to assign values. Instead, all\n\t\t\t// remaining statements (ActionItemList) can just be evaluated for their boolean\n\t\t\t// value.\n\t\t\t// This optimization is especially useful to check inductive invariants which\n\t\t\t// require TLC to generate a very large set of initial states.\n\t\t\twhile (!acts.isEmpty()) {\n\t\t\t\tfinal Value bval = this.eval(acts.carPred(), acts.carContext(), ps, TLCState.Empty, EvalControl.Init, acts.cm);\n\t\t\t\tif (!(bval instanceof BoolValue)) {\n\t\t\t\t\t//TODO Choose more fitting error message.\n\t\t\t\t\tAssert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING,\n\t\t\t\t\t\t\tnew String[] { "initial states", "boolean", bval.toString(), acts.pred.toString() }, acts.carPred(), acts.carContext());\n\t\t\t\t}\n\t\t\t\tif (!((BoolValue) bval).val) {\n\t\t\t\t\tif (coverage) {\n\t\t\t\t\t\t// Increase "states found".\n\t\t\t\t\t\tcm.getRoot().incSecondary();\n\t\t\t\t\t}\n\t\t\t\t\treturn;\n\t\t\t\t}\n\t\t\t\t// Move on to the next action in the ActionItemList.\n\t\t\t\tacts = acts.cdr();\n\t\t\t}\n\t\t\tif (coverage) {\n\t\t\t\tcm.incInvocations();\n\t\t\t\tcm.getRoot().incInvocations();\n\t\t\t}\n\t\t\tstates.addElement(ps.copy().setAction(acts.getAction()));\n\t\t\treturn;\n\t\t}\n\t\t// Assert.check(act.kind > 0 || act.kind == -1);\n\t\tActionItemList acts1 = acts.cdr();\n\t\tthis.getInitStates(acts.carPred(), acts1, acts.carContext(), ps, states, acts.cm);\n\t  }\n\n  protected void getInitStatesAppl(OpApplNode init, ActionItemList acts,\n                                       Context c, TLCState ps, IStateFunctor states, CostModel cm) {\n    if (coverage) {cm = cm.get(init);}\n        ExprOrOpArgNode[] args = init.getArgs();\n        int alen = args.length;\n        SymbolNode opNode = init.getOperator();\n        int opcode = BuiltInOPs.getOpCode(opNode.getName());\n\n        if (opcode == 0) {\n          // This is a user-defined operator with one exception: it may\n          // be substed by a builtin operator. This special case occurs\n          // when the lookup returns an OpDef with opcode # 0.\n          Object val = this.lookup(opNode, c, ps, false);\n\n          if (val instanceof OpDefNode) {\n            OpDefNode opDef = (OpDefNode)val;\n            opcode = BuiltInOPs.getOpCode(opDef.getName());\n            if (opcode == 0) {\n              // Context c1 = this.getOpContext(opDef, args, c, false);\n              Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId);\n              this.getInitStates(opDef.getBody(), acts, c1, ps, states, cm);\n              return;\n            }\n          }\n          // Added 13 Nov 2009 by LL to fix Yuan\'s fix.\n          /*********************************************************************\n          * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode    *\n          * imported with parameterized instantiation.                         *\n          *********************************************************************/\n          if (val instanceof ThmOrAssumpDefNode) {\n            ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode)val;\n            opcode = BuiltInOPs.getOpCode(opDef.getName());\n            Context c1 = this.getOpContext(opDef, args, c, true);\n            this.getInitStates(opDef.getBody(), acts, c1, ps, states, cm);\n            return;\n          }\n\n          if (val instanceof LazyValue) {\n            LazyValue lv = (LazyValue)val;\n            if (lv.getValue() == null || lv.isUncachable()) {\n              this.getInitStates(lv.expr, acts, lv.con, ps, states, cm);\n              return;\n            }\n            val = lv.getValue();\n          }\n\n          Object bval = val;\n          if (alen == 0) {\n            if (val instanceof MethodValue) {\n              bval = ((MethodValue)val).apply(EmptyArgs, EvalControl.Init);\n            } else if (val instanceof EvaluatingValue) {\n              // Allow EvaluatingValue overwrites to have zero arity.\n              bval = ((EvaluatingValue) val).eval(this, args, c, ps, TLCState.Empty, EvalControl.Init, cm);\n            }\n          }\n          else {\n            if (val instanceof OpValue) {\n          \t  bval = ((OpValue) val).eval(this, args, c, ps, TLCState.Empty, EvalControl.Init, cm);\n            }\n          }\n\n          if (opcode == 0)\n          {\n            if (!(bval instanceof BoolValue))\n            {\n              Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "initial states", "boolean",\n                        bval.toString(), init.toString() }, init, c);\n            }\n            if (((BoolValue) bval).val)\n            {\n              this.getInitStates(acts, ps, states, cm);\n            }\n            return;\n          }\n        }\n\n        switch (opcode) {\n        case OPCODE_dl:     // DisjList\n        case OPCODE_lor:\n          {\n            for (int i = 0; i < alen; i++) {\n              this.getInitStates(args[i], acts, c, ps, states, cm);\n            }\n            return;\n          }\n        case OPCODE_cl:     // ConjList\n        case OPCODE_land:\n          {\n            for (int i = alen-1; i > 0; i--) {\n              acts = (ActionItemList) acts.cons(args[i], c, cm, i);\n            }\n            this.getInitStates(args[0], acts, c, ps, states, cm);\n            return;\n          }\n        case OPCODE_be:     // BoundedExists\n          {\n            SemanticNode body = args[0];\n            ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init, cm);\n            Context c1;\n            while ((c1 = Enum.nextElement()) != null) {\n              this.getInitStates(body, acts, c1, ps, states, cm);\n            }\n            return;\n          }\n        case OPCODE_bf:     // BoundedForall\n          {\n            SemanticNode body = args[0];\n            ContextEnumerator Enum = this.contexts(init, c, ps, TLCState.Empty, EvalControl.Init, cm);\n            Context c1 = Enum.nextElement();\n            if (c1 == null) {\n              this.getInitStates(acts, ps, states, cm);\n            }\n            else {\n              ActionItemList acts1 = acts;\n              Context c2;\n              while ((c2 = Enum.nextElement()) != null) {\n                acts1 = (ActionItemList) acts1.cons(body, c2, cm, IActionItemList.PRED);\n              }\n              this.getInitStates(body, acts1, c1, ps, states, cm);\n            }\n            return;\n          }\n        case OPCODE_ite:    // IfThenElse\n          {\n            Value guard = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm);\n            if (!(guard instanceof BoolValue)) {\n              Assert.fail("In computing initial states, a non-boolean expression (" +\n                          guard.getKindString() + ") was used as the condition " +\n                          "of an IF.\\n" + init, init, c);\n            }\n            int idx = (((BoolValue)guard).val) ? 1 : 2;\n            this.getInitStates(args[idx], acts, c, ps, states, cm);\n            return;\n          }\n        case OPCODE_case:   // Case\n          {\n            SemanticNode other = null;\n            for (int i = 0; i < alen; i++) {\n              OpApplNode pair = (OpApplNode)args[i];\n              ExprOrOpArgNode[] pairArgs = pair.getArgs();\n              if (pairArgs[0] == null) {\n                other = pairArgs[1];\n              }\n              else {\n                Value bval = this.eval(pairArgs[0], c, ps, TLCState.Empty, EvalControl.Init, cm);\n                if (!(bval instanceof BoolValue)) {\n                  Assert.fail("In computing initial states, a non-boolean expression (" +\n                              bval.getKindString() + ") was used as a guard condition" +\n                              " of a CASE.\\n" + pairArgs[1], pairArgs[1], c);\n                }\n                if (((BoolValue)bval).val) {\n                  this.getInitStates(pairArgs[1], acts, c, ps, states, cm);\n                  return;\n                }\n              }\n            }\n            if (other == null) {\n              Assert.fail("In computing initial states, TLC encountered a CASE with no" +\n                          " conditions true.\\n" + init, init, c);\n            }\n            this.getInitStates(other, acts, c, ps, states, cm);\n            return;\n          }\n        case OPCODE_fa:     // FcnApply\n          {\n            Value fval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm);\n            if (fval instanceof FcnLambdaValue) {\n              FcnLambdaValue fcn = (FcnLambdaValue)fval;\n              if (fcn.fcnRcd == null) {\n                Context c1 = this.getFcnContext(fcn, args, c, ps, TLCState.Empty, EvalControl.Init, cm);\n                this.getInitStates(fcn.body, acts, c1, ps, states, cm);\n                return;\n              }\n              fval = fcn.fcnRcd;\n            }\n            else if (!(fval instanceof Applicable)) {\n              Assert.fail("In computing initial states, a non-function (" +\n                          fval.getKindString() + ") was applied as a function.\\n" + init, init, c);\n            }\n            Applicable fcn = (Applicable) fval;\n            Value argVal = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm);\n            Value bval = fcn.apply(argVal, EvalControl.Init);\n            if (!(bval instanceof BoolValue))\n            {\n              Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "initial states", "boolean",\n                      init.toString() }, args[1], c);\n            }\n            if (((BoolValue)bval).val) {\n              this.getInitStates(acts, ps, states, cm);\n            }\n            return;\n          }\n        case OPCODE_eq:\n          {\n            SymbolNode var = this.getVar(args[0], c, false, toolId);\n            if (var == null || var.getName().getVarLoc() < 0) {\n              Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm);\n              if (!((BoolValue)bval).val) {\n                return;\n              }\n            }\n            else {\n              UniqueString varName = var.getName();\n              IValue lval = ps.lookup(varName);\n              Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm);\n              if (lval == null) {\n                ps = ps.bind(varName, rval);\n                this.getInitStates(acts, ps, states, cm);\n                ps.unbind(varName);\n                return;\n              }\n              else {\n                if (!lval.equals(rval)) {\n                  return;\n                }\n              }\n            }\n            this.getInitStates(acts, ps, states, cm);\n            return;\n          }\n        case OPCODE_in:\n          {\n            SymbolNode var = this.getVar(args[0], c, false, toolId);\n            if (var == null || var.getName().getVarLoc() < 0) {\n              Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm);\n              if (!((BoolValue)bval).val) {\n                return;\n              }\n            }\n            else {\n              UniqueString varName = var.getName();\n              Value lval = (Value) ps.lookup(varName);\n              Value rval = this.eval(args[1], c, ps, TLCState.Empty, EvalControl.Init, cm);\n              if (lval == null) {\n                if (!(rval instanceof Enumerable)) {\n                  Assert.fail("In computing initial states, the right side of \\\\IN" +\n                              " is not enumerable.\\n" + init, init, c);\n                }\n                ValueEnumeration Enum = ((Enumerable)rval).elements();\n                Value elem;\n                while ((elem = Enum.nextElement()) != null) {\n                  ps.bind(varName, elem);\n                  this.getInitStates(acts, ps, states, cm);\n                  ps.unbind(varName);\n                }\n                return;\n              }\n              else {\n                if (!rval.member(lval)) {\n                  return;\n                }\n              }\n            }\n            this.getInitStates(acts, ps, states, cm);\n            return;\n          }\n        case OPCODE_implies:\n          {\n            Value lval = this.eval(args[0], c, ps, TLCState.Empty, EvalControl.Init, cm);\n            if (!(lval instanceof BoolValue)) {\n              Assert.fail("In computing initial states of a predicate of form" +\n                          " P => Q, P was " + lval.getKindString() + "\\n." + init, init, c);\n            }\n            if (((BoolValue)lval).val) {\n              this.getInitStates(args[1], acts, c, ps, states, cm);\n  }\n  \n  @Override\n  public final boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n\t  for (int i = 0; i < actions.length; i++) {\n\t\t\tfinal Action action = actions[i];\n\t\t\tthis.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state, TLCState.Empty.createEmpty(),\n        case OPCODE_nop:\n        {\n           this.getInitStates(args[0], acts, c, ps, states, cm);\n           return;\n        }\n        default:\n          {\n            // For all the other builtin operators, simply evaluate:\n            Value bval = this.eval(init, c, ps, TLCState.Empty, EvalControl.Init, cm);\n            if (!(bval instanceof BoolValue)) {\n\n              Assert.fail("In computing initial states, TLC expected a boolean expression," +\n                          "\\nbut instead found " + bval + ".\\n" + init, init, c);\n            }\n            if (((BoolValue)bval).val) {\n              this.getInitStates(acts, ps, states, cm);\n            }\n            return;\n          }\n        }\n  }\n  \n  /**\n   * This method returns the set of next states when taking the action\n   * in the given state.\n   */\n  @Override\n  public final StateVec getNextStates(Action action, TLCState state) {\n\t  return getNextStates(action, action.con, state);\n  }\n  \n  public final StateVec getNextStates(final Action action, final Context ctx, final TLCState state) {\n    ActionItemList acts = ActionItemList.Empty;\n    TLCState s1 = TLCState.Empty.createEmpty();\n    StateVec nss = new StateVec(0);\n    this.getNextStates(action, action.pred, acts, ctx, state, s1.setPredecessor(state).setAction(action), nss, action.cm);\n    if (coverage) { action.cm.incInvocations(nss.size()); }\n    if (PROBABLISTIC && nss.size() > 1) {System.err.println("Simulator generated more than one next state");}\n    return nss;\n  }\n  \n  @Override\n  public boolean getNextStates(final INextStateFunctor functor, final TLCState state) {\n\t  for (int i = 0; i < actions.length; i++) {\n\t\t\tthis.getNextStates(functor, state, actions[i]);\n\t\t}\n\t\treturn false;\n  }\n\n  public boolean getNextStates(final INextStateFunctor functor, final TLCState state, final Action action) {\n\t\tthis.getNextStates(action, action.pred, ActionItemList.Empty, action.con, state,\n\t\t\t\tTLCState.Empty.createEmpty().setPredecessor(state).setAction(action), functor, action.cm);\n\t\treturn false;\n  }\n  \n  protected abstract TLCState getNextStates(final Action action, SemanticNode pred, ActionItemList acts, Context c,\n                                       TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm);\n  \n  protected final TLCState getNextStatesImpl(final Action action, SemanticNode pred, ActionItemList acts, Context c,\n              TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm) {\n        switch (pred.getKind()) {\n        case OpApplKind:\n          {\n            OpApplNode pred1 = (OpApplNode)pred;\n            if (coverage) {cm = cm.get(pred);}\n            return this.getNextStatesAppl(action, pred1, acts, c, s0, s1, nss, cm);\n          }\n        case LetInKind:\n          {\n            LetInNode pred1 = (LetInNode)pred;\n            return this.getNextStates(action, pred1.getBody(), acts, c, s0, s1, nss, cm);\n          }\n        case SubstInKind:\n          {\n            return getNextStatesImplSubstInKind(action, (SubstInNode) pred, acts, c, s0, s1, nss, cm);\n          }\n        // Added by LL on 13 Nov 2009 to handle theorem and assumption names.\n        case APSubstInKind:\n          {\n            return getNextStatesImplApSubstInKind(action, (APSubstInNode) pred, acts, c, s0, s1, nss, cm);\n          }\n        // LabelKind class added by LL on 13 Jun 2007\n        case LabelKind:\n          {\n            LabelNode pred1 = (LabelNode)pred;\n            return this.getNextStates(action, pred1.getBody(), acts, c, s0, s1, nss, cm);\n          }\n        default:\n          {\n            Assert.fail("The next state relation is not a boolean expression.\\n" + pred, pred, c);\n          }\n        }\n    \treturn s1;\n  }\n\n  @ExpectInlined\n  private final TLCState getNextStatesImplSubstInKind(final Action action, SubstInNode pred1, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm) {\n  \tSubst[] subs = pred1.getSubsts();\n  \tint slen = subs.length;\n  \tContext c1 = c;\n  \tfor (int i = 0; i < slen; i++) {\n  \t  Subst sub = subs[i];\n  \t  c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, coverage ? sub.getCM() : cm, toolId));\n  \t}\n  \treturn this.getNextStates(action, pred1.getBody(), acts, c1, s0, s1, nss, cm);\n  }\n  \n  @ExpectInlined\n  private final TLCState getNextStatesImplApSubstInKind(final Action action, APSubstInNode pred1, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm) {\n  \tSubst[] subs = pred1.getSubsts();\n  \tint slen = subs.length;\n  \tContext c1 = c;\n  \tfor (int i = 0; i < slen; i++) {\n  \t  Subst sub = subs[i];\n  \t  c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, cm, toolId));\n  \t}\n  \treturn this.getNextStates(action, pred1.getBody(), acts, c1, s0, s1, nss, cm);\n  }\n  \n  @ExpectInlined\n  private final TLCState getNextStates(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1,\n          final INextStateFunctor nss, CostModel cm) {\n\t  final TLCState copy = getNextStates0(action, acts, s0, s1, nss, cm);\n\t  if (coverage && copy != s1) {\n\t\t  cm.incInvocations();\n\t  }\n\t  return copy;\n  }\n\n  \n  @ExpectInlined\n  private final TLCState getNextStates0(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1,\n                                       final INextStateFunctor nss, CostModel cm) {\n    if (acts.isEmpty()) {\n      nss.addElement(s0, action, s1);\n      return s1.copy();\n    } else if (TLCGlobals.warn && s1.allAssigned()) {\n\t\t// If all variables have been assigned and warnings are turned off, Tool can\n\t\t// execute the fast-path that avoids generating known successor states, but\n\t\t// doesn\'t trigger a warning in cases like:\n    \t//  ---- MODULE F ----\n    \t//  VARIABLES x\n    \t//  Init == x = 0\n    \t//  Next == x\' = 42 /\\ UNCHANGED x \\* UNCHANGED and changed!\n    \t//  ====\n    \t// => "Warning: The variable x was changed while it is specified as UNCHANGED"\n    \treturn getNextStatesAllAssigned(action, acts, s0, s1, nss, cm);\n    }\n\n    final int kind = acts.carKind();\n    SemanticNode pred = acts.carPred();\n    Context c = acts.carContext();\n    ActionItemList acts1 = acts.cdr();\n    cm = acts.cm;\n    if (kind > 0) {\n      return this.getNextStates(action, pred, acts1, c, s0, s1, nss, cm);\n    }\n    else if (kind == -1) {\n      return this.getNextStates(action, pred, acts1, c, s0, s1, nss, cm);\n    }\n    else if (kind == -2) {\n      return this.processUnchanged(action, pred, acts1, c, s0, s1, nss, cm);\n    }\n    else {\n      IValue v1 = this.eval(pred, c, s0, cm);\n      IValue v2 = this.eval(pred, c, s1, cm);\n      if (!v1.equals(v2)) {\n    \t  if (coverage) {\n    \t\t  return this.getNextStates(action, acts1, s0, s1, nss, cm);\n    \t  } else {\n    \t\t  return this.getNextStates0(action, acts1, s0, s1, nss, cm);\n    \t  }\n      }\n    }\n    return s1;\n  }\n  \n  private final TLCState getNextStatesAllAssigned(final Action action, ActionItemList acts, final TLCState s0, final TLCState s1,\n\t\t  \t\t\t\t\t\t\t\tfinal INextStateFunctor nss, final CostModel cm) {\n\t  int kind = acts.carKind();\n\t  SemanticNode pred = acts.carPred();\n\t  Context c = acts.carContext();\n      CostModel cm2 = acts.cm;\n\t  while (!acts.isEmpty()) {\n\t\t  if (kind > 0 || kind == -1) {\n\t\t\t  final Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm2);\n\t\t\t  if (!(bval instanceof BoolValue)) {\n\t\t\t\t  // TODO Choose more fitting error message.\n\t\t\t\t  Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING,\n\t\t\t\t\t\t  new String[] { "next states", "boolean", bval.toString(), acts.pred.toString() }, pred, c);\n\t\t\t  }\n\t\t\t  if (!((BoolValue) bval).val) {\n\t\t\t\t  return s1;\n\t\t\t  }\n\t\t  } else if (kind == -2) {\n\t\t\t  // Identical to default handling below (line 876). Ignored during this optimization.\n\t\t\t  return this.processUnchanged(action, pred, acts.cdr(), c, s0, s1, nss, cm2);\n\t\t  } else {\n\t\t\t  final IValue v1 = this.eval(pred, c, s0, cm2);\n\t\t\t  final IValue v2 = this.eval(pred, c, s1, cm2);\n\t\t\t  if (v1.equals(v2)) {\n\t\t\t\t  return s1;\n\t\t\t  }\n\t\t  }\n\t\t  // Move on to the next action in the ActionItemList.\n\t\t  acts = acts.cdr();\n\t\t  pred = acts.carPred();\n\t\t  c = acts.carContext();\n\t\t  kind = acts.carKind();\n          cm2 = acts.cm;\n\t  }\n\t  nss.addElement(s0, action, s1);\n\t  return s1.copy();\n  }\n\n  /* getNextStatesAppl */\n\n  @ExpectInlined\n  protected abstract TLCState getNextStatesAppl(final Action action, OpApplNode pred, ActionItemList acts, Context c,\n          TLCState s0, TLCState s1, INextStateFunctor nss, final CostModel cm);\n  \n  protected final TLCState getNextStatesApplImpl(final Action action, final OpApplNode pred, final ActionItemList acts, final Context c,\n                                           final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm) {\n        final ExprOrOpArgNode[] args = pred.getArgs();\n        final int alen = args.length;\n        final SymbolNode opNode = pred.getOperator();\n\n        int opcode = BuiltInOPs.getOpCode(opNode.getName());\n\n        if (opcode == 0) {\n          // This is a user-defined operator with one exception: it may\n          // be substed by a builtin operator. This special case occurs\n          // when the lookup returns an OpDef with opcode # 0.\n          Object val = this.lookup(opNode, c, s0, false);\n\n          if (val instanceof OpDefNode) {\n\t\t\t\tfinal OpDefNode opDef = (OpDefNode) val;\n\t\t\t\topcode = BuiltInOPs.getOpCode(opDef.getName());\n\t\t\t\tif (opcode == 0) {\n\t\t\t\t\treturn this.getNextStates(action, opDef.getBody(), acts, this.getOpContext(opDef, args, c, true, cm, toolId), s0, s1, nss, cm);\n\t            }\n          }\n\n          // Added by LL 13 Nov 2009 to fix Yuan\'s fix\n          /*********************************************************************\n           * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode    *\n           * imported with parameterized instantiation.                         *\n           *********************************************************************/\n          if (val instanceof ThmOrAssumpDefNode) {\n            final ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode)val;\n            return this.getNextStates(action, opDef.getBody(), acts, this.getOpContext(opDef, args, c, true), s0, s1, nss, cm);\n          }\n\n          if (val instanceof LazyValue) {\n            final LazyValue lv = (LazyValue)val;\n            if (lv.getValue() == null || lv.isUncachable()) {\n              return this.getNextStates(action, lv.expr, acts, lv.con, s0, s1, nss, lv.cm);\n            }\n            val = lv.getValue();\n          }\n\n          //TODO If all eval/apply in getNextStatesApplEvalAppl would be side-effect free (ie. not mutate args, c, s0,...), \n          // this call could be moved into the if(opcode==0) branch below. However, opcode!=0 will only be the case if\n          // OpDefNode above has been substed with a built-in operator. In other words, a user defines an operator Op1,\n          // and re-defines Op1 with a TLA+ built-in one in a TLC model (not assumed to be common). => No point in trying\n          // to move this call into if(opcode==0) because this will be the case most of the time anyway.\n          final Object bval = getNextStatesApplEvalAppl(alen, args, c, s0, s1, cm, val);\n\n\t      // opcode == 0 is a user-defined operator.\n          if (opcode == 0)\n          {\n            return getNextStatesApplUsrDefOp(action, pred, acts, s0, s1, nss, cm, bval);\n          }\n        }\n\n        return getNextStatesApplSwitch(action, pred, acts, c, s0, s1, nss, cm, args, alen, opcode);\n  }\n  \n  private final Object getNextStatesApplEvalAppl(final int alen, final ExprOrOpArgNode[] args, final Context c,\n\t\t\tfinal TLCState s0, final TLCState s1, final CostModel cm, final Object val) {\n\t      if (alen == 0) {\n        if (val instanceof MethodValue) {\n        \treturn ((MethodValue)val).apply(EmptyArgs, EvalControl.Clear);\n        } else if (val instanceof EvaluatingValue) {\n        \treturn ((EvaluatingValue)val).eval(this, args, c, s0, s1, EvalControl.Clear, cm);\n       }\n      }\n      else {\n        if (val instanceof OpValue) { // EvaluatingValue sub-class of OpValue!\n       \t  return ((OpValue) val).eval(this, args, c, s0, s1, EvalControl.Clear, cm);\n        }\n      }\n      return val;\n  }\n\n  private final TLCState getNextStatesApplUsrDefOp(final Action action, final OpApplNode pred, final ActionItemList acts, final TLCState s0,\n\t\tfinal TLCState s1, final INextStateFunctor nss, final CostModel cm, final Object bval) {\n\tif (!(bval instanceof BoolValue))\n\t{\n\t  Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "next states", "boolean",\n\t          bval.toString(), pred.toString() }, pred);\n\t}\n\tif (((BoolValue) bval).val)\n\t{\n\t  if (coverage) {\n\t\t  return this.getNextStates(action, acts, s0, s1, nss, cm);\n\t  } else {\n\t\t  return this.getNextStates0(action, acts, s0, s1, nss, cm);\n\t  }\n\t}\n\treturn s1;\n  }\n\n  private final TLCState getNextStatesApplSwitch(final Action action, final OpApplNode pred, final ActionItemList acts, final Context c, final TLCState s0,\n\t\tfinal TLCState s1, final INextStateFunctor nss, final CostModel cm, final ExprOrOpArgNode[] args, final int alen, final int opcode) {\n\tTLCState resState = s1;\n\tswitch (opcode) {\n\tcase OPCODE_cl:     // ConjList\n\tcase OPCODE_land:\n\t  {\n\t    ActionItemList acts1 = acts;\n\t    for (int i = alen - 1; i > 0; i--) {\n\t      acts1 = (ActionItemList) acts1.cons(args[i], c, cm, i);\n\t    }\n\t    return this.getNextStates(action, args[0], acts1, c, s0, s1, nss, cm);\n\t  }\n\tcase OPCODE_dl:     // DisjList\n\tcase OPCODE_lor:\n\t  {\n\t\tif (PROBABLISTIC) {\n\t\t\t// probabilistic (return after a state has been generated, ordered is randomized)\n\t\t\tfinal RandomGenerator rng = TLCGlobals.simulator.getRNG();\n\t\t\tint index = (int) Math.floor(rng.nextDouble() * alen);\n\t\t\tfinal int p = rng.nextPrime();\n\t\t    for (int i = 0; i < alen; i++) {\n\t\t\t      resState = this.getNextStates(action, args[index], acts, c, s0, resState, nss, cm);\n\t\t\t\t  if (nss.hasStates()) {\n\t\t\t\t\t\treturn resState;\n\t\t\t\t  }\n\t\t\t\t  index = (index + p) % alen;\n\t\t\t}\n\t\t} else {\n\t\t    for (int i = 0; i < alen; i++) {\n\t\t      resState = this.getNextStates(action, args[i], acts, c, s0, resState, nss, cm);\n\t\t    }\n\t\t}\n\t    return resState;\n\t  }\n\tcase OPCODE_be:     // BoundedExists\n\t  {\n\t    SemanticNode body = args[0];\n\t    \n\t    if (PROBABLISTIC) {\n\t\t    // probabilistic (return after a state has been generated, ordered is randomized)\n\t\t\tfinal ContextEnumerator Enum = this.contexts(Ordering.RANDOMIZED, pred, c, s0, s1, EvalControl.Clear, cm);\n\t\t\tContext c1;\n\t\t    while ((c1 = Enum.nextElement()) != null) {\n\t\t\t\tresState = this.getNextStates(action, body, acts, c1, s0, resState, nss, cm);\n\t\t\t\tif (nss.hasStates()) {\n\t\t\t\t\treturn resState;\n\t\t\t\t}\n\t\t    }\n\t    } else {\n\t    \t// non-deterministically generate successor states (potentially many)\n\t    \tContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Clear, cm);\n\t    \tContext c1;\n\t    \twhile ((c1 = Enum.nextElement()) != null) {\n\t    \t\tresState = this.getNextStates(action, body, acts, c1, s0, resState, nss, cm);\n\t    \t}\n\t    }\n\n\t    return resState;\n\t  }\n\tcase OPCODE_bf:     // BoundedForall\n\t  {\n\t    SemanticNode body = args[0];\n\t    ContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Clear, cm);\n\t    Context c1 = Enum.nextElement();\n\t    if (c1 == null) {\n\t      resState = this.getNextStates(action, acts, s0, s1, nss, cm);\n\t    }\n\t    else {\n\t      ActionItemList acts1 = acts;\n\t      Context c2;\n\t      while ((c2 = Enum.nextElement()) != null) {\n\t        acts1 = (ActionItemList) acts1.cons(body, c2, cm, IActionItemList.PRED);\n\t      }\n\t      resState = this.getNextStates(action, body, acts1, c1, s0, s1, nss, cm);\n\t    }\n\t    return resState;\n\t  }\n\tcase OPCODE_fa:     // FcnApply\n\t  {\n\t    Value fval = this.eval(args[0], c, s0, s1, EvalControl.KeepLazy, cm);\n\t    if (fval instanceof FcnLambdaValue) {\n\t      FcnLambdaValue fcn = (FcnLambdaValue)fval;\n\t      if (fcn.fcnRcd == null) {\n\t        Context c1 = this.getFcnContext(fcn, args, c, s0, s1, EvalControl.Clear, cm);\n\t        return this.getNextStates(action, fcn.body, acts, c1, s0, s1, nss, fcn.cm);\n\t      }\n\t      fval = fcn.fcnRcd;\n\t    }\n\t    if (!(fval instanceof Applicable)) {\n\t      Assert.fail("In computing next states, a non-function (" +\n\t                  fval.getKindString() + ") was applied as a function.\\n" + pred, pred, c);\n\t    }\n\t    Applicable fcn = (Applicable)fval;\n\t    Value argVal = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm);\n\t    Value bval = fcn.apply(argVal, EvalControl.Clear);\n\t    if (!(bval instanceof BoolValue)) {\n\t      Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "next states", "boolean",\n\t              pred.toString() }, args[1], c);\n\t    }\n\t    if (((BoolValue)bval).val) {\n\t      return this.getNextStates(action, acts, s0, s1, nss, cm);\n\t    }\n\t    return resState;\n\t  }\n\tcase OPCODE_aa:     // AngleAct <A>_e\n\t  {\n\t    ActionItemList acts1 = (ActionItemList) acts.cons(args[1], c, cm, IActionItemList.CHANGED);\n\t    return this.getNextStates(action, args[0], acts1, c, s0, s1, nss, cm);\n\t  }\n\tcase OPCODE_sa:     // [A]_e\n\t  {\n\t    /* The following two lines of code did not work, and were changed by\n\t     * YuanYu to mimic the way \\/ works.  Change made\n\t     *  11 Mar 2009, with LL sitting next to him.\n\t     */\n\t      //    this.getNextStates(action, args[0], acts, c, s0, s1, nss);\n\t      //    return this.processUnchanged(args[1], acts, c, s0, s1, nss);\n\t    resState = this.getNextStates(action, args[0], acts, c, s0, resState, nss, cm);\n\t    return this.processUnchanged(action, args[1], acts, c, s0, resState, nss, cm);\n\t  }\n\tcase OPCODE_ite:    // IfThenElse\n\t  {\n\t    Value guard = this.eval(args[0], c, s0, s1, EvalControl.Clear, cm);\n\t    if (!(guard instanceof BoolValue)) {\n\t      Assert.fail("In computing next states, a non-boolean expression (" +\n\t                  guard.getKindString() + ") was used as the condition of" +\n\t                  " an IF." + pred, pred, c);\n\t    }\n\t    if (((BoolValue)guard).val) {\n\t      return this.getNextStates(action, args[1], acts, c, s0, s1, nss, cm);\n\t    }\n\t    else {\n\t      return this.getNextStates(action, args[2], acts, c, s0, s1, nss, cm);\n\t    }\n\t  }\n\tcase OPCODE_case:   // Case\n\t  {\n\t    SemanticNode other = null;\n\t\tif (PROBABLISTIC) {\n\t\t\t// See Bounded exists above!\n\t\t\tthrow new UnsupportedOperationException(\n\t\t\t\t\t\t\t"Probabilistic evaluation of next-state relation not implemented for CASE yet.");\n\t\t}\n\t    for (int i = 0; i < alen; i++) {\n\t      OpApplNode pair = (OpApplNode)args[i];\n\t      ExprOrOpArgNode[] pairArgs = pair.getArgs();\n\t      if (pairArgs[0] == null) {\n\t        other = pairArgs[1];\n\t      }\n\t      else {\n\t        Value bval = this.eval(pairArgs[0], c, s0, s1, EvalControl.Clear, coverage ? cm.get(args[i]) : cm);\n\t        if (!(bval instanceof BoolValue)) {\n\t          Assert.fail("In computing next states, a non-boolean expression (" +\n\t                      bval.getKindString() + ") was used as a guard condition" +\n\t                      " of a CASE.\\n" + pairArgs[1], pairArgs[1], c);\n\t        }\n\t        if (((BoolValue)bval).val) {\n\t          return this.getNextStates(action, pairArgs[1], acts, c, s0, s1, nss, coverage ? cm.get(args[i]) : cm);\n\t        }\n\t      }\n\t    }\n\t    if (other == null) {\n\t      Assert.fail("In computing next states, TLC encountered a CASE with no" +\n\t                  " conditions true.\\n" + pred, pred, c);\n\t    }\n\t    return this.getNextStates(action, other, acts, c, s0, s1, nss, coverage ? cm.get(args[alen - 1]) : cm);\n\t  }\n\tcase OPCODE_eq:\n\t  {\n\t    SymbolNode var = this.getPrimedVar(args[0], c, false);\n\t    // Assert.check(var.getName().getVarLoc() >= 0);\n\t    if (var == null) {\n\t      Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm);\n\t      if (!((BoolValue)bval).val) {\n\t        return resState;\n\t      }\n\t    }\n\t    else {\n\t      UniqueString varName = var.getName();\n\t      IValue lval = s1.lookup(varName);\n\t      Value rval = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm);\n\t      if (lval == null) {\n\t        resState.bind(varName, rval);\n\t        resState = this.getNextStates(action, acts, s0, resState, nss, cm);\n\t        resState.unbind(varName);\n\t        return resState;\n\t      }\n\t      else if (!lval.equals(rval)) {\n\t        return resState;\n\t      }\n\t    }\n\t    return this.getNextStates(action, acts, s0, s1, nss, cm);\n\t  }\n\tcase OPCODE_in:\n\t  {\n\t    SymbolNode var = this.getPrimedVar(args[0], c, false);\n\t    // Assert.check(var.getName().getVarLoc() >= 0);\n\t    if (var == null) {\n\t      Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm);\n\t      if (!((BoolValue)bval).val) {\n\t        return resState;\n\t      }\n\t    }\n\t    else {\n\t      UniqueString varName = var.getName();\n\t      Value lval = (Value) s1.lookup(varName);\n\t      Value rval = this.eval(args[1], c, s0, s1, EvalControl.Clear, cm);\n\t      if (lval == null) {\n\t        if (!(rval instanceof Enumerable)) {\n\t          Assert.fail("In computing next states, the right side of \\\\IN" +\n\t                      " is not enumerable.\\n" + pred, pred, c);\n\t        }\n\t        \n\t\t\tif (PROBABLISTIC) {\n\t\t\t\tfinal ValueEnumeration Enum = ((Enumerable)rval).elements(Ordering.RANDOMIZED);\n\t\t\t\tValue elem;\n\t\t\t    while ((elem = Enum.nextElement()) != null) {\n\t\t\t        resState.bind(varName, elem);\n\t\t\t        resState = this.getNextStates(action, acts, s0, resState, nss, cm);\n\t\t\t        resState.unbind(varName);\n\t\t\t\t\tif (nss.hasStates()) {\n\t\t\t\t\t\treturn resState;\n\t\t\t\t\t}\n\t\t\t    }\n\t\t\t}\n\n\t        ValueEnumeration Enum = ((Enumerable)rval).elements();\n\t        Value elem;\n\t        while ((elem = Enum.nextElement()) != null) {\n\t          resState.bind(varName, elem);\n\t          resState = this.getNextStates(action, acts, s0, resState, nss, cm);\n\t          resState.unbind(varName);\n\t        }\n\t        return resState;\n\t      }\n\t      else if (!rval.member(lval)) {\n\t        return resState;\n\t      }\n\t    }\n\t    return this.getNextStates(action, acts, s0, s1, nss, cm);\n\t  }\n\tcase OPCODE_implies:\n\t  {\n\t    Value bval = this.eval(args[0], c, s0, s1, EvalControl.Clear, cm);\n\t    if (!(bval instanceof BoolValue)) {\n\t      Assert.fail("In computing next states of a predicate of the form" +\n\t                  " P => Q, P was\\n" + bval.getKindString() + ".\\n" + pred, pred, c);\n\t    }\n\t    if (((BoolValue)bval).val) {\n\t      return this.getNextStates(action, args[1], acts, c, s0, s1, nss, cm);\n\t    }\n\t    else {\n\t      return this.getNextStates(action, acts, s0, s1, nss, cm);\n\t    }\n\t  }\n\tcase OPCODE_unchanged:\n\t  {\n\t    return this.processUnchanged(action, args[0], acts, c, s0, s1, nss, cm);\n\t  }\n\tcase OPCODE_cdot:\n\t  {\n\t    Assert.fail("The current version of TLC does not support action composition.", pred, c);\n\t    /***\n\t    TLCState s01 = TLCStateFun.Empty;\n\t    StateVec iss = new StateVec(0);\n\t    this.getNextStates(action, args[0], ActionItemList.Empty, c, s0, s01, iss);\n\t    int sz = iss.size();\n\t    for (int i = 0; i < sz; i++) {\n\t      s01 = iss.elementAt(i);\n\t      this.getNextStates(action, args[1], acts, c, s01, s1, nss);\n\t    }\n\t    ***/\n\t    return s1;\n\t  }\n\t// The following case added by LL on 13 Nov 2009 to handle subexpression names.\n\tcase OPCODE_nop:\n\t{\n\t    return this.getNextStates(action, args[0], acts, c, s0, s1, nss, cm);\n\t}\n\tdefault:\n\t  {\n\t    // We handle all the other builtin operators here.\n\t    Value bval = this.eval(pred, c, s0, s1, EvalControl.Clear, cm);\n\t    if (!(bval instanceof BoolValue)) {\n\t      Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "next states", "boolean",\n\t              bval.toString(), pred.toString() }, pred, c);\n\t    }\n\t    if (((BoolValue)bval).val) {\n\t      resState = this.getNextStates(action, acts, s0, s1, nss, cm);\n\t    }\n\t    return resState;\n\t  }\n\t}\n  }\n  \n  /* processUnchanged */\n\n  @ExpectInlined\n  protected abstract TLCState processUnchanged(final Action action, SemanticNode expr, ActionItemList acts, Context c,\n                                          TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm);\n  \n  protected final TLCState processUnchangedImpl(final Action action, SemanticNode expr, ActionItemList acts, Context c,\n          TLCState s0, TLCState s1, INextStateFunctor nss, CostModel cm) {\n    if (coverage){cm = cm.get(expr);}\n        SymbolNode var = this.getVar(expr, c, false, toolId);\n        TLCState resState = s1;\n        if (var != null) {\n            return processUnchangedImplVar(action, expr, acts, s0, s1, nss, var, cm);\n        }\n\n        if (expr instanceof OpApplNode) {\n          OpApplNode expr1 = (OpApplNode)expr;\n          ExprOrOpArgNode[] args = expr1.getArgs();\n          int alen = args.length;\n          SymbolNode opNode = expr1.getOperator();\n          UniqueString opName = opNode.getName();\n          int opcode = BuiltInOPs.getOpCode(opName);\n\n          if (opcode == OPCODE_tup) {\n            return processUnchangedImplTuple(action, acts, c, s0, s1, nss, args, alen, cm, coverage ? cm.get(expr1) : cm);\n          }\n\n          if (opcode == 0 && alen == 0) {\n            // a 0-arity operator:\n            return processUnchangedImpl0Arity(action, expr, acts, c, s0, s1, nss, cm, opNode, opName);\n          }\n        }\n\n        return verifyUnchanged(action, expr, acts, c, s0, s1, nss, cm);\n  }\n\n  @ExpectInlined\n  private final TLCState processUnchangedImpl0Arity(final Action action, final SemanticNode expr, final ActionItemList acts,\n\t\t\tfinal Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss, final CostModel cm,\n\t\t\tfinal SymbolNode opNode, final UniqueString opName) {\n\t\tfinal Object val = this.lookup(opNode, c, false);\n\t\n\t\tif (val instanceof OpDefNode) {\n\t\t  return this.processUnchanged(action, ((OpDefNode)val).getBody(), acts, c, s0, s1, nss, cm);\n\t\t}\n\t\telse if (val instanceof LazyValue) {\n\t\t  final LazyValue lv = (LazyValue)val;\n\t\t  return this.processUnchanged(action, lv.expr, acts, lv.con, s0, s1, nss, cm);\n\t\t}\n        return verifyUnchanged(action, expr, acts, c, s0, s1, nss, cm);\n  }\n\n  /**\n   * Check that <code>expr</code> is unchanged without attempting to synthesize values for variables in the\n   * successor state.\n   */\n  private TLCState verifyUnchanged(final Action action, final SemanticNode expr, final ActionItemList acts,\n                                   final Context c, final TLCState s0, final TLCState s1, final INextStateFunctor nss,\n                                   final CostModel cm) {\n      TLCState resState = s1;\n      IValue v0 = this.eval(expr, c, s0, cm);\n      IValue v1 = this.eval(expr, c, s1, TLCState.Null, EvalControl.Clear, cm);\n      if (v0.equals(v1)) {\n          resState = this.getNextStates(action, acts, s0, s1, nss, cm);\n      }\n      return resState;\n  }\n\n  @Override\n  public IValue eval(SemanticNode expr, Context c, TLCState s0) {\n\t    return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, CostModel.DO_NOT_RECORD);\n\t  }\n\n  @Override\n  public IValue eval(SemanticNode expr, Context c) {\n\t    return this.eval(expr, c, TLCState.Empty);\n\t  }\n\n  @Override\n  public IValue eval(SemanticNode expr) {\n\t    return this.eval(expr, Context.Empty);\n\t  }\n\n  @ExpectInlined\n  private final TLCState processUnchangedImplTuple(final Action action, ActionItemList acts, Context c, TLCState s0, TLCState s1, INextStateFunctor nss,\n  \t\tExprOrOpArgNode[] args, int alen, CostModel cm, CostModel cmNested) {\n  \t// a tuple:\n  \tif (alen != 0) {\n  \t  ActionItemList acts1 = acts;\n  \t  for (int i = alen-1; i > 0; i--) {\n  \t    acts1 = (ActionItemList) acts1.cons(args[i], c, cmNested, IActionItemList.UNCHANGED);\n  \t  }\n  \t  return this.processUnchanged(action, args[0], acts1, c, s0, s1, nss, cmNested);\n  \t}\n  \treturn this.getNextStates(action, acts, s0, s1, nss, cm);\n  }\n  \n  @ExpectInlined\n  private final TLCState processUnchangedImplVar(final Action action, SemanticNode expr, ActionItemList acts, TLCState s0, TLCState s1, INextStateFunctor nss,\n  \t\tSymbolNode var, final CostModel cm) {\n          TLCState resState = s1;\n          // expr is a state variable:\n          final UniqueString varName = var.getName();\n          final IValue val0 = s0.lookup(varName);\n          final IValue val1 = s1.lookup(varName);\n          if (val1 == null) {\n\t\t  \tresState.bind(varName, val0);\n            if (coverage) {\n            \tresState = this.getNextStates(action, acts, s0, resState, nss, cm);\n            } else {\n            \tresState = this.getNextStates0(action, acts, s0, resState, nss, cm);\n            }\n\t\t  \tresState.unbind(varName);\n          }\n          else if (val0.equals(val1)) {\n              if (coverage) {\n                  resState = this.getNextStates(action, acts, s0, s1, nss, cm);\n              } else {\n                  resState = this.getNextStates0(action, acts, s0, s1, nss, cm);\n              }\n          }\n          else {\n        \t  MP.printWarning(EC.TLC_UNCHANGED_VARIABLE_CHANGED, new String[]{varName.toString(), expr.toString()});\n          }\n          return resState;\n  }\n    \n  /* eval */\n  public TLCState evalAlias(TLCState current, TLCState successor) {\n\t\tif ("".equals(this.config.getAlias())) {\n\t\t\treturn current;\n\t\t}\n\t\t// see getState(..)\n\t\tIdThread.setCurrentState(current);\n\t\t\n\t\t// See asserts in tlc2.debug.TLCActionStackFrame.TLCActionStackFrame(TLCStackFrame, SemanticNode, Context, Tool, TLCState, Action, TLCState, RuntimeException)\n\t\tif (successor.getLevel() != current.getLevel()) {\n\t\t\t// Calling setPrecessor when the levels are equal would increase the level of\n\t\t\t// successor.\n\t\t\tsuccessor.setPredecessor(current);\n\t\t}\n\n\t\ttry {\n\t\t\tfinal TLCState alias = eval(getAliasSpec(), Context.Empty, current, successor, EvalControl.Clear).toState();\n\t\t\tif (alias != null) {\n\t\t\t\treturn alias;\n\t\t\t}\n\t\t} catch (EvalException | TLCRuntimeException e) {\n\t\t\t// Fall back to original state if eval fails.\n\t\t\treturn current;\n\t\t}\n\t\t\n\t\treturn current;\n  }\n\n  \t@Override\n\tpublic TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor) {\n\t\tif (!hasAlias()) {\n\t\t\treturn current;\n\t\t}\n\t\treturn evalAlias(current, successor, Context.Empty);\n\t}\n\n  \t@Override\n\tpublic TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor, Supplier<List<TLCStateInfo>> prefix) {\n\t\tif (!hasAlias()) {\n\t\t\treturn current;\n\t\t}\n\n\t\tfinal ExternalModuleTable emt = getSpecProcessor().getSpecObj().getExternalModuleTable();\n\t\tfinal tla2sany.semantic.Context tlcExt = emt.getContext(UniqueString.of("TLCExt"));\n\t\tif (tlcExt == null) {\n\t\t\t// tlcExt is null if the TLCExt module is not extended or instantiated.  Thus,\n\t\t\t// Trace cannot appear in the spec.\n\t\t\treturn evalAlias(current, successor, Context.Empty);\n\t\t}\n\t\tfinal SymbolNode tlcExtTrace = tlcExt.getSymbol(UniqueString.of("Trace"));\n\t\t\n\t\treturn evalAlias(current, successor,\n\t\t\t\tContext.Empty.cons(tlcExtTrace, new LazySupplierValue(tlcExtTrace, (Supplier<Value>) () -> {\n\t\t\t\t\treturn new TupleValue(\n\t\t\t\t\t\t\tprefix.get().stream().map(si -> new RecordValue(si.state)).toArray(Value[]::new));\n\t\t\t\t})));\n\t}\n\n  private TLCStateInfo evalAlias(TLCStateInfo current, TLCState successor, Context ctxt) {\n\n\t\t// see getState(..)\n\t\tIdThread.setCurrentState(current.state);\n\n\t\t// See asserts in\n\t\t// tlc2.debug.TLCActionStackFrame.TLCActionStackFrame(TLCStackFrame,\n\t\t// SemanticNode, Context, Tool, TLCState, Action, TLCState, RuntimeException)\n\t\tif (successor.getLevel() != current.state.getLevel()) {\n\t\t\t// Calling setPrecessor when the levels are equal would increase the level of\n\t\t\t// successor.\n\t\t\tsuccessor.setPredecessor(current);\n\t\t}\n\n\t\ttry {\n\t\t\tfinal TLCState alias = eval(getAliasSpec(), ctxt, current.state, successor, EvalControl.Clear).toState();\n\t\t\tif (alias != null) {\n\t\t\t\treturn new AliasTLCStateInfo(alias, current);\n\t\t\t}\n\t\t} catch (EvalException | TLCRuntimeException e) {\n\t\t\t// Fall back to original state if eval fails.\n\t\t\treturn current;\n\t\t\t// TODO We have to somehow communicate this exception back to the user.\n\t\t\t// Unfortunately, the alias cannot be validated by SpecProcess (unless pure\n\t\t\t// constant expression who are too simple to be used in trace expressions).\n\t\t\t// Throwing the exception would be possible, but pretty annoying if TLC fails\n\t\t\t// to print an error trace because of a bogus alias after hours of model\n\t\t\t// checking (this is the very reason why the code falls back to return the \n\t\t\t// original/current state).  Printing the exception to stdout/stderr here\n\t\t\t// would mess with the Toolbox\'s parsing that reads stdout back in.  It would\n\t\t\t// also look bad because we would print the error on every evaluation of the\n\t\t\t// alias and it\'s conceivable that -in most cases- evaluation would fail for\n\t\t\t// all evaluations.  This suggests that we have to defer reporting of evaluation\n\t\t\t// and runtime exception until after the error-trace has been printed. If\n\t\t\t// evaluation only failed for some invocations of evalAlias, the user will\n\t\t\t// be able to figure out the ones that failed by looking at the trace.  This\n\t\t\t// state should not be kept in Tool, because it doesn\'t know how to group\n\t\t\t// sequences of evalAlias invocations.\n\t\t\t// We could avoid keeping state entirely, if the exception was attached as an\n\t\t\t// "auxiliary" variable to the TLCStateInfo and printed as part of the error\n\t\t\t// trace.  The error trace would look strange, but it appears to be the best\n\t\t\t// compromise, especially if only some of the evaluations fail.\n\t\t}\n\t\t\n\t\treturn current;\n  }\n  \n  /* Special version of eval for state expressions. */\n  @Override\n  public IValue eval(SemanticNode expr, Context c, TLCState s0, CostModel cm) {\n    return this.eval(expr, c, s0, TLCState.Empty, EvalControl.Clear, cm);\n  }\n  \n\t  @Override\n\tpublic final IValue eval(SemanticNode expr, Context c, TLCState s0,\n              TLCState s1, final int control) {\n\t\t  return eval(expr, c, s0, s1, control, CostModel.DO_NOT_RECORD);\n\t  }\n\t  \n\tpublic Value evalPure(final OpDefNode opDef, final ExprOrOpArgNode[] args, final Context c, final TLCState s0,\n\t\t\t\tfinal TLCState s1, final int control, final CostModel cm) {\n\t    final Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId);\n\t\treturn this.eval(opDef.getBody(), c1, s0, s1, control, cm);\n\t}\n\n  /*\n   * This method evaluates the expression expr in the given context,\n   * current state, and partial next state.\n   */\n  public abstract Value eval(SemanticNode expr, Context c, TLCState s0,\n                          TLCState s1, final int control, final CostModel cm);\n  \n  @ExpectInlined\n  protected Value evalImpl(final SemanticNode expr, final Context c, final TLCState s0,\n          final TLCState s1, final int control, CostModel cm) {\n        switch (expr.getKind()) {\n        /***********************************************************************\n        * LabelKind class added by LL on 13 Jun 2007.                          *\n        ***********************************************************************/\n        case LabelKind:\n          {\n            LabelNode expr1 = (LabelNode) expr;\n            return this.eval(expr1.getBody(), c, s0, s1, control, cm);\n          }\n        case OpApplKind:\n          {\n            OpApplNode expr1 = (OpApplNode)expr;\n            if (coverage) {cm = cm.get(expr);}\n            return this.evalAppl(expr1, c, s0, s1, control, cm);\n          }\n        case LetInKind:\n          {\n            return evalImplLetInKind((LetInNode) expr, c, s0, s1, control, cm);\n          }\n        case SubstInKind:\n          {\n            return evalImplSubstInKind((SubstInNode) expr, c, s0, s1, control, cm);\n          }\n        // Added by LL on 13 Nov 2009 to handle theorem and assumption names.\n        case APSubstInKind:\n          {\n            return evalImplApSubstInKind((APSubstInNode) expr, c, s0, s1, control, cm);\n          }\n        case NumeralKind:\n        case DecimalKind:\n        case StringKind:\n          {\n            return (Value) WorkerValue.mux(expr.getToolObject(toolId));\n          }\n        case AtNodeKind:\n          {\n            return (Value)c.lookup(EXCEPT_AT);\n          }\n        case OpArgKind:\n          {\n            return evalImplOpArgKind((OpArgNode) expr, c, s0, s1, cm);\n          }\n        default:\n          {\n            Assert.fail("Attempted to evaluate an expression that cannot be evaluated.\\n" +\n                        expr, expr, c);\n            return null;     // make compiler happy\n          }\n        }\n  }\n\n  @ExpectInlined\n  private final Value evalImplLetInKind(LetInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) {\n\tOpDefNode[] letDefs = expr1.getLets();\n\tint letLen = letDefs.length;\n\tContext c1 = c;\n\tfor (int i = 0; i < letLen; i++) {\n\t  OpDefNode opDef = letDefs[i];\n\t  if (opDef.getArity() == 0) {\n\t    Value rhs = new LazyValue(opDef.getBody(), c1, cm);\n\t    c1 = c1.cons(opDef, rhs);\n\t  }\n\t}\n\treturn this.eval(expr1.getBody(), c1, s0, s1, control, cm);\n  }\n\n  @ExpectInlined\n  private final Value evalImplSubstInKind(SubstInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) {\n  \tSubst[] subs = expr1.getSubsts();\n  \tint slen = subs.length;\n  \tContext c1 = c;\n  \tfor (int i = 0; i < slen; i++) {\n  \t  Subst sub = subs[i];\n  \t  c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, true, coverage ? sub.getCM() : cm, toolId));\n  \t}\n  \treturn this.eval(expr1.getBody(), c1, s0, s1, control, cm);\n  }\n    \n  @ExpectInlined\n  private final Value evalImplApSubstInKind(APSubstInNode expr1, Context c, TLCState s0, TLCState s1, final int control, final CostModel cm) {\n  \tSubst[] subs = expr1.getSubsts();\n  \tint slen = subs.length;\n  \tContext c1 = c;\n  \tfor (int i = 0; i < slen; i++) {\n  \t  Subst sub = subs[i];\n  \t  c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, true, cm, toolId));\n  \t}\n  \treturn this.eval(expr1.getBody(), c1, s0, s1, control, cm);\n  }\n  \n  @ExpectInlined\n  private final Value evalImplOpArgKind(OpArgNode expr1, Context c, TLCState s0, TLCState s1, final CostModel cm) {\n  \tSymbolNode opNode = expr1.getOp();\n  \tObject val = this.lookup(opNode, c, false);\n  \tif (val instanceof OpDefNode) {\n  \t  return setSource(expr1, new OpLambdaValue((OpDefNode)val, this, c, s0, s1, cm));\n  \t}\n  \treturn (Value)val;\n  }\n  \n  /* evalAppl */\n  \n  @ExpectInlined\n  protected abstract Value evalAppl(final OpApplNode expr, Context c, TLCState s0,\n          TLCState s1, final int control, final CostModel cm);\n\n  protected final Value evalApplImpl(final OpApplNode expr, Context c, TLCState s0,\n                              TLCState s1, final int control, CostModel cm) {\n    if (coverage){\n    \tcm = cm.getAndIncrement(expr);\n    }\n        ExprOrOpArgNode[] args = expr.getArgs();\n        SymbolNode opNode = expr.getOperator();\n        int opcode = BuiltInOPs.getOpCode(opNode.getName());\n\n        if (opcode == 0) {\n          // This is a user-defined operator with one exception: it may\n          // be substed by a builtin operator. This special case occurs\n          // when the lookup returns an OpDef with opcode # 0.\n          Object val = this.lookup(opNode, c, s0, EvalControl.isPrimed(control));\n\n//          if (val instanceof Supplier) {\n//        \t  val = ((Supplier) val).get();\n//          }\n          \n          // First, unlazy if it is a lazy value. We cannot use the cached\n          // value when s1 == null or isEnabled(control).\n\t\t\tif (val instanceof LazyValue) {\n\t\t\t\tfinal LazyValue lv = (LazyValue) val;\n\t\t\t\tif (s1 == null) {\n\t\t\t\t\tval = this.eval(lv.expr, lv.con, s0, TLCState.Null, control, lv.getCostModel());\n\t\t\t    } else if (lv.isUncachable() || EvalControl.isEnabled(control)) {\n\t\t\t\t\t// Never use cached LazyValues in an ENABLED expression. This is why all\n\t\t\t\t\t// this.enabled* methods pass EvalControl.Enabled (the only exception being the\n\t\t\t\t\t// call on line line 2799 which passes EvalControl.Primed). This is why we can\n\t\t\t    \t// be sure that ENALBED expressions are not affected by the caching bug tracked\n\t\t\t    \t// in Github issue 113 (see below).\n\t\t\t\t\tval = this.eval(lv.expr, lv.con, s0, s1, control, lv.getCostModel());\n\t\t\t\t} else {\n\t\t\t\t\tval = lv.getValue();\n\t\t\t\t\tif (val == null) {\n\t\t\t\t\t\tfinal Value res = this.eval(lv.expr, lv.con, s0, s1, control, lv.getCostModel());\n\t\t\t\t\t\t// This check has been suggested by Yuan Yu on 01/15/2018:\n\t\t\t\t\t\t//\n\t\t\t\t\t\t// If init-states are being generated, level has to be <= ConstantLevel for\n\t\t\t\t\t\t// caching/LazyValue to be allowed. If next-states are being generated, level\n\t\t\t\t\t\t// has to be <= VariableLevel. The level indicates if the expression to be\n\t\t\t\t\t\t// evaluated contains only constants, constants & variables, constants & \n\t\t\t\t\t\t// variables and primed variables (thus action) or is a temporal formula.\n\t\t\t\t\t\t//\n\t\t\t\t\t\t// This restriction is in place to fix Github issue 113\n\t\t\t\t\t\t// (https://github.com/tlaplus/tlaplus/issues/113) - \n\t\t\t\t\t\t// TLC can generate invalid sets of init or next-states caused by broken\n\t\t\t\t\t\t// LazyValue evaluation. The related tests are AssignmentInit* and\n\t\t\t\t\t\t// AssignmentNext*. Without this fix TLC essentially reuses a stale lv.val when\n\t\t\t\t\t\t// it needs to re-evaluate res because the actual operands to eval changed.\n\t\t\t\t\t\t// Below is Leslie\'s formal description of the bug:\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// The possible initial values of some variable  var  are specified by a subformula\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// F(..., var, ...)\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// in the initial predicate, for some operator F such that expanding the\n\t\t\t\t\t\t// definition of F results in a formula containing more than one occurrence of\n\t\t\t\t\t\t// var , not all occurring in separate disjuncts of that formula.\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// The possible next values of some variable  var  are specified by a subformula\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// F(..., var\', ...)\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// in the next-state relation, for some operator F such that expanding the\n\t\t\t\t\t\t// definition of F results in a formula containing more than one occurrence of\n\t\t\t\t\t\t// var\' , not all occurring in separate disjuncts of that formula.\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// An example of the first case is an initial predicate  Init  defined as follows:\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// VARIABLES x, ...\n\t\t\t\t\t\t// F(var) == \\/ var \\in 0..99 /\\ var % 2 = 0\n\t\t\t\t\t\t//           \\/ var = -1\n\t\t\t\t\t\t// Init == /\\ F(x)\n\t\t\t\t\t\t//         /\\ ...\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// The error would not appear if  F  were defined by:\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// F(var) == \\/ var \\in {i \\in 0..99 : i % 2 = 0}\n\t\t\t\t\t\t//           \\/ var = -1\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// or if the definition of  F(x)  were expanded in  Init :\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// Init == /\\ \\/ x \\in 0..99 /\\ x % 2 = 0\n\t\t\t\t\t\t//            \\/ x = -1\n\t\t\t\t\t\t//         /\\ ...\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// A similar example holds for case 2 with the same operator F and the\n\t\t\t\t\t\t// next-state formula\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// Next == /\\ F(x\')\n\t\t\t\t\t\t//         /\\ ...\n\t\t\t\t\t\t// \n\t\t\t\t\t\t// The workaround is to rewrite the initial predicate or next-state relation so\n\t\t\t\t\t\t// it is not in the form that can cause the bug. The simplest way to do that is\n\t\t\t\t\t\t// to expand (in-line) the definition of F in the definition of the initial\n\t\t\t\t\t\t// predicate or next-state relation.\n\t\t\t\t\t\t//\n\t\t\t\t\t\t// Note that EvalControl.Init is only set in the scope of this.getInitStates*,\n\t\t\t\t\t\t// but not in the scope of methods such as this.isInModel, this.isGoodState...\n\t\t\t\t\t\t// which are invoked by DFIDChecker and ModelChecker#doInit and doNext. These\n\t\t\t\t\t\t// invocation however don\'t pose a problem with regards to issue 113 because\n\t\t\t\t\t\t// they don\'t generate the set of initial or next states but get passed fully\n\t\t\t\t\t\t// generated/final states.\n\t\t\t\t\t\t//\n\t\t\t\t\t\t// !EvalControl.isInit(control) means Tool is either processing the spec in\n\t\t\t\t\t\t// this.process* as part of initialization or that next-states are being\n\t\t\t\t\t\t// generated. The latter case has to restrict usage of cached LazyValue as\n\t\t\t\t\t\t// discussed above.\n\t\t\t\t\t\tfinal int level = ((LevelNode) lv.expr).getLevel(); // cast to LevelNode is safe because LV only subclass of SN.\n\t\t\t\t\t\tif ((EvalControl.isInit(control) && level <= LevelConstants.ConstantLevel)\n\t\t\t\t\t\t\t\t|| (!EvalControl.isInit(control) && level <= LevelConstants.VariableLevel)) {\n\t\t\t\t\t\t\t// The performance benefits of caching values is generally debatable. The time\n\t\t\t\t\t\t\t// it takes TLC to check a reasonable sized model of the PaxosCommit [1] spec is\n\t\t\t\t\t\t\t// ~2h with, with limited caching due to the fix for issue 113 or without\n\t\t\t\t\t\t\t// caching. There is no measurable performance difference even though the change\n\t\t\t\t\t\t\t// for issue 113 reduces the cache hits from ~13 billion to ~4 billion. This was\n\t\t\t\t\t\t\t// measured with an instrumented version of TLC.\n\t\t\t\t\t\t\t// [1] general/performance/PaxosCommit/  \n\t\t\t\t\t\t\tlv.setValue(res);\n\t\t\t\t\t\t}\n\t\t\t\t\t\tval = res;\n\t\t\t\t\t}\n\t\t\t\t}\n\n\t\t\t}\n\n\t\t\tValue res = null;\n          if (val instanceof OpDefNode) {\n            OpDefNode opDef = (OpDefNode)val;\n            opcode = BuiltInOPs.getOpCode(opDef.getName());\n            if (opcode == 0) {\n              Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId);\n              res = this.eval(opDef.getBody(), c1, s0, s1, control, cm);\n            }\n          }\n          else if (val instanceof Value) {\n            res = (Value)val;\n            int alen = args.length;\n            if (alen == 0) {\n              if (val instanceof MethodValue) {\n                res = ((MethodValue)val).apply(EmptyArgs, EvalControl.Clear);\n              } else if (val instanceof EvaluatingValue) {\n            \t  // Allow EvaluatingValue overwrites to have zero arity.\n            \t  res = ((EvaluatingValue) val).eval(this, args, c, s0, s1, control, cm);\n              }\n            }\n            else {\n              if (val instanceof OpValue) {\n            \t  res = ((OpValue) val).eval(this, args, c, s0, s1, control, cm);\n               } \n            }\n          }\n          /*********************************************************************\n          * The following added by Yuan Yu on 13 Nov 2009 to allow theorem an  *\n          * assumption names to be used as expressions.                        *\n          *                                                                    *\n          * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode    *\n          * imported with parameterized instantiation.                         *\n          *********************************************************************/\n          else if (val instanceof ThmOrAssumpDefNode) {\n//            Assert.fail("Trying to evaluate the theorem or assumption name `"\n//                         + opNode.getName() + "\'. \\nUse `" + opNode.getName()\n//                         + "!:\' instead.\\n" +expr);\n            ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode) val ;\n            Context c1 = this.getOpContext(opDef, args, c, true);\n            return this.eval(opDef.getBody(), c1, s0, s1, control, cm);\n          }\n          else {\n\t\t\t\tif (!EvalControl.isEnabled(control) && EvalControl.isPrimed(control) && opNode instanceof OpDeclNode) {\n\t\t\t\t\t// We end up here if fairness is declared on a sub-action that doesn\'t define\n\t\t\t\t\t// the value of all variables given in the subscript vars (state pred) part of\n\t\t\t\t\t// the (weak or strong) fairness operator:\n\t\t\t\t\t// \n\t\t\t\t\t// VARIABLES a,b            \\* opNode is b up here.\n\t\t\t\t\t// vars == <<a,b>>\n\t\t\t\t\t// A == a\' = 42\n\t\t\t\t\t// Next == A /\\ b = b\' \\* Do something with b.\n\t\t\t\t\t// Spec == ... /\\ WF_vars(A)\n\t\t\t\t\t//\n\t\t\t\t\t// Variants:\n\t\t\t\t\t//        /\\ WF_b(TRUE)\n\t\t\t\t\t//        /\\ WF_vars(TRUE)\n\t\t\t\t\t//\n\t\t\t\t\t// This variant is debatable. It triggers the "generic" exception below:\n\t\t\t\t\t//        /\\ WF_vars(a\' = b\')\n\t\t\t\t\t//\n\t\t\t\t\t// For larger specs, this is obviously difficult to debug. Especially, \n\t\t\t\t\t// because opNode usually points to b on the vars == <<...>> line.\n\t\t\t\t\t//\n\t\t\t\t\t// The following issues confirm that even seasoned users run into this:\n\t\t\t\t\t// https://github.com/tlaplus/tlaplus/issues/317\n\t\t\t\t\t// https://github.com/tlaplus/tlaplus/issues/618\n\t\t\t\t\t// http://discuss.tlapl.us/msg03840.html\n\t\t\t\t\tAssert.fail(EC.TLC_STATE_NOT_COMPLETELY_SPECIFIED_LIVE,\n\t\t\t\t\t\t\tnew String[] { opNode.getName().toString(), expr.toString() }, expr, c);\n\t\t\t\t\t// Assert#fail throws exception, thus, no need for an else.\n\t\t\t\t}\n\t\t\t\t// EV#Enabled /\\ EV#Prime /\\ OpDeclNode is the case when A is an action (a boolean\n\t\t\t\t// valued transition function (see page 312 in Specifying Systems) appearing in an\n\t\t\t\t// invariant that TLC cannot evaluate. E.g.:\n        \t  \t// \n\t      \t    // Spec == Init /\\ [][a\' = a + 1]_a\n        \t    // Inv == ENABLED a\' > a\n        \t    // \n\t\t\t\t// -----------\n\t\t\t\t// EV#Clear /\\ OpDeclNode is the case when A is an action that TLC\n\t\t\t\t// cannot evaluate. E.g.:\n\t      \t  \t// \n\t      \t    // Spec == Init /\\ [][a\' > a]_a\n\t      \t    // \n\t            Assert.fail(EC.TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR,\n                new String[] { opNode.getName().toString(), expr.toString() }, expr, c);\n          }\n          if (opcode == 0) {\n            return res;\n          }\n        }\n\n        switch (opcode) {\n        case OPCODE_bc:     // BoundedChoose\n          {\n            SemanticNode pred = args[0];\n            SemanticNode inExpr = expr.getBdedQuantBounds()[0];\n            Value inVal = this.eval(inExpr, c, s0, s1, control, cm);\n            if (!(inVal instanceof Enumerable)) {\n              Assert.fail("Attempted to compute the value of an expression of\\n" +\n                          "form CHOOSE x \\\\in S: P, but S was not enumerable.\\n" + expr, expr, c);\n            }\n\n            // To fix Bugzilla Bug 279 : TLC bug caused by TLC\'s not preserving the semantics of CHOOSE\n            // (@see tlc2.tool.BugzillaBug279Test),\n            // the statement\n            //\n            //    inVal.normalize();\n            //\n            // was replaced by the following by LL on 7 Mar 2012.  This fix has not yet received\n            // the blessing of Yuan Yu, so it should be considered to be provisional.\n            // \n            //     Value convertedVal = inVal.ToSetEnum();\n            //       if (convertedVal != null) {\n            //         inVal = convertedVal;\n            //       } else {\n            //         inVal.normalize();\n            //     }\n            // end of fix.\n            \n            // MAK 09/22/2018:\n\t\t\t// The old fix above has the undesired side effect of enumerating inVal. In\n\t\t\t// other words, e.g. a SUBSET 1..8 would be enumerated and normalized into a\n\t\t\t// SetEnumValue. This is expensive and especially overkill, if the CHOOSE\n\t\t\t// predicate holds for most if not all elements of inVal. In this case, we\n            // don\'t want to fully enumerate inVal but instead return the first element\n\t\t\t// obtained from Enumerable#elements for which the predicate holds. Thus,\n\t\t\t// Enumerable#elements(Ordering) has been added by which we make the requirement\n\t\t\t// for elements to be normalized explicit. Implementor of Enumerable, such as\n\t\t\t// SubsetValue are then free to implement elements that returns elements in\n\t\t\t// normalized order without converting SubsetValue into SetEnumValue first.\n            \n            inVal.normalize();\n\n            ValueEnumeration enumSet = ((Enumerable)inVal).elements(Enumerable.Ordering.NORMALIZED);\n            FormalParamNode[] bvars = expr.getBdedQuantSymbolLists()[0];\n            boolean isTuple = expr.isBdedQuantATuple()[0];\n            if (isTuple) {\n              // Identifier tuple case:\n              int cnt = bvars.length;\n              Value val;\n              while ((val = enumSet.nextElement()) != null) {\n                TupleValue tv = (TupleValue) val.toTuple();\n                if (tv == null || tv.size() != cnt) {\n                  Assert.fail("Attempted to compute the value of an expression of form\\n" +\n                              "CHOOSE <<x1, ... , xN>> \\\\in S: P, but S was not a set\\n" +\n                              "of N-tuples.\\n" + expr, expr, c);\n                }\n                Context c1 = c;\n                for (int i = 0; i < cnt; i++) {\n                  c1 = c1.cons(bvars[i], tv.elems[i]);\n                }\n                Value bval = this.eval(pred, c1, s0, s1, control, cm);\n                if (!(bval instanceof BoolValue)) {\n                  Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}, pred, c1);\n                }\n                if (((BoolValue)bval).val) {\n                  return (Value) val;\n                }\n              }\n            }\n            else {\n              // Simple identifier case:\n              SymbolNode name = bvars[0];\n              Value val;\n              while ((val = enumSet.nextElement()) != null) {\n                Context c1 = c.cons(name, val);\n                Value bval = this.eval(pred, c1, s0, s1, control, cm);\n                if (!(bval instanceof BoolValue)) {\n                  Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}, pred, c1);\n                }\n                if (((BoolValue)bval).val) {\n                  return (Value) val;\n                }\n              }\n            }\n            Assert.fail("Attempted to compute the value of an expression of form\\n" +\n                        "CHOOSE x \\\\in S: P, but no element of S satisfied P.\\n" + expr, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_be:     // BoundedExists\n          {\n            ContextEnumerator Enum = this.contexts(expr, c, s0, s1, control, cm);\n            SemanticNode body = args[0];\n            Context c1;\n            while ((c1 = Enum.nextElement()) != null) {\n              Value bval = this.eval(body, c1, s0, s1, control, cm);\n              if (!(bval instanceof BoolValue)) {\n                Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}, body, c1);\n              }\n              if (((BoolValue)bval).val) {\n                return BoolValue.ValTrue;\n              }\n            }\n            return BoolValue.ValFalse;\n          }\n        case OPCODE_bf:     // BoundedForall\n          {\n            ContextEnumerator Enum = this.contexts(expr, c, s0, s1, control, cm);\n            SemanticNode body = args[0];\n            Context c1;\n            while ((c1 = Enum.nextElement()) != null) {\n              Value bval = this.eval(body, c1, s0, s1, control, cm);\n              if (!(bval instanceof BoolValue)) {\n                Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}, body, c1);\n              }\n              if (!((BoolValue)bval).val) {\n                return BoolValue.ValFalse;\n              }\n            }\n            return BoolValue.ValTrue;\n          }\n        case OPCODE_case:   // Case\n          {\n            int alen = args.length;\n            SemanticNode other = null;\n            for (int i = 0; i < alen; i++) {\n              OpApplNode pairNode = (OpApplNode)args[i];\n              ExprOrOpArgNode[] pairArgs = pairNode.getArgs();\n              if (pairArgs[0] == null) {\n                other = pairArgs[1];\n                if (coverage) { cm = cm.get(pairNode); }\n               }\n              else {\n                Value bval = this.eval(pairArgs[0], c, s0, s1, control, coverage ? cm.get(pairNode) : cm);\n                if (!(bval instanceof BoolValue)) {\n                  Assert.fail("A non-boolean expression (" + bval.getKindString() +\n                              ") was used as a condition of a CASE. " + pairArgs[0], pairArgs[0], c);\n                }\n                if (((BoolValue)bval).val) {\n                  return this.eval(pairArgs[1], c, s0, s1, control, coverage ? cm.get(pairNode) : cm);\n                }\n              }\n            }\n            if (other == null) {\n              Assert.fail("Attempted to evaluate a CASE with no conditions true.\\n" + expr, expr, c);\n            }\n            return this.eval(other, c, s0, s1, control, cm);\n          }\n        case OPCODE_cp:     // CartesianProd\n          {\n            int alen = args.length;\n            Value[] sets = new Value[alen];\n            for (int i = 0; i < alen; i++) {\n              sets[i] = this.eval(args[i], c, s0, s1, control, cm);\n            }\n            return setSource(expr, new SetOfTuplesValue(sets, cm));\n          }\n        case OPCODE_cl:     // ConjList\n          {\n            int alen = args.length;\n            for (int i = 0; i < alen; i++) {\n              Value bval = this.eval(args[i], c, s0, s1, control, cm);\n              if (!(bval instanceof BoolValue)) {\n                Assert.fail("A non-boolean expression (" + bval.getKindString() +\n                            ") was used as a formula in a conjunction.\\n" + args[i], args[i], c);\n              }\n              if (!((BoolValue)bval).val) {\n                return BoolValue.ValFalse;\n              }\n            }\n            return BoolValue.ValTrue;\n          }\n        case OPCODE_dl:     // DisjList\n          {\n            int alen = args.length;\n            for (int i = 0; i < alen; i++) {\n              Value bval = this.eval(args[i], c, s0, s1, control, cm);\n              if (!(bval instanceof BoolValue)) {\n                Assert.fail("A non-boolean expression (" + bval.getKindString() +\n                            ") was used as a formula in a disjunction.\\n" + args[i], args[i], c);\n              }\n              if (((BoolValue)bval).val) {\n                return BoolValue.ValTrue;\n              }\n            }\n            return BoolValue.ValFalse;\n          }\n        case OPCODE_exc:    // Except\n          {\n            int alen = args.length;\n            Value result = this.eval(args[0], c, s0, s1, control, cm);\n            // SZ: variable not used ValueExcept[] expts = new ValueExcept[alen-1];\n            for (int i = 1; i < alen; i++) {\n              OpApplNode pairNode = (OpApplNode)args[i];\n              ExprOrOpArgNode[] pairArgs = pairNode.getArgs();\n              SemanticNode[] cmpts = ((OpApplNode)pairArgs[0]).getArgs();\n\n              Value[] lhs = new Value[cmpts.length];\n              for (int j = 0; j < lhs.length; j++) {\n                lhs[j] = this.eval(cmpts[j], c, s0, s1, control,  coverage ? cm.get(pairNode).get(pairArgs[0]) : cm);\n              }\n              Value atVal = result.select(lhs);\n              if (atVal == null) {\n                // Do nothing but warn:\n                  MP.printWarning(EC.TLC_EXCEPT_APPLIED_TO_UNKNOWN_FIELD, new String[]{args[0].toString()});\n              }\n              else {\n                Context c1 = c.cons(EXCEPT_AT, atVal);\n                Value rhs = this.eval(pairArgs[1], c1, s0, s1, control,  coverage ? cm.get(pairNode) : cm);\n                ValueExcept vex = new ValueExcept(lhs, rhs);\n                result = (Value) result.takeExcept(vex);\n              }\n            }\n            return result;\n          }\n        case OPCODE_fa:     // FcnApply\n          {\n            Value result = null;\n            Value fval = this.eval(args[0], c, s0, s1, EvalControl.setKeepLazy(control), cm);\n            if ((fval instanceof FcnRcdValue) ||\n                (fval instanceof FcnLambdaValue)) {\n              Applicable fcn = (Applicable)fval;\n              Value argVal = this.eval(args[1], c, s0, s1, control, cm);\n              result = fcn.apply(argVal, control);\n            }\n            else if ((fval instanceof TupleValue) ||\n                     (fval instanceof RecordValue)) {\n              Applicable fcn = (Applicable)fval;\n              if (args.length != 2) {\n                Assert.fail("Attempted to evaluate an expression of form f[e1, ... , eN]" +\n                            "\\nwith f a tuple or record and N > 1.\\n" + expr, expr, c);\n              }\n              Value aval = this.eval(args[1], c, s0, s1, control, cm);\n              result = fcn.apply(aval, control);\n            }\n            else {\n              Assert.fail("A non-function (" + fval.getKindString() + ") was applied" +\n                          " as a function.\\n" + expr, expr, c);\n            }\n            return result;\n          }\n        case OPCODE_fc:     // FcnConstructor\n        case OPCODE_nrfs:   // NonRecursiveFcnSpec\n        case OPCODE_rfs:    // RecursiveFcnSpec\n          {\n            FormalParamNode[][] formals = expr.getBdedQuantSymbolLists();\n            boolean[] isTuples = expr.isBdedQuantATuple();\n            ExprNode[] domains = expr.getBdedQuantBounds();\n\n            Value[] dvals = new Value[domains.length];\n            boolean isFcnRcd = true;\n            for (int i = 0; i < dvals.length; i++) {\n              dvals[i] = this.eval(domains[i], c, s0, s1, control, cm);\n              isFcnRcd = isFcnRcd && (dvals[i] instanceof Reducible);\n            }\n            FcnParams params = new FcnParams(formals, isTuples, dvals);\n\n            SemanticNode fbody = args[0];\n            FcnLambdaValue fval = (FcnLambdaValue) setSource(expr, new FcnLambdaValue(params, fbody, this, c, s0, s1, control, cm));\n            if (opcode == OPCODE_rfs) {\n              SymbolNode fname = expr.getUnbdedQuantSymbols()[0];\n              fval.makeRecursive(fname);\n              isFcnRcd = false;\n            }\n            if (isFcnRcd && !EvalControl.isKeepLazy(control)) {\n              return (Value) fval.toFcnRcd();\n            }\n            return fval;\n          }\n        case OPCODE_ite:    // IfThenElse\n          {\n            Value bval = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(bval instanceof BoolValue)) {\n              Assert.fail("A non-boolean expression (" + bval.getKindString() +\n                          ") was used as the condition of an IF.\\n" + expr, expr, c);\n            }\n            if (((BoolValue)bval).val) {\n              return this.eval(args[1], c, s0, s1, control, cm);\n            }\n            return this.eval(args[2], c, s0, s1, control, cm);\n          }\n        case OPCODE_rc:     // RcdConstructor\n          {\n            int alen = args.length;\n            UniqueString[] names = new UniqueString[alen];\n            Value[] vals = new Value[alen];\n            for (int i = 0; i < alen; i++) {\n              OpApplNode pairNode = (OpApplNode)args[i];\n              ExprOrOpArgNode[] pair = pairNode.getArgs();\n              names[i] = ((StringValue)pair[0].getToolObject(toolId)).getVal();\n              vals[i] = this.eval(pair[1], c, s0, s1, control, coverage ? cm.get(pairNode) : cm);\n            }\n            return setSource(expr, new RecordValue(names, vals, false, cm));\n          }\n        case OPCODE_rs:     // RcdSelect\n          {\n            Value rval = this.eval(args[0], c, s0, s1, control, cm);\n            Value sval = (Value) WorkerValue.mux(args[1].getToolObject(toolId));\n            if (rval instanceof RecordValue) {\n              Value result = (Value) ((RecordValue)rval).select(sval);\n              if (result == null) {\n                Assert.fail("Attempted to select nonexistent field " + sval + " from the" +\n                            " record\\n" + Values.ppr(rval.toString()) + "\\n" + expr, expr, c);\n              }\n              return result;\n            }\n            else {\n              FcnRcdValue fcn = (FcnRcdValue) rval.toFcnRcd();\n              if (fcn == null) {\n                Assert.fail("Attempted to select field " + sval + " from a non-record" +\n                            " value " + Values.ppr(rval.toString()) + "\\n" + expr, expr, c);\n              }\n              return fcn.apply(sval, control);\n            }\n          }\n        case OPCODE_se:     // SetEnumerate\n          {\n            int alen = args.length;\n            ValueVec vals = new ValueVec(alen);\n            for (int i = 0; i < alen; i++) {\n              vals.addElement(this.eval(args[i], c, s0, s1, control, cm));\n            }\n            return setSource(expr, new SetEnumValue(vals, false, cm));\n          }\n        case OPCODE_soa:    // SetOfAll: {e(x) : x \\in S}\n          {\n            ValueVec vals = new ValueVec();\n            ContextEnumerator Enum = this.contexts(expr, c, s0, s1, control, cm);\n            SemanticNode body = args[0];\n            Context c1;\n            while ((c1 = Enum.nextElement()) != null) {\n              Value val = this.eval(body, c1, s0, s1, control, cm);\n              vals.addElement(val);\n              // vals.addElement1(val);\n            }\n            return setSource(expr, new SetEnumValue(vals, false, cm));\n          }\n        case OPCODE_sor:    // SetOfRcds\n          {\n            int alen = args.length;\n            UniqueString names[] = new UniqueString[alen];\n            Value vals[] = new Value[alen];\n            for (int i = 0; i < alen; i++) {\n              OpApplNode pairNode = (OpApplNode)args[i];\n              ExprOrOpArgNode[] pair = pairNode.getArgs();\n              names[i] = ((StringValue)pair[0].getToolObject(toolId)).getVal();\n              vals[i] = this.eval(pair[1], c, s0, s1, control, coverage ? cm.get(pairNode) : cm);\n            }\n            return setSource(expr, new SetOfRcdsValue(names, vals, false, cm));\n          }\n        case OPCODE_sof:    // SetOfFcns\n          {\n            Value lhs = this.eval(args[0], c, s0, s1, control, cm);\n            Value rhs = this.eval(args[1], c, s0, s1, control, cm);\n            return setSource(expr, new SetOfFcnsValue(lhs, rhs, cm));\n          }\n        case OPCODE_sso:    // SubsetOf\n          {\n            SemanticNode pred = args[0];\n            SemanticNode inExpr = expr.getBdedQuantBounds()[0];\n            Value inVal = this.eval(inExpr, c, s0, s1, control, cm);\n            boolean isTuple = expr.isBdedQuantATuple()[0];\n            FormalParamNode[] bvars = expr.getBdedQuantSymbolLists()[0];\n            if (inVal instanceof Reducible) {\n              ValueVec vals = new ValueVec();\n              ValueEnumeration enumSet = ((Enumerable)inVal).elements();\n              Value elem;\n              if (isTuple) {\n                while ((elem = enumSet.nextElement()) != null) {\n                  Context c1 = c;\n                  Value[] tuple = ((TupleValue)elem).elems;\n                  for (int i = 0; i < bvars.length; i++) {\n                    c1 = c1.cons(bvars[i], tuple[i]);\n                  }\n                  Value bval = this.eval(pred, c1, s0, s1, control, cm);\n                  if (!(bval instanceof BoolValue)) {\n                    Assert.fail("Attempted to evaluate an expression of form {x \\\\in S : P(x)}" +\n                                " when P was " + bval.getKindString() + ".\\n" + pred, pred, c1);\n                  }\n                  if (((BoolValue)bval).val) {\n                    vals.addElement(elem);\n                  }\n                }\n              }\n              else {\n                SymbolNode idName = bvars[0];\n                while ((elem = enumSet.nextElement()) != null) {\n                  Context c1 = c.cons(idName, elem);\n                  Value bval = this.eval(pred, c1, s0, s1, control, cm);\n                  if (!(bval instanceof BoolValue)) {\n                    Assert.fail("Attempted to evaluate an expression of form {x \\\\in S : P(x)}" +\n                                " when P was " + bval.getKindString() + ".\\n" + pred, pred, c1);\n                  }\n                  if (((BoolValue)bval).val) {\n                    vals.addElement(elem);\n                  }\n                }\n              }\n              return setSource(expr, new SetEnumValue(vals, inVal.isNormalized(), cm));\n            }\n            else if (isTuple) {\n              return setSource(expr, new SetPredValue(bvars, inVal, pred, this, c, s0, s1, control, cm));\n            }\n            else {\n              return setSource(expr, new SetPredValue(bvars[0], inVal, pred, this, c, s0, s1, control, cm));\n            }\n          }\n        case OPCODE_tup:    // Tuple\n          {\n            int alen = args.length;\n            Value[] vals = new Value[alen];\n            for (int i = 0; i < alen; i++) {\n              vals[i] = this.eval(args[i], c, s0, s1, control, cm);\n            }\n            return setSource(expr, new TupleValue(vals, cm));\n          }\n        case OPCODE_uc:     // UnboundedChoose\n          {\n            Assert.fail("TLC attempted to evaluate an unbounded CHOOSE.\\n" +\n                        "Make sure that the expression is of form CHOOSE x \\\\in S: P(x).\\n" +\n                        expr, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_ue:     // UnboundedExists\n          {\n            Assert.fail("TLC attempted to evaluate an unbounded \\\\E.\\n" +\n                        "Make sure that the expression is of form \\\\E x \\\\in S: P(x).\\n" +\n                        expr, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_uf:     // UnboundedForall\n          {\n            Assert.fail("TLC attempted to evaluate an unbounded \\\\A.\\n" +\n                        "Make sure that the expression is of form \\\\A x \\\\in S: P(x).\\n" +\n                        expr, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_lnot:\n          {\n            Value arg = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(arg instanceof BoolValue)) {\n              Assert.fail("Attempted to apply the operator ~ to a non-boolean\\n(" +\n                          arg.getKindString() + ")\\n" + expr, args[0], c);\n            }\n            return (((BoolValue)arg).val) ? BoolValue.ValFalse : BoolValue.ValTrue;\n          }\n        case OPCODE_subset:\n          {\n            Value arg = this.eval(args[0], c, s0, s1, control, cm);\n\t\t\treturn setSource(expr, new SubsetValue(arg, cm));\n          }\n        case OPCODE_union:\n          {\n            Value arg = this.eval(args[0], c, s0, s1, control, cm);\n            return setSource(expr, UnionValue.union(arg));\n          }\n        case OPCODE_domain:\n          {\n            Value arg = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(arg instanceof Applicable)) {\n              Assert.fail("Attempted to apply the operator DOMAIN to a non-function\\n(" +\n                          arg.getKindString() + ")\\n" + expr, expr, c);\n            }\n            return setSource(expr, ((Applicable)arg).getDomain());\n          }\n        case OPCODE_enabled:\n          {\n            TLCState sfun = TLCStateFun.Empty;\n            Context c1 = Context.branch(c);\n            sfun = this.enabled(args[0], ActionItemList.Empty, c1, s0, sfun, cm);\n            return (sfun != null) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_eq:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            return (arg1.equals(arg2)) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_land:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(arg1 instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form P /\\\\ Q" +\n                          " when P was\\n" + arg1.getKindString() + ".\\n" + expr, expr, c);\n            }\n            if (((BoolValue)arg1).val) {\n              Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n              if (!(arg2 instanceof BoolValue)) {\n                Assert.fail("Attempted to evaluate an expression of form P /\\\\ Q" +\n                            " when Q was\\n" + arg2.getKindString() + ".\\n" + expr, expr, c);\n              }\n              return arg2;\n            }\n            return BoolValue.ValFalse;\n          }\n        case OPCODE_lor:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(arg1 instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form P \\\\/ Q" +\n                          " when P was\\n" + arg1.getKindString() + ".\\n" + expr, expr, c);\n            }\n            if (((BoolValue)arg1).val) {\n              return BoolValue.ValTrue;\n            }\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (!(arg2 instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form P \\\\/ Q" +\n                          " when Q was\\n" + arg2.getKindString() + ".\\n" + expr, expr, c);\n            }\n            return arg2;\n          }\n        case OPCODE_implies:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(arg1 instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form P => Q" +\n                          " when P was\\n" + arg1.getKindString() + ".\\n" + expr, expr, c);\n            }\n            if (((BoolValue)arg1).val) {\n              Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n              if (!(arg2 instanceof BoolValue)) {\n                Assert.fail("Attempted to evaluate an expression of form P => Q" +\n                            " when Q was\\n" + arg2.getKindString() + ".\\n" + expr, expr, c);\n              }\n              return arg2;\n            }\n            return BoolValue.ValTrue;\n          }\n        case OPCODE_equiv:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (!(arg1 instanceof BoolValue) || !(arg2 instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form P <=> Q" +\n                          " when P or Q was not a boolean.\\n" + expr, expr, c);\n            }\n            BoolValue bval1 = (BoolValue)arg1;\n            BoolValue bval2 = (BoolValue)arg2;\n            return (bval1.val == bval2.val) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_noteq:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            return arg1.equals(arg2) ? BoolValue.ValFalse : BoolValue.ValTrue;\n          }\n        case OPCODE_subseteq:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (!(arg1 instanceof Enumerable)) {\n              Assert.fail("Attempted to evaluate an expression of form S \\\\subseteq T," +\n                          " but S was not enumerable.\\n" + expr, expr, c);\n            }\n            return ((Enumerable) arg1).isSubsetEq(arg2);\n          }\n        case OPCODE_in:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            return (arg2.member(arg1)) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_notin:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            return (arg2.member(arg1)) ? BoolValue.ValFalse : BoolValue.ValTrue;\n          }\n        case OPCODE_setdiff:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (arg1 instanceof Reducible) {\n              return setSource(expr, ((Reducible)arg1).diff(arg2));\n            }\n            return setSource(expr, new SetDiffValue(arg1, arg2));\n          }\n        case OPCODE_cap:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (arg1 instanceof Reducible) {\n              return setSource(expr, ((Reducible)arg1).cap(arg2));\n            }\n            else if (arg2 instanceof Reducible) {\n              return setSource(expr, ((Reducible)arg2).cap(arg1));\n            }\n            return setSource(expr, new SetCapValue(arg1, arg2));\n          }\n        case OPCODE_nop:\n          // Added by LL on 2 Aug 2007\n          {\n            return eval(args[0], c, s0, s1, control, cm);\n          }\n        case OPCODE_cup:\n          {\n            Value arg1 = this.eval(args[0], c, s0, s1, control, cm);\n            Value arg2 = this.eval(args[1], c, s0, s1, control, cm);\n            if (arg1 instanceof Reducible) {\n              return setSource(expr, ((Reducible)arg1).cup(arg2));\n            }\n            else if (arg2 instanceof Reducible) {\n              return setSource(expr, ((Reducible)arg2).cup(arg1));\n            }\n            return setSource(expr, new SetCupValue(arg1, arg2, cm));\n          }\n        case OPCODE_prime:\n          {\n        \t  // MAK 03/2019:  Cannot reproduce this but without this check the nested evaluation\n        \t  // fails with a NullPointerException which subsequently is swallowed. This makes it \n        \t  // impossible for a user to diagnose what is going on.  Since I cannot reproduce the\n        \t  // actual expression, I leave this commented for.  I recall an expression along the\n        \t  // lines of:\n        \t  //    ...\n        \t  //    TLCSet(23, CHOOSE p \\in pc: pc[p] # pc[p]\')\n        \t  //    ...\n        \t  // The fail statement below is obviously too generic to be useful and needs to be\n        \t  // clarified if the actual cause has been identified.\n//        \t  if (s1 == null) {\n//                  Assert.fail("Attempted to evaluate the following expression," +\n//                          " but expression failed to evaluate.\\n" + expr);\n//        \t  }\n            return this.eval(args[0], c, s1, TLCState.Null, EvalControl.setPrimedIfEnabled(control), cm);\n          }\n        case OPCODE_unchanged:\n          {\n            Value v0 = this.eval(args[0], c, s0, TLCState.Empty, control, cm);\n            Value v1 = this.eval(args[0], c, s1, TLCState.Null, EvalControl.setPrimedIfEnabled(control), cm);\n            return (v0.equals(v1)) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_aa:     // <A>_e\n          {\n            Value res = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(res instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form <A>_e," +\n                          " but A was not a boolean.\\n" + expr, expr, c);\n            }\n            if (!((BoolValue)res).val) {\n              return BoolValue.ValFalse;\n            }\n            Value v0 = this.eval(args[1], c, s0, TLCState.Empty, control, cm);\n            Value v1 = this.eval(args[1], c, s1, TLCState.Null, EvalControl.setPrimedIfEnabled(control), cm);\n            return v0.equals(v1) ? BoolValue.ValFalse : BoolValue.ValTrue;\n          }\n        case OPCODE_sa:     // [A]_e\n          {\n            Value res = this.eval(args[0], c, s0, s1, control, cm);\n            if (!(res instanceof BoolValue)) {\n              Assert.fail("Attempted to evaluate an expression of form [A]_e," +\n                          " but A was not a boolean.\\n" + expr, expr, c);\n            }\n            if (((BoolValue)res).val) {\n              return BoolValue.ValTrue;\n            }\n            Value v0 = this.eval(args[1], c, s0, TLCState.Empty, control, cm);\n            Value v1 = this.eval(args[1], c, s1, TLCState.Null, EvalControl.setPrimedIfEnabled(control), cm);\n            return (v0.equals(v1)) ? BoolValue.ValTrue : BoolValue.ValFalse;\n          }\n        case OPCODE_cdot:\n          {\n            Assert.fail("The current version of TLC does not support action composition.", expr, c);\n            /***\n            TLCState s01 = TLCStateFun.Empty;\n            StateVec iss = new StateVec(0);\n            this.getNextStates(args[0], ActionItemList.Empty, c, s0, s01, iss);\n            int sz = iss.size();\n            for (int i = 0; i < sz; i++) {\n              s01 = iss.elementAt(i);\n              this.eval(args[1], c, s01, s1, control);\n            }\n            ***/\n            return null;    // make compiler happy\n          }\n        case OPCODE_sf:     // SF\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"SF", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_wf:     // WF\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"WF", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_te:     // TemporalExists\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"\\\\EE", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_tf:     // TemporalForAll\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"\\\\AA", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_leadto:\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"a ~> b", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_arrow:\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"a -+-> formula", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_box:\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"[]A", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n        case OPCODE_diamond:\n          {\n            Assert.fail(EC.TLC_ENCOUNTERED_FORMULA_IN_PREDICATE, new String[]{"<>A", expr.toString()}, expr, c);\n            return null;    // make compiler happy\n          }\n\n        default:\n          {\n            Assert.fail("TLC BUG: could not evaluate this expression.\\n" + expr, expr, c);\n            return null;\n          }\n        }\n  }\n\n  protected abstract Value setSource(final SemanticNode expr, final Value value);\n\n  /**\n   * This method determines if the argument is a valid state.  A state\n   * is good iff it assigns legal explicit values to all the global\n   * state variables.\n   */\n  @Override\n  public final boolean isGoodState(TLCState state) {\n    return state.allAssigned();\n  }\n\n  /* This method determines if a state satisfies the model constraints. */\n  @Override\n  public final boolean isInModel(TLCState state) throws EvalException {\n    ExprNode[] constrs = this.getModelConstraints();\n    for (int i = 0; i < constrs.length; i++) {\n      final CostModel cm = coverage ? ((Action) constrs[i].getToolObject(toolId)).cm : CostModel.DO_NOT_RECORD;\n      IValue bval = this.eval(constrs[i], Context.Empty, state, cm);\n      if (!(bval instanceof BoolValue)) {\n        Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", constrs[i].toString()}, constrs[i]);\n      }\n      if (!((BoolValue)bval).val) {\n  \t\t  if (coverage) {\n  \t\t\t  cm.incInvocations();\n\t\t  }\n    \t  return false;\n      } else {\n  \t\t  if (coverage) {\n  \t\t\t  cm.incSecondary();\n\t\t  }\n      }\n    }\n    return true;\n  }\n\n  /* This method determines if a pair of states satisfy the action constraints. */\n  @Override\n  public final boolean isInActions(TLCState s1, TLCState s2) throws EvalException {\n    ExprNode[] constrs = this.getActionConstraints();\n    for (int i = 0; i < constrs.length; i++) {\n      final CostModel cm = coverage ? ((Action) constrs[i].getToolObject(toolId)).cm : CostModel.DO_NOT_RECORD;\n      Value bval = this.eval(constrs[i], Context.Empty, s1, s2, EvalControl.Clear, cm);\n      if (!(bval instanceof BoolValue)) {\n        Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", constrs[i].toString()}, constrs[i]);\n      }\n      if (!((BoolValue)bval).val) {\n  \t\t  if (coverage) {\n\t\t\t  cm.incInvocations();\n\t\t  }\n    \t  return false;\n      } else {\n  \t\t  if (coverage) {\n  \t\t\t  cm.incSecondary();\n\t\t  }\n      }\n    }\n    return true;\n  }\n  \n  @Override\n  public final boolean hasStateOrActionConstraints() {\n\t  return this.getModelConstraints().length > 0 || this.getActionConstraints().length > 0;\n  }\n  \n  @Override\n  public final TLCState enabled(SemanticNode pred, Context c, TLCState s0, TLCState s1) {\n\t\t  return enabled(pred, ActionItemList.Empty, c, s0, s1, CostModel.DO_NOT_RECORD);\n  }\n  \n  @Override\n  public final TLCState enabled(SemanticNode pred, Context c, TLCState s0, TLCState s1, ExprNode subscript, final int ail) {\n      ActionItemList acts = (ActionItemList) ActionItemList.Empty.cons(subscript, c, CostModel.DO_NOT_RECORD, ail);\n\t  return enabled(pred, acts, c, s0, s1, CostModel.DO_NOT_RECORD);\n  }\n  \n  @Override\n  public final TLCState enabled(SemanticNode pred, IActionItemList acts, Context c, TLCState s0, TLCState s1) {\n\t\t  return enabled(pred, acts, c, s0, s1, CostModel.DO_NOT_RECORD);\n  }\n\n  /**\n   * This method determines if an action is enabled in the given state.\n   * More precisely, it determines if (act.pred /\\ (sub\' # sub)) is\n   * enabled in the state s and context act.con.\n   */\n  @Override\n  public abstract TLCState enabled(SemanticNode pred, IActionItemList acts,\n                                Context c, TLCState s0, TLCState s1, CostModel cm);\n\n  protected final TLCState enabledImpl(SemanticNode pred, ActionItemList acts,\n          Context c, TLCState s0, TLCState s1, CostModel cm) {\n        switch (pred.getKind()) {\n        case OpApplKind:\n          {\n            OpApplNode pred1 = (OpApplNode)pred;\n            return this.enabledAppl(pred1, acts, c, s0, s1, cm);\n          }\n        case LetInKind:\n          {\n            LetInNode pred1 = (LetInNode)pred;\n            OpDefNode[] letDefs = pred1.getLets();\n            Context c1 = c;\n            for (int i = 0; i < letDefs.length; i++) {\n              OpDefNode opDef = letDefs[i];\n              if (opDef.getArity() == 0) {\n                Value rhs = new LazyValue(opDef.getBody(), c1, cm);\n                c1 = c1.cons(opDef, rhs);\n              }\n            }\n            return this.enabled(pred1.getBody(), acts, c1, s0, s1, cm);\n          }\n        case SubstInKind:\n          {\n            SubstInNode pred1 = (SubstInNode)pred;\n            Subst[] subs = pred1.getSubsts();\n            int slen = subs.length;\n            Context c1 = c;\n            for (int i = 0; i < slen; i++) {\n              Subst sub = subs[i];\n              c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, coverage ? sub.getCM() : cm, toolId));\n            }\n            return this.enabled(pred1.getBody(), acts, c1, s0, s1, cm);\n          }\n        // Added by LL on 13 Nov 2009 to handle theorem and assumption names.\n        case APSubstInKind:\n          {\n            APSubstInNode pred1 = (APSubstInNode)pred;\n            Subst[] subs = pred1.getSubsts();\n            int slen = subs.length;\n            Context c1 = c;\n            for (int i = 0; i < slen; i++) {\n              Subst sub = subs[i];\n              c1 = c1.cons(sub.getOp(), this.getVal(sub.getExpr(), c, false, cm, toolId));\n            }\n            return this.enabled(pred1.getBody(), acts, c1, s0, s1, cm);\n          }\n        // LabelKind class added by LL on 13 Jun 2007\n        case LabelKind:\n          {\n            LabelNode pred1 = (LabelNode)pred;\n            return this.enabled(pred1.getBody(), acts, c, s0, s1, cm);\n          }\n        default:\n          {\n            // We should not compute enabled on anything else.\n            Assert.fail("Attempted to compute ENABLED on a non-boolean expression.\\n" + pred, pred, c);\n            return null;    // make compiler happy\n          }\n        }\n  }\n\n  private final TLCState enabled(ActionItemList acts, TLCState s0, TLCState s1, CostModel cm) {\n    if (acts.isEmpty()) return s1;\n\n    final int kind = acts.carKind();\n    SemanticNode pred = acts.carPred();\n    Context c = acts.carContext();\n    cm = acts.cm;\n    ActionItemList acts1 = acts.cdr();\n    if (kind > IActionItemList.CONJUNCT) {\n      TLCState res = this.enabled(pred, acts1, c, s0, s1, cm);\n      return res;\n    }\n    else if (kind == IActionItemList.PRED) {\n      TLCState res = this.enabled(pred, acts1, c, s0, s1, cm);\n      return res;\n    }\n    if (kind == IActionItemList.UNCHANGED) {\n      TLCState res = this.enabledUnchanged(pred, acts1, c, s0, s1, cm);\n      return res;\n    }\n\n    Value v1 = this.eval(pred, c, s0, TLCState.Empty, EvalControl.Enabled, cm);\n\t// We are now in ENABLED and primed state. Second TLCState parameter being null\n\t// effectively disables LazyValue in evalAppl (same effect as\n\t// EvalControl.setPrimed(EvalControl.Enabled)).\n    Value v2 = this.eval(pred, c, s1, TLCState.Null, EvalControl.Primed, cm);\n\n    if (v1.equals(v2)) return null;\n    TLCState res = this.enabled(acts1, s0, s1, cm);\n    return res;\n  }\n\n  protected abstract TLCState enabledAppl(OpApplNode pred, ActionItemList acts, Context c, TLCState s0, TLCState s1, CostModel cm);\n\n  protected final TLCState enabledApplImpl(OpApplNode pred, ActionItemList acts, Context c, TLCState s0, TLCState s1, CostModel cm)\n  {\n    if (coverage) {cm = cm.get(pred);}\n        ExprOrOpArgNode[] args = pred.getArgs();\n        int alen = args.length;\n        SymbolNode opNode = pred.getOperator();\n        int opcode = BuiltInOPs.getOpCode(opNode.getName());\n\n        if (opcode == 0)\n        {\n          // This is a user-defined operator with one exception: it may\n          // be substed by a builtin operator. This special case occurs\n          // when the lookup returns an OpDef with opcode # 0.\n          Object val = this.lookup(opNode, c, s0, false);\n\n          if (val instanceof OpDefNode)\n          {\n            OpDefNode opDef = (OpDefNode) val;\n            opcode = BuiltInOPs.getOpCode(opDef.getName());\n            if (opcode == 0)\n            {\n              // Context c1 = this.getOpContext(opDef, args, c, false);\n              Context c1 = this.getOpContext(opDef, args, c, true, cm, toolId);\n              return this.enabled(opDef.getBody(), acts, c1, s0, s1, cm);\n            }\n          }\n\n\n          // Added 13 Nov 2009 by LL to handle theorem or assumption names\n          /*********************************************************************\n          * Modified on 23 October 2012 by LL to work if ThmOrAssumpDefNode    *\n          * imported with parameterized instantiation.                         *\n          *********************************************************************/\n          if (val instanceof ThmOrAssumpDefNode)\n          {\n            ThmOrAssumpDefNode opDef = (ThmOrAssumpDefNode) val;\n            Context c1 = this.getOpContext(opDef, args, c, true);\n            return this.enabled(opDef.getBody(), acts, c1, s0, s1, cm);\n          }\n\n\n          if (val instanceof LazyValue)\n          {\n            LazyValue lv = (LazyValue) val;\n            return this.enabled(lv.expr, acts, lv.con, s0, s1, lv.cm);\n          }\n\n          Object bval = val;\n          if (alen == 0)\n          {\n            if (val instanceof MethodValue)\n            {\n              bval = ((MethodValue) val).apply(EmptyArgs, EvalControl.Clear); // EvalControl.Clear is ignored by MethodValuea#apply\n            } else if (val instanceof EvaluatingValue) {\n              bval = ((EvaluatingValue) val).eval(this, args, c, s0, s1, EvalControl.Enabled, cm);\n            }\n          } else\n          {\n            if (val instanceof OpValue)\n            {\n            \tbval = ((OpValue) val).eval(this, args, c, s0, s1, EvalControl.Enabled, cm);\n             }\n          }\n\n          if (opcode == 0)\n          {\n            if (!(bval instanceof BoolValue))\n            {\n              Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "ENABLED", "boolean",\n                      bval.toString(), pred.toString() }, pred, c);\n            }\n            if (((BoolValue) bval).val)\n            {\n              return this.enabled(acts, s0, s1, cm);\n            }\n            return null;\n          }\n        }\n\n        switch (opcode) {\n        case OPCODE_aa: // AngleAct <A>_e\n          {\n        \t  ActionItemList acts1 = (ActionItemList) acts.cons(args[1], c, cm, IActionItemList.CHANGED);\n            return this.enabled(args[0], acts1, c, s0, s1, cm);\n          }\n        case OPCODE_be: // BoundedExists\n          {\n            SemanticNode body = args[0];\n            ContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Enabled, cm);\n            Context c1;\n            while ((c1 = Enum.nextElement()) != null)\n            {\n              TLCState s2 = this.enabled(body, acts, c1, s0, s1, cm);\n              if (s2 != null) {\n                return s2;\n              }\n            }\n            return null;\n          }\n        case OPCODE_bf: // BoundedForall\n          {\n            SemanticNode body = args[0];\n            ContextEnumerator Enum = this.contexts(pred, c, s0, s1, EvalControl.Enabled, cm);\n            Context c1 = Enum.nextElement();\n            if (c1 == null)\n            {\n              return this.enabled(acts, s0, s1, cm);\n            }\n            ActionItemList acts1 = acts;\n            Context c2;\n            while ((c2 = Enum.nextElement()) != null)\n            {\n              acts1 = (ActionItemList) acts1.cons(body, c2, cm, IActionItemList.PRED);\n            }\n            return this.enabled(body, acts1, c1, s0, s1, cm);\n          }\n        case OPCODE_case: // Case\n          {\n            SemanticNode other = null;\n            for (int i = 0; i < alen; i++)\n            {\n              OpApplNode pair = (OpApplNode) args[i];\n              ExprOrOpArgNode[] pairArgs = pair.getArgs();\n              if (pairArgs[0] == null)\n              {\n                other = pairArgs[1];\n              } else\n              {\n                Value bval = this.eval(pairArgs[0], c, s0, s1, EvalControl.Enabled, cm);\n                if (!(bval instanceof BoolValue))\n                {\n                  Assert.fail("In computing ENABLED, a non-boolean expression(" + bval.getKindString()\n                          + ") was used as a guard condition" + " of a CASE.\\n" + pairArgs[1], pairArgs[1], c);\n                }\n                if (((BoolValue) bval).val)\n                {\n                  return this.enabled(pairArgs[1], acts, c, s0, s1, cm);\n                }\n              }\n            }\n            if (other == null)\n            {\n              Assert.fail("In computing ENABLED, TLC encountered a CASE with no" + " conditions true.\\n" + pred, pred, c);\n            }\n            return this.enabled(other, acts, c, s0, s1, cm);\n          }\n        case OPCODE_cl: // ConjList\n        case OPCODE_land:\n          {\n            ActionItemList acts1 = acts;\n            for (int i = alen - 1; i > 0; i--)\n            {\n              acts1 = (ActionItemList) acts1.cons(args[i], c, cm, i);\n            }\n            return this.enabled(args[0], acts1, c, s0, s1, cm);\n          }\n        case OPCODE_dl: // DisjList\n        case OPCODE_lor:\n          {\n            for (int i = 0; i < alen; i++)\n            {\n              TLCState s2 = this.enabled(args[i], acts, c, s0, s1, cm);\n              if (s2 != null) {\n                return s2;\n              }\n            }\n            return null;\n          }\n        case OPCODE_fa: // FcnApply\n          {\n            Value fval = this.eval(args[0], c, s0, s1, EvalControl.setKeepLazy(EvalControl.Enabled), cm); // KeepLazy does not interfere with EvalControl.Enabled in this.evalAppl\n            if (fval instanceof FcnLambdaValue)\n            {\n              FcnLambdaValue fcn = (FcnLambdaValue) fval;\n              if (fcn.fcnRcd == null)\n              {\n                Context c1 = this.getFcnContext(fcn, args, c, s0, s1, EvalControl.Enabled, cm); // EvalControl.Enabled passed on to nested this.evalAppl\n                return this.enabled(fcn.body, acts, c1, s0, s1, cm);\n              }\n              fval = fcn.fcnRcd;\n            }\n            if (fval instanceof Applicable)\n            {\n              Applicable fcn = (Applicable) fval;\n              Value argVal = this.eval(args[1], c, s0, s1, EvalControl.Enabled, cm);\n              Value bval = fcn.apply(argVal, EvalControl.Enabled); // EvalControl.Enabled not taken into account by any subclass of Applicable\n              if (!(bval instanceof BoolValue))\n              {\n                Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING2, new String[] { "ENABLED", "boolean",\n                        pred.toString() }, args[1], c);\n              }\n              if (!((BoolValue) bval).val) {\n                return null;\n              }\n            } else\n            {\n              Assert.fail("In computing ENABLED, a non-function (" + fval.getKindString()\n                      + ") was applied as a function.\\n" + pred, pred, c);\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n        case OPCODE_ite: // IfThenElse\n          {\n            Value guard = this.eval(args[0], c, s0, s1, EvalControl.Enabled, cm);\n            if (!(guard instanceof BoolValue))\n            {\n              Assert.fail("In computing ENABLED, a non-boolean expression(" + guard.getKindString()\n                      + ") was used as the guard condition" + " of an IF.\\n" + pred, pred, c);\n            }\n            int idx = (((BoolValue) guard).val) ? 1 : 2;\n            return this.enabled(args[idx], acts, c, s0, s1, cm);\n          }\n        case OPCODE_sa: // SquareAct [A]_e\n          {\n            TLCState s2 = this.enabled(args[0], acts, c, s0, s1, cm);\n            if (s2 != null) {\n              return s2;\n            }\n            return this.enabledUnchanged(args[1], acts, c, s0, s1, cm);\n          }\n        case OPCODE_te: // TemporalExists\n        case OPCODE_tf: // TemporalForAll\n          {\n            Assert.fail("In computing ENABLED, TLC encountered temporal quantifier.\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_uc: // UnboundedChoose\n          {\n            Assert.fail("In computing ENABLED, TLC encountered unbounded CHOOSE. "\n                    + "Make sure that the expression is of form CHOOSE x \\\\in S: P(x).\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_ue: // UnboundedExists\n          {\n            Assert.fail("In computing ENABLED, TLC encountered unbounded quantifier. "\n                    + "Make sure that the expression is of form \\\\E x \\\\in S: P(x).\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_uf: // UnboundedForall\n          {\n            Assert.fail("In computing ENABLED, TLC encountered unbounded quantifier. "\n                    + "Make sure that the expression is of form \\\\A x \\\\in S: P(x).\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_sf: // SF\n          {\n            Assert.fail(EC.TLC_ENABLED_WRONG_FORMULA, new String[]{ "SF", pred.toString()}, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_wf: // WF\n          {\n            Assert.fail(EC.TLC_ENABLED_WRONG_FORMULA, new String[] { "WF", pred.toString() }, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_box:\n          {\n            Assert.fail(EC.TLC_ENABLED_WRONG_FORMULA, new String[] { "[]", pred.toString() }, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_diamond:\n          {\n            Assert.fail(EC.TLC_ENABLED_WRONG_FORMULA, new String[] { "<>", pred.toString() }, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_unchanged:\n          {\n            return this.enabledUnchanged(args[0], acts, c, s0, s1, cm);\n          }\n        case OPCODE_eq:\n          {\n            SymbolNode var = this.getPrimedVar(args[0], c, true);\n            if (var == null)\n            {\n              Value bval = this.eval(pred, c, s0, s1, EvalControl.Enabled, cm);\n              if (!((BoolValue) bval).val) {\n                return null;\n              }\n            } else\n            {\n              UniqueString varName = var.getName();\n              IValue lval = s1.lookup(varName);\n              Value rval = this.eval(args[1], c, s0, s1, EvalControl.Enabled, cm);\n              if (lval == null)\n              {\n                TLCState s2 = s1.bind(var, rval);\n                return this.enabled(acts, s0, s2, cm);\n              } else\n              {\n                if (!lval.equals(rval)) {\n                  return null;\n                }\n              }\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n        case OPCODE_implies:\n          {\n            Value bval = this.eval(args[0], c, s0, s1, EvalControl.Enabled, cm);\n            if (!(bval instanceof BoolValue))\n            {\n              Assert.fail("While computing ENABLED of an expression of the form" + " P => Q, P was "\n                      + bval.getKindString() + ".\\n" + pred, pred, c);\n            }\n            if (((BoolValue) bval).val)\n            {\n              return this.enabled(args[1], acts, c, s0, s1, cm);\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n        case OPCODE_cdot:\n          {\n            Assert.fail("The current version of TLC does not support action composition.", pred, c);\n            /***\n            TLCState s01 = TLCStateFun.Empty;\n            StateVec iss = new StateVec(0);\n            this.getNextStates(args[0], ActionItemList.Empty, c, s0, s01, iss);\n            int sz = iss.size();\n            for (int i = 0; i < sz; i++) {\n              s01 = iss.elementAt(i);\n              TLCState s2 = this.enabled(args[1], acts, c, s01, s1);\n              if (s2 != null) return s2;\n            }\n            ***/\n            return null; // make compiler happy\n          }\n        case OPCODE_leadto:\n          {\n            Assert.fail("In computing ENABLED, TLC encountered a temporal formula" + " (a ~> b).\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_arrow:\n          {\n            Assert.fail("In computing ENABLED, TLC encountered a temporal formula" + " (a -+-> formula).\\n" + pred, pred, c);\n            return null; // make compiler happy\n          }\n        case OPCODE_in:\n          {\n            SymbolNode var = this.getPrimedVar(args[0], c, true);\n            if (var == null)\n            {\n                Value bval = this.eval(pred, c, s0, s1, EvalControl.Enabled, cm);\n                if (!((BoolValue) bval).val) {\n                  return null;\n                }\n            } else\n            {\n              UniqueString varName = var.getName();\n              Value lval = (Value) s1.lookup(varName);\n              Value rval = this.eval(args[1], c, s0, s1, EvalControl.Enabled, cm);\n              if (lval == null)\n              {\n                if (!(rval instanceof Enumerable))\n                {\n                  Assert.fail("The right side of \\\\IN is not enumerable.\\n" + pred, pred, c);\n                }\n                ValueEnumeration Enum = ((Enumerable) rval).elements();\n                Value val;\n                while ((val = Enum.nextElement()) != null)\n                {\n                  TLCState s2 = s1.bind(var, val);\n                  s2 = this.enabled(acts, s0, s2, cm);\n                  if (s2 != null) {\n                    return s2;\n                  }\n                }\n                return null;\n              } else\n              {\n                if (!rval.member(lval)) {\n                  return null;\n                }\n              }\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n        // The following case added by LL on 13 Nov 2009 to handle subexpression names.\n        case OPCODE_nop:\n          {\n            return this.enabled(args[0], acts, c, s0, s1, cm);\n          }\n\n        default:\n          {\n            // We handle all the other builtin operators here.\n            Value bval = this.eval(pred, c, s0, s1, EvalControl.Enabled, cm);\n            if (!(bval instanceof BoolValue))\n            {\n              Assert.fail(EC.TLC_EXPECTED_EXPRESSION_IN_COMPUTING, new String[] { "ENABLED", "boolean",\n                      bval.toString(), pred.toString() }, pred, c);\n            }\n            if (((BoolValue) bval).val)\n            {\n              return this.enabled(acts, s0, s1, cm);\n            }\n            return null;\n          }\n        }\n  }\n\n  protected abstract TLCState enabledUnchanged(SemanticNode expr, ActionItemList acts,\n                                          Context c, TLCState s0, TLCState s1, CostModel cm);\n  \n  protected final TLCState enabledUnchangedImpl(SemanticNode expr, ActionItemList acts,\n            Context c, TLCState s0, TLCState s1, CostModel cm) {\n\t    if (coverage) {cm = cm.get(expr);}\n        SymbolNode var = this.getVar(expr, c, true, toolId);\n        if (var != null) {\n          // a state variable, e.g. UNCHANGED var1\n          UniqueString varName = var.getName();\n          Value v0 = this.eval(expr, c, s0, s1, EvalControl.Enabled, cm);\n          IValue v1 = s1.lookup(varName);\n          if (v1 == null) {\n            s1 = s1.bind(var, v0);\n            return this.enabled(acts, s0, s1, cm);\n          }\n          if (v1.equals(v0)) {\n            return this.enabled(acts, s0, s1, cm);\n          }\n          MP.printWarning(EC.TLC_UNCHANGED_VARIABLE_CHANGED, new String[]{varName.toString() , expr.toString()});\n          return null;\n        }\n\n        if (expr instanceof OpApplNode) {\n          OpApplNode expr1 = (OpApplNode)expr;\n          ExprOrOpArgNode[] args = expr1.getArgs();\n          int alen = args.length;\n          SymbolNode opNode = expr1.getOperator();\n          UniqueString opName = opNode.getName();\n          int opcode = BuiltInOPs.getOpCode(opName);\n\n          if (opcode == OPCODE_tup) {\n            // a tuple, e.g. UNCHANGED <<var1, var2>>\n            if (alen != 0) {\n              ActionItemList acts1 = acts;\n              for (int i = 1; i < alen; i++) {\n                acts1 = (ActionItemList) acts1.cons(args[i], c, cm, IActionItemList.UNCHANGED);\n              }\n              return this.enabledUnchanged(args[0], acts1, c, s0, s1, cm);\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n\n          if (opcode == 0 && alen == 0) {\n            // a 0-arity operator:\n            Object val = this.lookup(opNode, c, false);\n\n            if (val instanceof LazyValue) {\n              LazyValue lv = (LazyValue)val;\n              return this.enabledUnchanged(lv.expr, acts, lv.con, s0, s1, cm);\n            }\n            else if (val instanceof OpDefNode) {\n              return this.enabledUnchanged(((OpDefNode)val).getBody(), acts, c, s0, s1, cm);\n            }\n            else if (val == null) {\n              Assert.fail("In computing ENABLED, TLC found the undefined identifier\\n" +\n                          opName + " in an UNCHANGED expression at\\n" + expr, expr ,c);\n            }\n            return this.enabled(acts, s0, s1, cm);\n          }\n        }\n\n        final Value v0 = this.eval(expr, c, s0, TLCState.Empty, EvalControl.Enabled, cm);\n        // We are in ENABLED and primed but why pass only primed? This appears to\n        // be the only place where we call eval from the ENABLED scope without\n        // additionally passing EvalControl.Enabled. Not passing Enabled allows a \n        // cached LazyValue could be used (see comments above on line 1384).\n        // \n        // The current scope is a nested UNCHANGED in an ENABLED and evaluation is set\n        // to primed. However, UNCHANGED e equals e\' = e , so anything primed in e\n        // becomes double-primed in ENABLED UNCHANGED e. This makes it illegal TLA+\n        // which is rejected by SANY\'s level checking. A perfectly valid spec - where\n        // e is not primed - but that also causes this code path to be taken is 23 below:\n        // \n        // -------- MODULE 23 ---------\n        // VARIABLE t\n        // op(var) == var\n        // Next == /\\ (ENABLED (UNCHANGED op(t)))\n        //         /\\ (t\'= t)\n        // Spec == (t = 0) /\\ [][Next]_t\n        // ============================\n        // \n        // However, spec 23 causes the call to this.eval(...) below to throw an\n        // EvalException either with EvalControl.Primed. The exception\'s message is\n        // "In evaluation, the identifier t is either undefined or not an operator."\n        // indicating that this code path is buggy.\n        // \n        // If this bug is ever fixed to make TLC accept spec 23, EvalControl.Primed\n        // should likely be rewritten to EvalControl.setPrimed(EvalControl.Enabled)\n        // to disable reusage of LazyValues on line ~1384 above.\n\t\tfinal Value v1 = this.eval(expr, c, s1, TLCState.Empty, EvalControl.Primed, cm);\n        if (!v0.equals(v1)) {\n          return null;\n        }\n        return this.enabled(acts, s0, s1, cm);\n  }\n\n  /* This method determines if the action predicate is valid in (s0, s1). */\n  @Override\n  public final boolean isValid(Action act, TLCState s0, TLCState s1) {\n    Value val = this.eval(act.pred, act.con, s0, s1, EvalControl.Clear, act.cm);\n    if (!(val instanceof BoolValue)) {\n      Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", act.pred.toString()}, act.pred, act.con);\n    }\n    return ((BoolValue)val).val;\n  }\n\n  /* Returns true iff the predicate is valid in the state. */\n  @Override\n  public boolean isValid(Action act, TLCState state) {\n    return this.isValid(act, state, TLCState.Empty);\n  }\n\n  /* Returns true iff the predicate is valid in the state. */\n  @Override\n  public final boolean isValid(Action act) {\n    return this.isValid(act, TLCState.Empty, TLCState.Empty);\n  }\n\n    @Override\n\tpublic boolean isValid(ExprNode expr, Context ctxt) {\n\t    IValue val = this.eval(expr, ctxt, TLCState.Empty, TLCState.Empty, \n\t    \t\tEvalControl.Const, CostModel.DO_NOT_RECORD);\n\t    if (!(val instanceof BoolValue)) {\n\t      Assert.fail(EC.TLC_EXPECTED_VALUE, new String[]{"boolean", expr.toString()}, expr);\n\t    }\n\t    return ((BoolValue)val).val;\n\t}\n\n  @Override\n  public final boolean isValid(ExprNode expr) {\n\t  return isValid(expr, Context.Empty);\n  }\n\n  public boolean isValidAssumption(ExprNode assumption) {\n\t  return isValid(assumption);\n  }\n  \n  @Override\n  public final int checkAssumptions() {\n      final ExprNode[] assumps = getAssumptions();\n      final boolean[] isAxiom = getAssumptionIsAxiom();\n      for (int i = 0; i < assumps.length; i++)\n      {\n          try\n          {\n              if ((!isAxiom[i]) && !isValidAssumption(assumps[i]))\n              {\n                  return MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());\n              }\n          } catch (final Exception e)\n          {\n              // Assert.printStack(e);\n              return MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,\n                      new String[] { assumps[i].toString(), e.getMessage() });\n          }\n      }\n      return EC.NO_ERROR;\n  }\n\n\t@Override\n\tpublic final int checkPostCondition() {\n\t\treturn checkPostConditionWithContext(Context.Empty);\n\t}\n\n\t@Override\n\tpublic final int checkPostConditionWithCounterExample(final IValue value) {\n\t\tfinal SymbolNode def = getCounterExampleDef();\n\t\tif (def == null) {\n\t\t\t// TLCExt!CounterExample does not appear anywhere in the spec.\n\t\t\treturn checkPostCondition();\n\t\t}\n\t\tfinal Context ctxt = Context.Empty.cons(def, value);\n\t\treturn checkPostConditionWithContext(ctxt);\n\t}\n\n\tprivate final int checkPostConditionWithContext(final Context ctxt) {\n\t\t// User request: http://discuss.tlapl.us/msg03658.html\n\t\tfinal ExprNode[] postConditions = getPostConditionSpecs();\n\t\tfor (int i = 0; i < postConditions.length; i++) {\n\t\t\tfinal ExprNode en = postConditions[i];\n\t\t\ttry {\n\t\t\t\tif (!isValid(en, ctxt)) {\n\t\t\t\t\t// It\'s not an assumption because the expression doesn\'t appear inside\n\t\t\t\t\t// an ASSUME, but good enough for this prototype.\n\t\t\t\t\treturn MP.printError(EC.TLC_ASSUMPTION_FALSE, en.toString());\n\t\t\t\t}\n\t\t\t} catch (Exception e) {\n\t\t\t\t// tool.isValid(sn) failed to evaluate...\n\t\t\t\treturn MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,\n\t\t\t\t\t\tnew String[] { en.toString(), e.getMessage() });\n\t\t\t}\n\t\t}\n\t\t// The PostCheckAssumption/PostCondition cannot be stated as an ordinary\n\t\t// invariant\n\t\t// with the help of TLCSet/Get because the invariant will only be evaluated for\n\t\t// distinct states, but we want it to be evaluated after state-space exploration\n\t\t// finished. Hacking away with TLCGet("queue") = 0 doesn\'t work because the\n\t\t// queue\n\t\t// can be empty during the evaluation of the next-state relation when a worker\n\t\t// dequeues\n\t\t// the last state S, that has more successor states.\n\t\treturn EC.NO_ERROR;\n\t}\n  \n    /* Reconstruct the initial state whose fingerprint is fp. */\n\t@Override\n\tpublic final TLCStateInfo getState(final long fp) {\n\t\tclass InitStateSelectorFunctor implements IStateFunctor {\n\t\t\tprivate final long fp;\n\t\t\tpublic TLCState state;\n\t\t\tpublic InitStateSelectorFunctor(long fp) {\n\t\t\t\tthis.fp = fp;\n\t\t\t}\n\t\t\t@Override\n\t\t\tpublic Object addElement(TLCState state) {\n\t\t\t\tif (state == null) {\n\t\t\t\t\treturn null;\n\t\t\t\t} else if (this.state != null) {\n\t\t\t\t\t// Always return the first match found. Do not let later matches override\n\t\t\t\t\t// this.state. This is in line with the original implementation that called\n\t\t\t\t\t// getInitStates().\n\t\t\t\t\treturn null;\n\t\t\t\t} else if (fp == state.fingerPrint()) {\n\t\t\t\t\tthis.state = state;\n\t\t\t\t\t// TODO Stop generation of initial states preemptively. E.g. make the caller of\n\t\t\t\t\t// addElement check for a special return value such as this (the functor).\n\t\t\t\t}\n\t\t\t\treturn null;\n\t\t\t}\n\t\t}\n\t\t// Registry a selector that extract out of the (possibly) large set of initial\n\t\t// states the one identified by fp. The functor pattern has the advantage\n\t\t// compared to this.getInitStates(), that it kind of streams the initial states\n\t\t// to the functor whereas getInitStates() stores _all_ init states in a set\n\t\t// which is traversed afterwards. This is also consistent with\n\t\t// ModelChecker#DoInitFunctor. Using the functor pattern for the processing of\n\t\t// init states in ModelChecker#doInit but calling getInitStates() here results\n\t\t// in a bug during error trace generation when the set of initial states is too\n\t\t// large for getInitStates(). Earlier TLC would have refused to run the model\n\t\t// during ModelChecker#doInit.\n\t\tfinal InitStateSelectorFunctor functor = new InitStateSelectorFunctor(fp);\n\t\tthis.getInitStates(functor);\n\t\tfinal TLCState state = functor.state;\n\t\tif (state != null) {\n\t\t\tassert state.isInitial();\n\t\t\tfinal TLCStateInfo info = new TLCStateInfo(state);\n\t\t\tinfo.fp = fp;\n\t\t\treturn info;\n\t\t}\n\t\treturn null;\n\t}\n\n  /**\n\t * Reconstruct the next state of state s whose fingerprint is fp.\n\t *\n\t * @return Returns the TLCState wrapped in TLCStateInfo. TLCStateInfo stores\n\t *         the stateNumber (relative to the given sinfo) and a pointer to\n\t *         the predecessor.\n\t */\n  @Override\n  public final TLCStateInfo getState(long fp, TLCStateInfo sinfo) {\n    final TLCStateInfo tlcStateInfo = getState(fp, sinfo.state);\n    if (tlcStateInfo == null) {\n      throw new EvalException(EC.TLC_FAILED_TO_RECOVER_NEXT);\n    }\n    tlcStateInfo.stateNumber = sinfo.stateNumber + 1;\n    tlcStateInfo.predecessorState = sinfo;\n    tlcStateInfo.fp = fp;\n    return tlcStateInfo;\n  }\n\n  /* Reconstruct the next state of state s whose fingerprint is fp. */\n  @Override\n  public final TLCStateInfo getState(long fp, TLCState s) {\n\t  IdThread.setCurrentState(s);\n    for (int i = 0; i < this.actions.length; i++) {\n      Action curAction = this.actions[i];\n      StateVec nextStates = this.getNextStates(curAction, s);\n      for (int j = 0; j < nextStates.size(); j++) {\n        TLCState state = nextStates.elementAt(j);\n        long nfp = state.fingerPrint();\n        if (fp == nfp) {\n        \tstate.setPredecessor(s);\n        \tassert !state.isInitial();\n          return new TLCStateInfo(state, curAction);\n        }\n      }\n    }\n    return null;\n  }\n\n  /* Reconstruct the info for s1.   */\n  @Override\n  public final TLCStateInfo getState(TLCState s1, TLCState s) {\n\t  IdThread.setCurrentState(s);\n    for (int i = 0; i < this.actions.length; i++) {\n      Action curAction = this.actions[i];\n      StateVec nextStates = this.getNextStates(curAction, s);\n      for (int j = 0; j < nextStates.size(); j++) {\n        TLCState state = nextStates.elementAt(j);\n        try {\n        \tif (s1.equals(state)) {\n        \t\tstate.setPredecessor(s);\n        \t\tassert !state.isInitial();\n        \t\treturn new TLCStateInfo(state, curAction);\n        \t}\n        } catch (TLCRuntimeException e) {\n          // s might have two or more successors, whose values are incomparable to the\n          // values of s1 (https://github.com/tlaplus/tlaplus/issues/743). Assume s\n          // to equal <<"foo", 3>> and its two successor states t1 to equal <<"foo", 4>>\n          // and t2 to equal <<TRUE, 5>>. t1 and s1 equal to <<TRUE, 5>> are incomparable. \n          // and t2 to equal <<TRUE, 5>>. t1 and s1 equal to <<TRUE, 5>> are incomparable. \n          // Next ==\n          // \\/ /\\ x\' = "foo"\n          //    /\\ y\' = y + 1\n          // \\/ /\\ x\' = TRUE\n          //    /\\ y\' = y + 2\n        \tcontinue;\n        }\n      }\n    }\n    return null;\n  }\n\n  /* Return the set of all permutations under the symmetry assumption. */\n  @Override\n  public final IMVPerm[] getSymmetryPerms() {\n    final String name = this.config.getSymmetry();\n    if (name.length() == 0) { return null; }\n    final Object symm = this.unprocessedDefns.get(name);\n    if (symm == null) {\n      Assert.fail(EC.TLC_CONFIG_SPECIFIED_NOT_DEFINED, new String[] { "symmetry function", name});\n    }\n    if (!(symm instanceof OpDefNode)) {\n      Assert.fail("The symmetry function " + name + " must specify a set of permutations.");\n    }\n    final OpDefNode opDef = (OpDefNode)symm;\n    // This calls tlc2.module.TLC.Permutations(Value) and returns a Value of |fcns|\n    // = n! where n is the capacity of the symmetry set.\n    final IValue fcns = this.eval(opDef.getBody(), Context.Empty, TLCState.Empty, CostModel.DO_NOT_RECORD);\n    if (!(fcns instanceof Enumerable) || !(fcns instanceof SetEnumValue)) {\n      Assert.fail("The symmetry operator must specify a set of functions.", opDef.getBody());\n    }\n    final List<Value> values = ((SetEnumValue)fcns).elements().all();\n    for (final Value v : values) {\n    \tif (!(v instanceof FcnRcdValue)) {\n    \t\tAssert.fail("The symmetry values must be function records.", opDef.getBody());\n    \t}\n    }\n    final ExprOrOpArgNode[] argNodes = ((OpApplNode)opDef.getBody()).getArgs();\n    // In the case where the config defines more than one set which is symmetric, they will pass through the\n    //\t\tenumerable size() check even if they are single element sets\n    final StringBuilder cardinalityOneSetList = new StringBuilder();\n    int offenderCount = 0;\n    if (argNodes.length >= values.size()) {\n    \t// If equal, we have as many values as we have permuted sets => we have all 1-element sets;\n    \t//\t\tif greater than, then we have a heterogenous cardinality of sets, including 0 element sets.\n    \tfor (final ExprOrOpArgNode node : argNodes) {\n\t\t\taddToSubTwoSizedSymmetrySetList(node, cardinalityOneSetList);\n\t\t\toffenderCount++;\n    \t}\n    }\n    \n    final IMVPerm[] subgroup;\n    if (offenderCount == 0) {\n        subgroup = MVPerms.permutationSubgroup((Enumerable)fcns);\n        final HashSet<ModelValue> subgroupMembers = new HashSet<>();\n        for (final IMVPerm imvp : subgroup) {\n        \tif (imvp instanceof MVPerm) { // should always be the case\n        \t\tsubgroupMembers.addAll(((MVPerm)imvp).getAllModelValues());\n        \t}\n        }\n        for (final ExprOrOpArgNode node : argNodes) {\n        \tfinal SetEnumValue enumValue = getSetEnumValueFromArgumentNode(node);\n        \t\n        \tif (enumValue != null) {\n        \t\tfinal ValueEnumeration ve = enumValue.elements();\n        \t\t\n        \t\tboolean found = false;\n        \t\tValue v;\n        \t\twhile ((v = ve.nextElement()) != null) {\n        \t\t\tif ((v instanceof ModelValue) && subgroupMembers.contains(v)) {\n        \t\t\t\tfound = true;\n        \t\t\t\tbreak;\n        \t\t\t}\n        \t\t}\n        \t\t\n        \t\tif (!found) {\n    \t\t\t\taddToSubTwoSizedSymmetrySetList(node, cardinalityOneSetList);\n    \t\t\t\toffenderCount++;\n        \t\t}\n        \t}\n        }\n    } else {\n    \tsubgroup = null;\n    }\n    \n    if (offenderCount > 0) {\n      final String plurality = (offenderCount > 1) ? "s" : "";\n      final String antiPlurality = (offenderCount > 1) ? "" : "s";\n      final String toHaveConjugation = (offenderCount > 1) ? "have" : "has";\n      \n      MP.printWarning(EC.TLC_SYMMETRY_SET_TOO_SMALL,\n    \t\t  \t  \t  new String[] { plurality, cardinalityOneSetList.toString(), toHaveConjugation, antiPlurality });\n    }\n    \n    return subgroup;\n  }\n  \n  /**\n   * Teases the original spec name for the set out of node and appends it to the {@code StringBuilder} instance.\n   */\n  private void addToSubTwoSizedSymmetrySetList(final ExprOrOpArgNode node, final StringBuilder cardinalityOneSetList) {\n\t\tfinal SyntaxTreeNode tn = (SyntaxTreeNode)node.getTreeNode();\n\t\tfinal String image = tn.getHumanReadableImage();\n\t\tfinal String alias;\n\t    if (image.startsWith(TLAConstants.BuiltInOperators.PERMUTATIONS)) {\n\t\t  final int imageLength = image.length();\n\t\t  alias = image.substring((TLAConstants.BuiltInOperators.PERMUTATIONS.length() + 1),\n\t\t\t\t  \t\t\t\t\t\t  (imageLength - 1));\n\t    } else {\n\t    \talias = image;\n\t    }\n\t\tfinal String specDefinitionName = this.config.getOverridenSpecNameForConfigName(alias);\n\t\tfinal String displayDefinition = (specDefinitionName != null) ? specDefinitionName : alias;\n\t\t\n\t\tif (cardinalityOneSetList.length() > 0) {\n\t\t\tcardinalityOneSetList.append(", and ");\n\t\t}\n\n\t\tcardinalityOneSetList.append(displayDefinition);\n  }\n  \n  /**\n   * @param node\n   * @return if the node represents a permutation, this will return the {@link SetEnumValue} instance contains its\n   * \t\t\t\t\tmodel values\n   */\n  private SetEnumValue getSetEnumValueFromArgumentNode(final ExprOrOpArgNode node) {\n\t  if (node instanceof OpApplNode) {\n\t\t  final OpApplNode permutationNode = (OpApplNode)node;\n\t\t  if (permutationNode.getOperator() instanceof OpDefNode) {\n\t\t\t  final OpDefNode operator = (OpDefNode)permutationNode.getOperator();\n\t\t\t  if (TLAConstants.BuiltInOperators.PERMUTATIONS.equals(operator.getName().toString())) {\n\t\t\t\t  final ExprOrOpArgNode[] operands = permutationNode.getArgs();\n\t\t\t\t  if ((operands.length == 1)\n\t\t\t\t\t\t  && (operands[0] instanceof OpApplNode)\n\t\t\t\t\t\t  && (((OpApplNode)operands[0]).getOperator() instanceof OpDefOrDeclNode)) {\n\t\t\t\t\t  final Object o = ((OpDefOrDeclNode)((OpApplNode)operands[0]).getOperator()).getToolObject(toolId);\n\t\t\t\t\t  \n\t\t\t\t\t  if (o instanceof SetEnumValue) {\n\t\t\t\t\t\t  return (SetEnumValue)o;\n\t\t\t\t\t  } else if (o instanceof WorkerValue) {\n\t\t\t\t\t\t  // If TLC was started with a -workers N specification, N > 1, o will be a WorkerValue instance\n\t\t\t\t\t\t  final WorkerValue wv = (WorkerValue)o;\n\t\t\t\t\t\t  final Object unwrapped = WorkerValue.mux(wv);\n\t\t\t\t\t\t  \n\t\t\t\t\t\t  if (unwrapped instanceof SetEnumValue) {\n\t\t\t\t\t\t\t  return (SetEnumValue)unwrapped;\n\t\t\t\t\t\t  }\n\t\t\t\t\t  }\n\t\t\t\t  }\n\t\t\t  }\n\t\t  }\n\t  }\n\n\t  return null;\n  }\n\n  @Override\n  public final boolean hasSymmetry() {\n    if (this.config == null) {\n      return false;\n    }\n    final String name = this.config.getSymmetry();\n    return name.length() > 0;\n  }\n  @Override\n  public final Context getFcnContext(IFcnLambdaValue fcn, ExprOrOpArgNode[] args,\n          Context c, TLCState s0, TLCState s1,\n          final int control) {\n\t  return getFcnContext(fcn, args, c, s0, s1, control, CostModel.DO_NOT_RECORD);\n  }\n\n  @Override\n  public final Context getFcnContext(IFcnLambdaValue fcn, ExprOrOpArgNode[] args,\n                                     Context c, TLCState s0, TLCState s1,\n                                     final int control, CostModel cm) {\n    Context fcon = fcn.getCon();\n    int plen = fcn.getParams().length();\n    FormalParamNode[][] formals = fcn.getParams().getFormals();\n    Value[] domains = (Value[]) fcn.getParams().getDomains();\n    boolean[] isTuples = fcn.getParams().isTuples();\n    Value argVal = this.eval(args[1], c, s0, s1, control, cm);\n\n    if (plen == 1) {\n      if (!domains[0].member(argVal)) {\n        Assert.fail("In applying the function\\n" + Values.ppr(fcn.toString()) +\n                    ",\\nthe first argument is:\\n" + Values.ppr(argVal.toString()) +\n                    "which is not in its domain.\\n" + args[0], args[0], c);\n      }\n      if (isTuples[0]) {\n        FormalParamNode[] ids = formals[0];\n        TupleValue tv = (TupleValue) argVal.toTuple();\n        if (tv == null || argVal.size() != ids.length) {\n          Assert.fail("In applying the function\\n" + Values.ppr(this.toString()) +\n                      ",\\nthe argument is:\\n" + Values.ppr(argVal.toString()) +\n                      "which does not match its formal parameter.\\n" + args[0], args[0], c);\n        }\n        Value[] elems = tv.elems;\n        for (int i = 0; i < ids.length; i++) {\n          fcon = fcon.cons(ids[i], elems[i]);\n        }\n      }\n      else {\n        fcon = fcon.cons(formals[0][0], argVal);\n      }\n    }\n    else {\n      TupleValue tv = (TupleValue) argVal.toTuple();\n      if (tv == null) {\n        Assert.fail("Attempted to apply a function to an argument not in its" +\n                    " domain.\\n" + args[0], args[0], c);\n      }\n      int argn = 0;\n      Value[] elems = tv.elems;\n      for (int i = 0; i < formals.length; i++) {\n        FormalParamNode[] ids = formals[i];\n        Value domain = domains[i];\n        if (isTuples[i]) {\n          if (!domain.member(elems[argn])) {\n            Assert.fail("In applying the function\\n" + Values.ppr(fcn.toString()) +\n                        ",\\nthe argument number " + (argn+1) + " is:\\n" +\n                        Values.ppr(elems[argn].toString()) +\n                        "\\nwhich is not in its domain.\\n" + args[0], args[0], c);\n          }\n          TupleValue tv1 = (TupleValue) elems[argn++].toTuple();\n          if (tv1 == null || tv1.size() != ids.length) {\n            Assert.fail("In applying the function\\n" + Values.ppr(fcn.toString()) +\n                        ",\\nthe argument number " + argn + " is:\\n" +\n                        Values.ppr(elems[argn-1].toString()) +\n                        "which does not match its formal parameter.\\n" + args[0], args[0], c);\n          }\n          Value[] avals = tv1.elems;\n          for (int j = 0; j < ids.length; j++) {\n            fcon = fcon.cons(ids[j], avals[j]);\n          }\n        }\n        else {\n          for (int j = 0; j < ids.length; j++) {\n            if (!domain.member(elems[argn])) {\n              Assert.fail("In applying the function\\n" + Values.ppr(fcn.toString()) +\n                          ",\\nthe argument number " + (argn+1) + " is:\\n" +\n                          Values.ppr(elems[argn].toString()) +\n                          "which is not in its domain.\\n" + args[0], args[0], c);\n            }\n            fcon = fcon.cons(ids[j], elems[argn++]);\n          }\n        }\n      }\n    }\n    return fcon;\n  }\n\n  @Override\n  public final IContextEnumerator contexts(OpApplNode appl, Context c, TLCState s0,\n          TLCState s1, final int control) {\n\t  return contexts(appl, c, s0, s1, control, CostModel.DO_NOT_RECORD);\n  }\n\n  /* A context enumerator for an operator application. */\n  public final ContextEnumerator contexts(OpApplNode appl, Context c, TLCState s0,\n                                          TLCState s1, final int control, CostModel cm) {\n    return contexts(Ordering.NORMALIZED, appl, c, s0, s1, control, cm);\n  }\n\n\tprivate final ContextEnumerator contexts(Ordering ordering, OpApplNode appl, Context c, TLCState s0, TLCState s1, final int control,\n\t\t\tCostModel cm) {\n\t\tFormalParamNode[][] formals = appl.getBdedQuantSymbolLists();\n\t    boolean[] isTuples = appl.isBdedQuantATuple();\n\t    ExprNode[] domains = appl.getBdedQuantBounds();\n\t\n\t    int flen = formals.length;\n\t    int alen = 0;\n\t    for (int i = 0; i < flen; i++) {\n\t      alen += (isTuples[i]) ? 1 : formals[i].length;\n\t    }\n\t    Object[] vars = new Object[alen];\n\t    ValueEnumeration[] enums = new ValueEnumeration[alen];\n\t    int idx = 0;\n\t    for (int i = 0; i < flen; i++) {\n\t      Value boundSet = this.eval(domains[i], c, s0, s1, control, cm);\n\t      if (!(boundSet instanceof Enumerable)) {\n\t        Assert.fail("TLC encountered a non-enumerable quantifier bound\\n" +\n\t                    Values.ppr(boundSet.toString()) + ".\\n" + domains[i], domains[i], c);\n\t      }\n\t      FormalParamNode[] farg = formals[i];\n\t      if (isTuples[i]) {\n\t        vars[idx] = farg;\n\t        enums[idx++] = ((Enumerable)boundSet).elements(ordering);\n\t      }\n\t      else {\n\t        for (int j = 0; j < farg.length; j++) {\n\t          vars[idx] = farg[j];\n\t          enums[idx++] = ((Enumerable)boundSet).elements(ordering);\n\t        }\n\t      }\n\t    }\n\t    return new ContextEnumerator(vars, enums, c);\n\t}\n\n    // These three are expected by implementing the {@link ITool} interface; they used\n    //\t\tto mirror exactly methods that our parent class ({@link Spec}) implemented\n    //\t\thowever those methods have changed signature with refactoring done for \n    //\t\tIssue #393\n\t@Override\n\tpublic Context getOpContext(OpDefNode odn, ExprOrOpArgNode[] args, Context ctx, boolean b) {\n\t\treturn getOpContext(odn, args, ctx, b, toolId);\n\t}\n\t\n\t@Override\n\tpublic Object lookup(SymbolNode opNode, Context con, boolean b) {\n\t\treturn lookup(opNode, con, b, toolId);\n\t}\n\t\n\t@Override\n\tpublic Object getVal(ExprOrOpArgNode expr, Context con, boolean b) {\n\t\treturn getVal(expr, con, b, toolId);\n\t}\n\n\tpublic static boolean isProbabilistic() {\n\t\treturn PROBABLISTIC;\n\t}\n}\n', 'message': 'Debug the next-state relation.\n\n[Feature][Debugger]\n', 'author_name': 'Markus Alexander Kuppe', 'lang': 'lamport'}