Differences

This shows you the differences between two versions of the page.

--- creating:actions [2025/06/06 22:01] – Handle basic x' = expr case ahelwer
+++ creating:actions [2025/11/03 23:08] (current) – One more instanceof-cast ahelwer
@@ Line 45: / Line 45: @@
     ));
 </code>
 Then use the old ''do''/''while'' trick to parse comma-separated variable names in the ''declaration()'' method of the ''Parser'' class:
 <code java [highlight_lines_extra="4,5,6,7,8,9,10"]>
@@ Line 62: / Line 63: @@
 Before we can define a ''Stmt.VarDecl'' visitor, we need to come up with a way to manage variables & states.
-It's simplest to copy the ''Environment'' approach and record the current state as a field in the ''Interpreter'' class:
+The interpreter must keep track of only two states: the current state, and the next state.
-<code java [highlight_lines_extra="6"]>
+Each state is a mapping from strings - representing variables - to values.
+The interpreter also must keep track of the set of declared variables.
+For this we add three new fields near the top of the ''Interpreter'' class:
+<code java [highlight_lines_extra="6,7,8"]>
 class Interpreter implements Expr.Visitor<Object>,
                              Stmt.Visitor<Void> {
   final Environment globals;
   private Environment environment;
-  private final PrintStream out;
-  private State state = new State();
+  private final Map<String, Token> variables = new HashMap<>();
+  private Map<String, Object> current = null;
+  private Map<String, Object> next = new HashMap<>();
 </code>
-This requires a new class!
+We choose to initialize the ''current'' state to ''null'' because when the interpreter is created, the system's initial state has not yet been defined.
-Create a file called ''State.java''; for now, this just supports the ability to declare variables; it also produces an error if the user attempts to declare the same variable twice:
+The system's initial state will be built in ''next'', which then eventually becomes ''current''.
-<code java>
-package tla;
-import java.util.HashMap;
-import java.util.Map;
-class State {
-  private Map<String, Token> variables = new HashMap<>();
-  boolean isDeclared(Token name) {
-    return variables.containsKey(name.lexeme);
-  }
-  void declareVariable(Token name) {
-    if (isDeclared(name)) {
-      throw new RuntimeError(name, "Redeclared state variable.");
-    }
-    variables.put(name.lexeme, name);
-  }
-}
-</code>
-That's enough to implement ''visitVarDeclStmt()'' in the ''Interpreter'' class:
+The new fields are enough to implement ''visitVarDeclStmt()'' in the ''Interpreter'' class:
 <code java>
   @Override
@@ Line 103: / Line 87: @@
     checkNotDefined(stmt.names);
     for (Token name : stmt.names) {
-      state.declareVariable(name);
+      variables.put(name.lexeme, name);
+      next.put(name.lexeme, new UnboundVariable(name));
     }
@@ Line 110: / Line 95: @@
 </code>
-In intepreter mode we continue to support redefining operators, but will produce an error if the user attempts to redefine an operator as a state variable or vice versa.
+This requires a new datatype!
-Add this check to the ''visitOpDefStmt()'' method of the ''Interpreter'' class:
+What is the value of a variable when it is declared but not yet bound to a value?
-<code java [highlight_lines_extra="2,3,4"]>
+It must be a new null type, which we will call ''UnboundVariable''.
+Add ''UnboundVariable'' as a new record type near the top of the ''Interpreter'' class:
+<code java [highlight_lines_extra="4,5,6,7,8,9"]>
+class Interpreter implements Expr.Visitor<Object>,
+                             Stmt.Visitor<Void> {
+  private record UnboundVariable(Token name) {
+    @Override
+    public String toString() {
+      return name.lexeme;
+    }
+  }
+  final Environment globals;
+</code>
+It's important to keep variable declarations & operator definitions disjoint.
+In interpreter mode we continue to support redefining operators, but should produce an error if the user attempts to redefine an operator as a state variable or vice versa.
+Add the highlighted code to ''visitOpDefStmt()'' in the ''Interpreter'' class:
+<code java [highlight_lines_extra="9,10,11"]>
   public Void visitOpDefStmt(Stmt.OpDef stmt) {
-    if (state.isDeclared(stmt.name)) {
+    checkNotDefined(stmt.params);
+    for (Token param : stmt.params) {
+      if (param.lexeme.equals(stmt.name.lexeme)) {
+        throw new RuntimeError(param, "Identifier already in use.");
+      }
+    }
+    if (variables.containsKey(stmt.name.lexeme)) {
       throw new RuntimeError(stmt.name, "State variable redeclared as operator.");
     }
     TlaOperator op = new TlaOperator(stmt);
-    environment.define(stmt.name, op);
 </code>
@@ Line 130: / Line 140: @@
       }
-      if (state.isDeclared(name)) {
+      if (variables.containsKey(name.lexeme)) {
         throw new RuntimeError(name, "Name conflicts with state variable.");
       }
@@ Line 136: / Line 146: @@
 </code>
-===== Initializing State Variables =====
+===== Reading, Priming, & Setting State Variables =====
-Now that we can declare variables, what value are they initialized to?
+To resolve variable values, modify the ever-more-complicated ''visitVariableExpr()'' method of the ''Interpreter'' class to first check whether it's resolving a variable, falling back to an ''environment'' lookup if not:
-We've successfully dodged this issue for a very long time in this tutorial series, but unfortunately the initial value of these variables is undefined.
+<code java [highlight_lines_extra="2,3,4,5"]>
-That means we will need a null value type.
+  public Object visitVariableExpr(Expr.Variable expr) {
-We've avoided null types thus far, which means we haven't had to do as many checks before using values in the interpreter - a real luxury!
+    Object referent =
-Alas we now depart this wonderful land.
+      variables.containsKey(expr.name.lexeme)
-Create a new class, ''UnboundVariable.java'':
+      ? (primed ? next : current).get(expr.name.lexeme)
-<code java>
+      : environment.get(expr.name);
-package tla;
-record UnboundVariable(Token name, boolean primed) {
+    if (!(referent instanceof TlaCallable)) {
-  @Override
-  public String toString() {
-    return name.lexeme + (primed ? "'" : "");
-  }
-}
 </code>
-In the ''State'' class, we need to track variable values for the current & next states; add one ''Map<>'' instance for each:
+This makes use of yet another field we must add to the ''Interpreter'' class, ''primed'':
-<code java [highlight_lines_extra="3,4"]>
+<code java [highlight_lines_extra="2"]>
-class State {
-  private Map<String, Token> variables = new HashMap<>();
-  private Map<String, Object> current = new HashMap<>();
   private Map<String, Object> next = new HashMap<>();
+  private boolean primed = true;
+  public Interpreter(boolean replMode) {
 </code>
-Then, in ''declareVariable()'', initialize the variables to instances of ''UnboundVariable'':
+The ''primed'' field controls whether variable values are pulled from the ''current'' or ''next'' states.
-<code java [highlight_lines_extra="2,3,4"]>
+When inside a primed expression, variables are pulled from ''next''; when outside of primed expressions, variables are pulled from ''current''.
-    variables.put(name.lexeme, name);
+The ''primed'' field is initialized to ''true'', since the interpreter builds the system's initial state in the ''next'' field so we want all expressions to be implicitly primed at first.
-    current.put(name.lexeme, new UnboundVariable(name, false));
+We can now finally define the prime operator for real, in ''visitUnaryExpr()'' in the ''Interpreter'' class:
-    next.put(name.lexeme, new UnboundVariable(name, true));
+<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12,13,14"]>
+  public Object visitUnaryExpr(Expr.Unary expr) {
+    switch (expr.operator.type) {
+      case PRIME: {
+        if (primed) {
+          throw new RuntimeError(expr.operator,
+              current == null
+              ? "Cannot prime expression in initial state."
+              : "Cannot double-prime expression.");
+        } try {
+          primed = true;
+          return evaluate(expr.expr);
+        } finally {
+          primed = false;
+        }
+      } case ENABLED: {
+</code>
+Double-priming an expression or priming an expression in the initial state are both fatal errors in TLA⁺.
+The meaning of priming an expression is that all state variables within that expression are primed, so the way the expression is evaluated is fundamentally changed.
+This is why the prime operator somewhat uniquely modifies the state of the ''Interpreter'' instance itself.
+Similar to in ''executeBlock()'', we wrap this ''Interpreter'' state modification inside a ''try''/''finally'' block to ensure that if the evaluation produces a runtime exception, ''primed'' is reset to ''false'' so the ''Interpreter'' instance is not left in a corrupted state.
+We can retrieve state variable values, but what about assigning them?
+To start, let's handle the simple case of expressions of the form ''x' = expr''.
+This requires modifying the ''EQUAL'' case of ''visitBinaryExpr()'' in the ''Interpreter'' class.
+If the ''left'' operand is an ''UnboundVariable'' instance, then bind the ''left'' state variable to the value of ''right'':
+<code java [highlight_lines_extra="2,3,4,5"]>
+      case EQUAL:
+        if (left instanceof UnboundVariable var) {
+          next.put(var.name().lexeme, right);
+          return true;
+        }
+        return left.equals(right);
+</code>
+We only modify variable values in ''next'', not ''current''; variable values in ''current'' should be considered immutable, and we will never let an ''UnboundVariable'' value into the ''current'' state.
+===== Nondeterminism =====
+In TLA⁺, states generally do not have only one successor state.
+Instead, there are usually multiple possible states to transition to.
+This is called nondeterminism, and is a key TLA⁺ feature enabling modeling of concurrent scheduling & much more.
+Nondeterminism is expressed in TLA⁺ through the use of disjunction; for example:
+<code haskell>
+Action ==
+  \/ x' = 0
+  \/ x' = 1
+</code>
+The ''Action'' predicate matches next states where ''x'' is //either// 0 or 1.
+This means ''Action'' represents a nondeterministic step where the system can arbitrarily move to a state where ''x'' is 0, or a state where ''x'' is 1.
+Currently, we store the next state in a single field in the ''Interpreter'' class.
+How can we represent & compute with multiple possible next states?
+The answer is to add another field to the ''Interpreter'' class, holding the set of identified possible next states:
+<code java [highlight_lines_extra="3"]>
+  private Map<String, Object> current = null;
+  private Map<String, Object> next = new HashMap<>();
+  private Set<Map<String, Object>> possibleNext = new HashSet<>();
+  private boolean primed = true;
+  public Interpreter(boolean replMode) {
+</code>
+When our interpreter finds multiple possible next states, it tosses them into ''possibleNext'' for later consideration and continues evaluating & binding the variables in the next state currently under construction.
+Then some top-level loop churns through the ''possibleNext'' set, either ruling out or accepting each possible next state until none remain.
+We will write this very critical top-level loop now; create a new method ''getNextStates()'' in the ''Interpreter'' class:
+<code java>
+  List<Map<String, Object>> getNextStates(Token location, Expr action) {
   }
 </code>
-===== Getting State Variables =====
+''getNextStates()'' will use the following algorithm:
+  - Clear the ''next'' state and push it onto ''possibleNext''
+  - While states remain in ''possibleNext'', choose one, set it as ''next'', and evaluate ''action''
+  - If ''action'' evaluates to ''true'' and also results in a complete ''next'' state with all variables bound to values, add ''next'' to a set of confirmed next states
+  - Evaluating ''action'' might have pushed more states onto ''possibleNext'', so repeat the process until ''possibleNext'' is empty
+  - Return the set of confirmed next states
-To retrieve variable values, modify the ever-more-complicated ''visitVariableExpr()'' method of the ''Interpreter'' class to call a new ''getValue()'' helper; if the value resolves to an ''UnboundVariable'' instance, return it immediately:
+Here's how we set up everything outside of the central loop:
-<code java [highlight_lines_extra="2,4,5,6"]>
+<code java [highlight_lines_extra="2,3,4,5,6,8,9,10,11,13"]>
-  public Object visitVariableExpr(Expr.Variable expr) {
+  List<Map<String, Object>> getNextStates(Token location, Expr action) {
-    Object referent = getValue(expr.name);
+    Set<Map<String, Object>> confirmedNext = new HashSet<>();
+    clearNext();
+    possibleNext.add(new HashMap<>(next));
+    try {
+      while (!possibleNext.isEmpty()) {
-    if (referent instanceof UnboundVariable) {
+      }
-      return referent;
+    } finally {
+      clearNext();
     }
-    if (!(referent instanceof TlaCallable)) {
+    return new ArrayList<>(confirmedNext);
+  }
 </code>
-The new ''getValue()'' helper merges lookup logic for state variables & operators; these should be disjoint, although state variable values are checked first:
+We use the familiar ''try''/''finally'' approach when evaluating expressions within a modified ''Interpreter'' state to ensure runtime exceptions do not corrupt the ''Interpreter'' instance.
+We also use the ''new HashMap<>(next)'' copy constructor to copy ''next'' before putting it in ''possibleNext'', which avoids a //very// subtle bug: since evaluating the action modifies the values in ''next'', and we put ''next'' into a ''HashMap<>'' which records its position by calculating a hash of the value of ''next'', if we subsequently modify the same object put into the ''HashMap<>'' then that value will get "lost" in the datastructure, because its hash value changed.
+For more on this peculiar issue, consult the Java ''[[https://docs.oracle.com/javase/8/docs/api/java/util/Map.html|Map<>]]'' documentation which warns against using mutable objects as keys.
+This code also requires a new ''clearNext()'' helper method in the ''Interpreter'' class, which does what you might expect from the name; it clears ''possibleNext'' then unbinds all variables in ''next'':
 <code java>
-  private Object getValue(Token name) {
+  private void clearNext() {
-    if (state.isDeclared(name)) {
+    possibleNext = new HashSet<>();
-      return state.getValue(name);
+    next = new HashMap<>();
+    for (Token variable : variables.values()) {
+      next.put(variable.lexeme, new UnboundVariable(variable));
     }
-    return environment.get(name);
   }
 </code>
-To define ''getValue()'' in the ''State'' class we need to determine whether to pull state variable values from ''current'' or ''next''.
+Now we can write the central ''getNextStates()'' loop:
-For this there must be some way of tracking whether we are currently inside a primed expression.
+<code java [highlight_lines_extra="2,3,4,5,6,7"]>
-Not just variables can be primed in TLA⁺, entire expressions can be!
+      while (!possibleNext.isEmpty()) {
-The meaning of a primed expression is that every state variable within that expression is primed.
+        Map<String, Object> trunk = possibleNext.iterator().next();
-This is tracked with a boolean class variable in ''State'', which is initialized to false:
+        next = new HashMap<>(trunk);
-<code java [highlight_lines_extra="2"]>
+        Object satisfied = evaluate(action);
-class State {
+        checkBooleanOperand(location, satisfied);
-  private boolean primed = false;
+        if ((boolean)satisfied && isComplete()) confirmedNext.add(next);
-  private Map<String, Token> variables = new HashMap<>();
+        possibleNext.remove(trunk);
+      }
 </code>
-Now define ''getValue()'' in the ''State'' class.
+Note again the judicious use of ''HashMap<>'' copy constructors to avoid the mutable ''HashMap<>'' key bug.
-If ''primed'' is true, we retrieve the state variable value from ''next''; if false, we retrieve it from ''current'':
+This code requires yet another ''Interpreter'' helper method to check whether a next state candidate is complete (has all variables assigned to concrete values):
 <code java>
-  Object getValue(Token name) {
+  private boolean isComplete() {
-    return (primed ? next : current).get(name.lexeme);
+    return !variables.isEmpty() && next.values().stream()
+        .noneMatch(v -> v instanceof UnboundVariable);
   }
 </code>
-===== Setting State Variables =====
+It's worth spending some time considering the ''getNextStates()'' method.
+From a pure functional perspective the approach is quite displeasing; our interpreter isn't just evaluating expressions anymore, it's also spewing out a bunch of half-baked states on the side.
+This side-effectful method makes it quite a bit harder to reason about the current state of our interpreter, but within the limitations of the Java language the method is appropriate.
-We can retrieve state variable values, but what about assigning them?
+There is also the question of termination.
-To start, let's handle the simple case of expressions of the form ''x = expr'' or ''x' = expr''.
+What is preventing ''getNextStates()'' from entering an infinite loop?
-This requires modifying the ''EQUAL'' case of ''visitBinaryExpr()'' in the ''Interpreter'' class.
+The answer is that we only add a state to ''possibleNext'' if either it is //already// in ''possibleNext'' (in which case it is de-duplicated) or after binding the value of at least one more variable than is bound in the ''next'' state under consideration.
-If the ''left'' operand is an ''UnboundVariable'' instance, then bind the ''left'' state variable to the value of ''right'':
+Thus the number of variables bound to concrete values in ''possibleNext'' increases monotonically, eventually encompassing all declared variables and terminating the loop.
-<code java [highlight_lines_extra="2,3,4,5,6"]>
-      case EQUAL:
+Let's get concrete.
-        if (left instanceof UnboundVariable) {
+How do we add states to ''possibleNext'' while evaluating disjunction?
-          UnboundVariable var = (UnboundVariable)left;
+For each disjunct, we use a fresh copy of the ''next'' state, then evaluate the disjunct and add the resulting modified ''next'' state to ''possibleNext''.
-          state.bindValue(var, right);
+As described above, this state will either already be in ''possibleNext'' (so be de-duplicated) or have bound the value of at least one more state variable.
-          return true;
+We need to evaluate every disjunct to ensure we find all possible next states, which is why TLA⁺ disjunction does not short-circuit.
+Modify the ''OR'' handling code in ''visitVariadicExpr()'' as highlighted:
+<code java [highlight_lines_extra="3,5,8"]>
+      case OR:
+        boolean result = false;
+        Map<String, Object> trunk = next;
+        for (Expr disjunct : expr.parameters) {
+          next = new HashMap<>(trunk);
+          Object junctResult = evaluate(disjunct);
+          checkBooleanOperand(expr.operator, junctResult);
+          possibleNext.add(new HashMap<>(next));
+          result |= (boolean)junctResult;
         }
-        return left.equals(right);
+        return result;
+      default:
 </code>
-Define ''bindValue()'' in the ''State'' class, which binds the variable's value in ''next'' if the ''UnboundVariable'' instance is primed and ''current'' if it is not:
+There are two other operators to support for binding state variables: the set membership ''\in'' operator, and the ''\E'' existential quantification operator.
-<code java>
+Actions like ''x' \in {0, 1}'' or ''\E v \in {0, 1} : x' = v'' are equivalent to ''x' = 0 \/ x' = 1''.
-  void bindValue(UnboundVariable var, Object value) {
+Add the following code to the ''IN'' case in ''visitBinaryExpr()'':
-    (var.primed() ? next : current).put(var.name().lexeme, value);
+<code java [highlight_lines_extra="3,4,5,6,7,8,9,10,11,12"]>
-  }
+      case IN:
+        checkSetOperand(expr.operator, right);
+        if (left instanceof UnboundVariable var) {
+          Map<String, Object> trunk = next;
+          for (Object element : (Set<?>)right) {
+            next = new HashMap<>(trunk);
+            next.put(var.name().lexeme, element);
+            left = element;
+            possibleNext.add(new HashMap<>(next));
+          }
+          return true;
+        }
+        return ((Set<?>)right).contains(left);
 </code>
-===== The Prime Operator =====
+Then update the ''EXISTS'' case of ''visitQuantFnExpr()'' as highlighted:
+<code java [highlight_lines_extra="3,5,8"]>
-We now have everything necessary to define the prime operator.
+      } case EXISTS: {
-Here's how it should work: in ''visitUnaryExpr()'' in the ''Interpreter'' class, detect that we are evaluating the prime operator; if so, prime the current state, evaluate the operand as a primed expression, then unprime the state and return the value of the operand.
+        boolean result = false;
-<code java>
+        State current = state;
-  public Object visitUnaryExpr(Expr.Unary expr) {
+        Map<String, Object> trunk = next;
-    if (TokenType.PRIME == expr.operator.type) {
+        for (Environment binding : bindings) {
-      state.prime(expr.operator);
+          next = new HashMap<>(trunk);
-      try {
+          Object junctResult = executeBlock(expr.body, binding);
-        return evaluate(expr.expr);
+          checkBooleanOperand(expr.op, junctResult);
-      } finally {
+          possibleNext.add(new HashMap<>(next));
-        state.unprime();
+          result |= (boolean)junctResult;
-      }
+        }
-    }
+        return result;
 </code>
-Note that we wrap the evaluation in a ''try''/''finally'' similar to in ''executeBlock()'', to restore the interpreter to an ordinary state if the evaluation results in an exception.
-We need to put the code at the top of ''visitUnaryExpr()'' because the other unary operators evaluate the operand first, but the prime operator changes how the operand is evaluated - it calls ''state.prime()'' beforehand!
+We can now generate all nondeterministic next states by calling ''getNextStates()'' with an appropriate action!
-Let's define the ''prime()'' and ''unprime()'' methods in the ''State'' class:
-<code java>
-  void prime(Token op) {
-    if (primed) {
-      throw new RuntimeError(op, "Cannot double-prime expression.");
-    }
-    primed = true;
+===== The ENABLED Operator =====
-  }
-  void unprime() {
+Now that we've written ''getNextStates()'', we can fully define the ''ENABLED'' prefix operator!
-    primed = false;
+An expression ''ENABLED Action'' evaluates to ''true'' if ''Action'' produces at least one possible next state.
-  }
+So, as simple as a quick call to ''getNextStates()'' to see whether it returns an empty list or not!
+Well, not quite - the ''ENABLED'' operator can possibly be evaluated //inside// an action, so inside a call to ''getNextStates()''!
+This means we need some extra ceremony to stash the current values of ''next'' and ''possibleNext'', then restore them using the standard ''try''/''finally'' block method.
+Add the highlighted code to the ''ENABLED'' case in ''visitUnaryExpr()'':
+<code java [highlight_lines_extra="2,3,4,5,6,7,8,9,10"]>
+      } case ENABLED: {
+        Map<String, Object> oldNext = next;
+        Set<Map<String,Object>> oldPossibleNext = possibleNext;
+        try {
+          clearNext();
+          return !getNextStates(expr.operator, expr.expr).isEmpty();
+        } finally {
+          next = oldNext;
+          possibleNext = oldPossibleNext;
+        }
+      } case NOT: {
 </code>
-Double-priming an expression is illegal in TLA⁺, so results in a runtime error.
+This is a big milestone: we now have fully defined //everything// in our minimal TLA⁺ language subset!
+We aren't at the end yet, but it's well within sight.
 ===== Error Checking =====
 Our code is nice & simple, but unfortunately it has more holes than Swiss cheese.
-Let's muddy it up with a bunch of error checks.
+Let's add some error checks!
 Null value types like ''UnboundVariable'' produce a major annoyance: we now need to sprinkle null checks throughout our evaluation code!
-Thankfully many null checks are already handled by our existing stable of ''check-Operand()'' helpers, but some cases still remain
+Thankfully many null checks are already handled by our existing stable of ''check-Operand()'' helpers, but some cases still remain.
-Near the bottom of the ''Interpreter'' class, create a new helper method ''checkIsDefined()'':
+Near the bottom of the ''Interpreter'' class, create a new helper method ''checkIsValue()'':
 <code java>
-  private void checkIsDefined(Object... operands) {
+  private void checkIsValue(Object... operands) {
     for (Object operand : operands) {
-      if (operand instanceof UnboundVariable) {
+      if (operand instanceof UnboundVariable var) {
-        UnboundVariable var = (UnboundVariable)operand;
         throw new RuntimeError(var.name(), "Use of unbound variable.");
       }
@@ Line 294: / Line 417: @@
 In our ''EQUALS'' handling logic, we can only bind the value of ''right'' to a variable if ''right'' has a defined concrete value.
 Also, two values can only be compared for equality if they are both defined:
-<code java [highlight_lines_extra="4,8"]>
+<code java [highlight_lines_extra="3,7"]>
       case EQUAL:
-        if (left instanceof UnboundVariable) {
+        if (left instanceof UnboundVariable var) {
-          UnboundVariable var = (UnboundVariable)left;
+          checkIsValue(right);
-          checkIsDefined(right);
+          next.put(var.name().lexeme, right);
-          state.bindValue(var, right);
           return true;
         }
-        checkIsDefined(left, right);
+        checkIsValue(left, right);
         return left.equals(right);
 </code>
-A null check also must be added to the ''LEFT_BRACE'' case of ''visitVariadicExpr()''; we can't let the user construct sets full of undefined values!
+A null check must also must be added to the ''LEFT_BRACE'' case in ''visitVariadicExpr()'':
 <code java [highlight_lines_extra="5"]>
       case LEFT_BRACE:
@@ Line 312: / Line 434: @@
         for (Expr parameter : expr.parameters) {
           Object value = evaluate(parameter);
-          checkIsDefined(value);
+          checkIsValue(value);
           set.add(value);
         }
 </code>
-First, we have to think about initial states.
+The ''ALL_MAP_TO'' case in ''visitQuantFnExpr()'':
-Not all components of a TLA⁺ spec are actions; the initial state is a predicate only on unprimed variables.
+<code java [highlight_lines_extra="6"]>
-What if we are in the initial state and process an expression containing a primed variable?
+      case ALL_MAP_TO: {
-It should result in an error.
+        Token param = expr.params.get(0);
-Add another field to ''State'' indicating whether the interpreter is in the initial state; as you might expect, this is initially true:
+        Map<Object, Object> function = new HashMap<>();
+        for (Environment binding : bindings) {
+          Object value = executeBlock(expr.body, binding);
+          checkIsValue(value);
+          function.put(binding.get(param), value);
+        }
+        return function;
+</code>
+And also the ''visitFnApplyExpr()'' method:
+<code java [highlight_lines_extra="5"]>
+  public Object visitFnApplyExpr(Expr.FnApply expr) {
+    Object callee = evaluate(expr.fn);
+    checkFunctionOperand(expr.bracket, callee);
+    Object argument = evaluate(expr.argument);
+    checkIsValue(argument);
+    Map<?, ?> function = (Map<?, ?>)callee;
+</code>
+===== Hooking Up the Interpreter =====
+It takes a bit of thought to consider how we should expose our new state-stepping capabilities through the REPL.
+One decent approach is to hijack ''Stmt.Print'' statements to trigger steps if they happen to define possible next states.
+For this, add the following code to the bottom of the ''run()'' method in the ''TlaPlus'' class:
+<code java [highlight_lines_extra="4,5,6,7,8,9"]>
+    // Stop if there was a syntax error.
+    if (hadError) return;
+    if (replMode && statements.size() == 1
+        && statements.get(0) instanceof Stmt.Print action) {
+      tryStep(action);
+    } else {
+      interpreter.interpret(statements);
+    }
+  }
+</code>
+This calls a method we'll define in ''TlaPlus'' called ''tryStep()''.
+The ''tryStep()'' method should first speculatively execute ''action'' to see what sort of value it returns; if it doesn't return a ''Boolean'', treat it as an ordinary ''Stmt.Print'' statement.
+However, if ''action'' //does// return a ''Boolean'', it might be a valid action leading to new states, so call ''getNextStates()''.
+If this generates no new states, again treat ''action'' as an ordinary ''Stmt.Print'' statement:
+<code java>
+  private static void tryStep(Stmt.Print action) {
+    Object result = interpreter.executeBlock(action.expression, interpreter.globals);
+    if (!(result instanceof Boolean)) {
+      action.accept(interpreter);
+      return;
+    }
+    List<Map<String, Object>> nextStates =
+      interpreter.getNextStates(action.location, action.expression);
+    if (nextStates.isEmpty()) {
+      action.accept(interpreter);
+      return;
+    }
+  }
+</code>
+The ''java.util.Map'' class must be imported at the top of the file:
 <code java [highlight_lines_extra="2"]>
-class State {
+import java.util.List;
-  private boolean initialState = true;
+import java.util.Map;
-  private boolean primed = false;
+public class TlaPlus {
 </code>
-In ''bindValue()'', raise an error if the user attempts to bind the value of a primed variable in the initial state:
+At this point all that remains is to handle the case of what happens when the ''Stmt.Print'' statement //does// generate possible next states.
-<code java [highlight_lines_extra="2,3,4,5"]>
+The REPL should choose one next state and make ''interpreter'' step to it; add this to the bottom of ''tryStep()'':
- void bindValue(UnboundVariable var, Object value) {
+<code java [highlight_lines_extra="8,9,10,11,12"]>
-    if (var.primed() && initialState) {
+    List<Map<String, Object>> nextStates =
-      throw new RuntimeError(var.name(),
+      interpreter.getNextStates(action.location, action.expression);
-          "Cannot prime variable in initial state.");
+    if (nextStates.isEmpty()) {
+      System.out.println(false);
+      return;
     }
+    Map<String, Object> nextState = pickNext(nextStates);
+    interpreter.goToState(nextState);
+    System.out.println(true);
+    System.out.println(nextState);
+  }
 </code>
-Later we'll look at how to transition beyond the initial state.
+We also print out ''true'' - the value ''Stmt.Print'' would have printed - and display the value of the next state for the user.
+This called two methods; one, ''goToState()'' in ''Interpreter'', sets the ''current'' state to the one given:
+<code java>
+  void goToState(Map<String, Object> state) {
+    current = state;
+    primed = state == null;
+    clearNext();
+  }
+</code>
+The other, in ''TlaPlus'', picks the next state to step to.
+If there are multiple possible next states, the user is prompted to choose one:
+<code java>
+  private static Map<String, Object> pickNext(List<Map<String, Object>> nextStates) {
+    if (nextStates.size() == 1) {
+      return nextStates.get(0);
+    } else {
+      System.out.println("Select next state (enter number): ");
+      for (int i = 0; i < nextStates.size(); i++) {
+        System.out.println(i + ": " + nextStates.get(i));
+      }
+      System.out.print("> ");
+      try (java.util.Scanner in = new java.util.Scanner(System.in)) {
+        return nextStates.get(in.nextInt());
+      }
+    }
+  }
+</code>
+And that's it!
+You can now run the REPL and step through the state space!
+Try entering expressions like the following:
+  - ''VARIABLE x''
+  - ''x = 0''
+  - ''x' \in 0 .. 5''
+This was a pivotal chapter; excellent work making it to the end.
+You can find the expected state of the codebase in [[https://github.com/tlaplus/devkit/tree/main/8-actions|this repository]].
+Now we can put it all together and build a real model checker in [[creating:safety|the next chapter]]!
+[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:safety|Next Page >]]