creating:actions

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
creating:actions [2025/06/06 22:01] – Handle basic x' = expr case ahelwercreating:actions [2025/06/19 21:36] (current) – Finished probable final draft of actions tutorial ahelwer
Line 45: Line 45:
     ));     ));
 </code> </code>
 +
 Then use the old ''do''/''while'' trick to parse comma-separated variable names in the ''declaration()'' method of the ''Parser'' class: 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"]> <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. 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>, class Interpreter implements Expr.Visitor<Object>,
                              Stmt.Visitor<Void> {                              Stmt.Visitor<Void> {
   final Environment globals;   final Environment globals;
   private Environment environment;   private Environment environment;
-  private final PrintStream out; 
-  private State state = new State(); 
-</code> 
  
-This requires a new class! +  private final Map<String, Token> variables = new HashMap<>(); 
-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: +  private Map<String, Object> current = null; 
-<code java> +  private Map<String, Object> next = new HashMap<>(); 
-package tla;+</code>
  
-import java.util.HashMap; +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. 
-import java.util.Map; +The system's initial state will be built in ''next'', which then eventually becomes ''current''.
- +
-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> <code java>
   @Override   @Override
Line 103: Line 87:
     checkNotDefined(stmt.names);     checkNotDefined(stmt.names);
     for (Token name : 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> </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) {   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.");       throw new RuntimeError(stmt.name, "State variable redeclared as operator.");
     }     }
  
     TlaOperator op = new TlaOperator(stmt);     TlaOperator op = new TlaOperator(stmt);
-    environment.define(stmt.name, op); 
 </code> </code>
  
Line 130: Line 140:
       }       }
  
-      if (state.isDeclared(name)) {+      if (variables.containsKey(name.lexeme)) {
         throw new RuntimeError(name, "Name conflicts with state variable.");         throw new RuntimeError(name, "Name conflicts with state variable.");
       }       }
Line 136: Line 146:
 </code> </code>
  
-===== Initializing State Variables =====+===== Reading & Priming 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. +
-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! +
-Alas we now depart this wonderful land. +
-Create a new class, ''UnboundVariable.java'': +
-<code java> +
-package tla; +
- +
-record UnboundVariable(Token name, boolean primed) { +
-  @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: +
-<code java [highlight_lines_extra="3,4"]> +
-class State { +
-  private Map<String, Token> variables = new HashMap<>(); +
-  private Map<String, Object> current = new HashMap<>(); +
-  private Map<String, Object> next = new HashMap<>(); +
-</code> +
- +
-Then, in ''declareVariable()'', initialize the variables to instances of ''UnboundVariable'': +
-<code java [highlight_lines_extra="2,3,4"]> +
-    variables.put(name.lexeme, name); +
-    current.put(name.lexeme, new UnboundVariable(name, false)); +
-    next.put(name.lexeme, new UnboundVariable(name, true)); +
-  } +
-</code> +
- +
-===== Getting State Variables ===== +
- +
-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: +
-<code java [highlight_lines_extra="2,4,5,6"]>+
   public Object visitVariableExpr(Expr.Variable expr) {   public Object visitVariableExpr(Expr.Variable expr) {
-    Object referent = getValue(expr.name); +    Object referent = 
- +      variables.containsKey(expr.name.lexeme) 
-    if (referent instanceof UnboundVariable) { +      ? (primed ? next : current).get(expr.name.lexeme) 
-      return referent; +      : environment.get(expr.name);
-    }+
  
     if (!(referent instanceof TlaCallable)) {     if (!(referent instanceof TlaCallable)) {
 </code> </code>
  
-The new ''getValue()'' helper merges lookup logic for state variables & operators; these should be disjoint, although state variable values are checked first: +This makes use of yet another field we must add to the ''Interpreter'' class, ''primed'': 
-<code java> +<code java [highlight_lines_extra="2"]> 
-  private Object getValue(Token name) { +  private Map<String, Object> next = new HashMap<>(); 
-    if (state.isDeclared(name)) { +  private boolean primed = true;
-      return state.getValue(name); +
-    }+
  
-    return environment.get(name); +  public Interpreter(boolean replMode) {
-  }+
 </code> </code>
  
-To define ''getValue()'' in the ''State'' class we need to determine whether to pull state variable values from ''current'' or ''next''. +The ''primed'' field controls whether variable values are pulled from the ''current'' or ''next'' states. 
-For this there must be some way of tracking whether we are currently inside a primed expression. +When inside a primed expression, variables are pulled from ''next''; when outside of primed expressions, variables are pulled from ''current''. 
-Not just variables can be primed in TLA⁺, entire expressions can be! +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. 
-The meaning of a primed expression is that every state variable within that expression is primed. +We can now finally define the prime operator for real, in ''visitUnaryExpr()'' in the ''Interpreter'' class: 
-This is tracked with a boolean class variable in ''State'', which is initialized to false: +<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12"]> 
-<code java [highlight_lines_extra="2"]> +  public Object visitUnaryExpr(Expr.Unary expr) { 
-class State { +    switch (expr.operator.type) { 
-  private boolean primed = false; +      case PRIME: { 
-  private Map<String, Token> variables = new HashMap<>();+        if (primed) { 
 +          throw new RuntimeError(expr.operator, 
 +              "Cannot double-prime expression nor prime initial state."); 
 +        } try { 
 +          primed = true; 
 +          return evaluate(expr.expr); 
 +        } finally { 
 +          primed = false; 
 +        } 
 +      } case ENABLED: {
 </code> </code>
  
-Now define ''getValue()'' in the ''State'' class. +Double-priming an expression or priming an expression in the initial state are both fatal errors in TLA⁺. 
-If ''primed'' is true, we retrieve the state variable value from ''next''; if false, we retrieve it from ''current'': +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. 
-<code java> +This is why the prime operator somewhat uniquely modifies the state of the ''Interpreter'' instance itself. 
-  Object getValue(Token name) { +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.
-    return (primed ? next : current).get(name.lexeme); +
-  } +
-</code>+
  
 ===== Setting State Variables ===== ===== Setting State Variables =====
  
 We can retrieve state variable values, but what about assigning them? 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'' or ''x' = expr''.+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. 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'': 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,6"]> <code java [highlight_lines_extra="2,3,4,5,6"]>
       case EQUAL:       case EQUAL:
-        if (left instanceof UnboundVariable) {+        if (left instanceof State.UnboundVariable) {
           UnboundVariable var = (UnboundVariable)left;           UnboundVariable var = (UnboundVariable)left;
-          state.bindValue(var, right);+          next.put(var.name().lexeme, right);
           return true;           return true;
         }         }
Line 231: Line 208:
 </code> </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:+We only modify variable values in ''next'', not ''current''; variable values in ''current'' should be considered immutable. 
 + 
 +Although we won't yet use it, now is also a good time to define our ''step()'' method, which transitions the ''Interpreter'' instance to the next state; it has two associated helper methods, ''isComplete()'' and ''clearNext()'':
 <code java> <code java>
-  void bindValue(UnboundVariable var, Object value) { +  void step(Token location) { 
-    (var.primed() ? next : current).put(var.name().lexeme, value);+    if (!isComplete()) { 
 +      throw new RuntimeError(location, 
 +          "Cannot step to incomplete next state."); 
 +    } 
 + 
 +    primed = false; 
 +    current = next; 
 +    clearNext();
   }   }
-</code> 
  
-===== The Prime Operator =====+  private void isComplete() { 
 +    return !variables.isEmpty() && next.values().stream() 
 +        .noneMatch(v -> v instanceof UnboundVariable); 
 +  }
  
-We now have everything necessary to define the prime operator. +  private void clearNext() { 
-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. +    next = new HashMap<>(); 
-<code java> +    for (Token variable : variables.values()) { 
-  public Object visitUnaryExpr(Expr.Unary expr) { +      next.put(variable.lexeme, new UnboundVariable(variable));
-    if (TokenType.PRIME == expr.operator.type) { +
-      state.prime(expr.operator); +
-      try { +
-        return evaluate(expr.expr); +
-      } finally { +
-        state.unprime(); +
-      }+
     }     }
 +  }
 </code> </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! +''isComplete()'' checks to ensure the next state is completely defined, and ''clearNext()'' resets the value of ''next''. 
-Let's define the ''prime()'' and ''unprime()'' methods in the ''State'' class:+ 
 +Now we see things taking shape: ''Interpreter'' is initialized with ''current'' set to ''null'' and ''primed'' set to ''true'', ready to define the system's initial state. 
 +The system's initial state is defined by setting the values of all declared variables in ''next'', using expressions like ''x = 0''. 
 +Then, ''step()'' is called, which sets ''current'' to ''next'' and ''primed'' to ''false''; the system is now in its initial state, ready to take steps to next states. 
 +The values of variables in ''next'' are subsequently set using expressions like ''x' = 1 - x'', then ''step()'' is called again, and so on. 
 + 
 +===== 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> 
 + 
 +We also update ''clearNext()'' to wipe the new ''possibleNext'' field: 
 +<code java [highlight_lines_extra="2"]> 
 +  private void clearNext() { 
 +    possibleNext = new HashSet<>(); 
 +    next = new HashMap<>(); 
 +</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 current state. 
 +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> <code java>
-  void prime(Token op) { +  List<Map<String, Object>> getNextStates(Token location, Expr action) {
-    if (primed) { +
-      throw new RuntimeError(op, "Cannot double-prime expression."); +
-    }+
  
-    primed = true; 
   }   }
 +</code>
  
-  void unprime() { +''getNextStates()'' will use the following algorithm: 
-    primed = false;+  - 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 
 + 
 +Here's how we set up everything outside of the central loop: 
 +<code java [highlight_lines_extra="2,3,4,5,6,8,9,10,11,13"]> 
 +  List<Map<String, Object>> getNextStates(Token location, Expr action) { 
 +    Set<Map<String, Object>> confirmedNext = new HashSet<>(); 
 +    clearNext(); 
 +    possibleNext.add(new HashMap<>(next)); 
 +    try { 
 +      while (!possibleNext.isEmpty()) { 
 + 
 +      } 
 +    } finally { 
 +      clearNext(); 
 +    } 
 + 
 +    return new ArrayList<>(confirmedNext);
   }   }
 </code> </code>
  
-Double-priming an expression is illegal in TLA⁺, so results in a runtime error.+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. 
 + 
 +Now we can write the central loop: 
 +<code java [highlight_lines_extra="2,3,4,5,6,7"]> 
 +      while (!possibleNext.isEmpty()) { 
 +        Map<String, Object> trunk = possibleNext.iterator().next(); 
 +        next = new HashMap<>(trunk); 
 +        Object satisfied = evaluate(action); 
 +        checkBooleanOperand(location, satisfied); 
 +        if ((boolean)satisfied && isComplete()) confirmedNext.add(next); 
 +        possibleNext.remove(trunk); 
 +      } 
 +</code> 
 + 
 +Note again the judicious use of ''HashMap<>'' copy constructors to avoid the mutable ''HashMap<>'' key bug. 
 + 
 +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. 
 + 
 +There is also the question of termination. 
 +What is preventing ''getNextStates()'' from entering an infinite loop? 
 +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. 
 +Thus the number of variables bound to concrete values in ''possibleNext'' increases monotonically, eventually encompassing all declared variables and terminating the loop. 
 + 
 +Let's get concrete. 
 +How do we add states to ''possibleNext'' while evaluating disjunction? 
 +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''. 
 +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. 
 +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 result; 
 +      default: 
 +</code> 
 + 
 +There are two other operators to support for binding state variables: the set membership ''\in'' operator, and the ''\E'' existential quantification operator. 
 +Actions like ''x' \in {0, 1}'' or ''\E v \in {0, 1} : x' = v'' are equivalent to ''x' = 0 \/ x' = 1''. 
 +Add the following code to the ''IN'' case in ''visitBinaryExpr()'': 
 +<code java [highlight_lines_extra="3,4,5,6,7,8,9,10,11,12,13"]> 
 +      case IN: 
 +        checkSetOperand(expr.operator, right); 
 +        if (left instanceof State.UnboundVariable) { 
 +          UnboundVariable var = (UnboundVariable)left; 
 +          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> 
 + 
 +Then update the ''EXISTS'' case of ''visitQuantFnExpr()'' as highlighted: 
 +<code java [highlight_lines_extra="3,5,8"]> 
 +      } case EXISTS: { 
 +        boolean result = false; 
 +        State current = state; 
 +        Map<String, Object> trunk = next; 
 +        for (Environment binding : bindings) { 
 +          next = new HashMap<>(trunk); 
 +          Object junctResult = executeBlock(expr.body, binding); 
 +          checkBooleanOperand(expr.op, junctResult); 
 +          possibleNext.add(new HashMap<>(next)); 
 +          result |= (boolean)junctResult; 
 +        } 
 +        return result; 
 +</code> 
 + 
 +We can now generate all nondeterministic next states by calling ''getNextStates()'' with an appropriate action! 
 + 
 +===== The ENABLED Operator ===== 
 + 
 +Now that we've written ''getNextStates()'', we can fully define the ''ENABLED'' prefix operator! 
 +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> 
 + 
 +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 ===== ===== Error Checking =====
  
 Our code is nice & simple, but unfortunately it has more holes than Swiss cheese. 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! 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> <code java>
-  private void checkIsDefined(Object... operands) {+  private void checkIsValue(Object... operands) {
     for (Object operand : operands) {     for (Object operand : operands) {
       if (operand instanceof UnboundVariable) {       if (operand instanceof UnboundVariable) {
Line 298: Line 446:
         if (left instanceof UnboundVariable) {         if (left instanceof UnboundVariable) {
           UnboundVariable var = (UnboundVariable)left;           UnboundVariable var = (UnboundVariable)left;
-          checkIsDefined(right); +          checkIsValue(right); 
-          state.bindValue(var, right);+          next.put(var.name().lexeme, right);
           return true;           return true;
         }         }
-        checkIsDefined(left, right);+        checkIsValue(left, right);
         return left.equals(right);         return left.equals(right);
 </code> </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"]> <code java [highlight_lines_extra="5"]>
       case LEFT_BRACE:       case LEFT_BRACE:
Line 312: Line 460:
         for (Expr parameter : expr.parameters) {         for (Expr parameter : expr.parameters) {
           Object value = evaluate(parameter);           Object value = evaluate(parameter);
-          checkIsDefined(value);+          checkIsValue(value);
           set.add(value);           set.add(value);
         }         }
 </code> </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) { 
 +      tryStep((Stmt.Print)statements.get(0)); 
 +    } 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"]> <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> </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.setNextState(nextState);
 +    interpreter.step(action.location);
 +    System.out.println(true);
 +    System.out.println(nextState);
 +  }
 </code> </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, in ''Interpreter'', sets the value of ''next'': 
 +<code java> 
 +  void setNextState(Map<String, Object> next) { 
 +    this.next = next; 
 +  } 
 +</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]]. 
 +See you in the [[creating:closures|next chapter on closures!]] 
 + 
 +[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:closures|Next Page >]]
  
  • creating/actions.1749247307.txt.gz
  • Last modified: 2025/06/06 22:01
  • by ahelwer