creating:actions

Differences

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

Link to this comparison view

Next revision		 Previous revision
creating:actions [2025/06/06 18:54] – Parsing & interpreting variable declarations ahelwercreating:actions [2025/06/19 21:36] (current) – Finished probable final draft of actions tutorial ahelwer
Line 31: Line 31:
 What this means is that we only support certain types of expressions incorporating primed variables, so we restrict ourselves to only model-checking TLA⁺ specs written in a particular idiom. What this means is that we only support certain types of expressions incorporating primed variables, so we restrict ourselves to only model-checking TLA⁺ specs written in a particular idiom.
  
-====== Variables and Priming ====== 
 Let's start by supporting a simple operation on primed variables, expressions of the form ''x' = expr''. Let's start by supporting a simple operation on primed variables, expressions of the form ''x' = expr''.
 There is a fair bit of groundwork necessary to reach that point. There is a fair bit of groundwork necessary to reach that point.
  
-===== Variable Declarations =====+===== Declaring State Variables ===== 
 First off we have to add support for variable declarations; these are top-level syntactic constructs that look like ''VARIABLES x, y, z''. First off we have to add support for variable declarations; these are top-level syntactic constructs that look like ''VARIABLES x, y, z''.
 Create a new statement type for them in the ''GenerateAst'' class: Create a new statement type for them in the ''GenerateAst'' class:
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! 
-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: 
-<code java> 
-package tla; 
- 
-import java.util.HashMap; 
-import java.util.Map; 
  
-class State { +  private final Map<String, Token> variables = new HashMap<>(); 
-  private Map<String, Token> variables = new HashMap<>();+  private Map<String, Object> current = null; 
 +  private Map<String, Object> next = new HashMap<>(); 
 +</code>
  
-  boolean isDeclared(Token name) { +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. 
-    return variables.containsKey(name.lexeme); +The system's initial state will be built in ''next'', which then eventually becomes ''current''.
-  } +
- +
-  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>
 +
 Also augment the ''checkNotDefined()'' helper method, so state variables cannot be shadowed by operator parameters: Also augment the ''checkNotDefined()'' helper method, so state variables cannot be shadowed by operator parameters:
 <code java [highlight_lines_extra="7,8,9"]> <code java [highlight_lines_extra="7,8,9"]>
Line 129: 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 135: Line 146:
 </code> </code>
  
-===== Variable Values =====+===== Reading & Priming State Variables ===== 
 + 
 +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: 
 +<code java [highlight_lines_extra="2,3,4,5"]> 
 +  public Object visitVariableExpr(Expr.Variable expr) { 
 +    Object referent = 
 +      variables.containsKey(expr.name.lexeme) 
 +      ? (primed ? next : current).get(expr.name.lexeme) 
 +      : environment.get(expr.name); 
 + 
 +    if (!(referent instanceof TlaCallable)) { 
 +</code> 
 + 
 +This makes use of yet another field we must add to the ''Interpreter'' class, ''primed'': 
 +<code java [highlight_lines_extra="2"]> 
 +  private Map<String, Object> next = new HashMap<>(); 
 +  private boolean primed = true; 
 + 
 +  public Interpreter(boolean replMode) { 
 +</code> 
 + 
 +The ''primed'' field controls whether variable values are pulled from the ''current'' or ''next'' states. 
 +When inside a primed expression, variables are pulled from ''next''; when outside of primed expressions, variables are pulled from ''current''. 
 +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. 
 +We can now finally define the prime operator for real, in ''visitUnaryExpr()'' in the ''Interpreter'' class: 
 +<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12"]> 
 +  public Object visitUnaryExpr(Expr.Unary expr) { 
 +    switch (expr.operator.type) { 
 +      case PRIME: { 
 +        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> 
 + 
 +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. 
 + 
 +===== Setting State Variables ===== 
 + 
 +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,6"]> 
 +      case EQUAL: 
 +        if (left instanceof State.UnboundVariable) { 
 +          UnboundVariable var = (UnboundVariable)left; 
 +          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. 
 + 
 +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> 
 +  void step(Token location) { 
 +    if (!isComplete()) { 
 +      throw new RuntimeError(location, 
 +          "Cannot step to incomplete next state."); 
 +    } 
 + 
 +    primed = false; 
 +    current = next; 
 +    clearNext(); 
 +  } 
 + 
 +  private void isComplete() { 
 +    return !variables.isEmpty() && next.values().stream() 
 +        .noneMatch(v -> v instanceof UnboundVariable); 
 +  } 
 + 
 +  private void clearNext() { 
 +    next = new HashMap<>(); 
 +    for (Token variable : variables.values()) { 
 +      next.put(variable.lexeme, new UnboundVariable(variable)); 
 +    } 
 +  } 
 +</code> 
 + 
 +''isComplete()'' checks to ensure the next state is completely defined, and ''clearNext()'' resets the value of ''next''. 
 + 
 +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> 
 +  List<Map<String, Object>> getNextStates(Token location, Expr action) { 
 + 
 +  } 
 +</code> 
 + 
 +''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 
 + 
 +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> 
 + 
 +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 ===== 
 + 
 +Our code is nice & simple, but unfortunately it has more holes than Swiss cheese. 
 +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. 
 +Near the bottom of the ''Interpreter'' class, create a new helper method ''checkIsValue()'': 
 +<code java> 
 +  private void checkIsValue(Object... operands) { 
 +    for (Object operand : operands) { 
 +      if (operand instanceof UnboundVariable) { 
 +        UnboundVariable var = (UnboundVariable)operand; 
 +        throw new RuntimeError(var.name(), "Use of unbound variable."); 
 +      } 
 +    } 
 +  } 
 +</code> 
 + 
 +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"]> 
 +      case EQUAL: 
 +        if (left instanceof UnboundVariable) { 
 +          UnboundVariable var = (UnboundVariable)left; 
 +          checkIsValue(right); 
 +          next.put(var.name().lexeme, right); 
 +          return true; 
 +        } 
 +        checkIsValue(left, right); 
 +        return left.equals(right); 
 +</code> 
 + 
 +A null check must also must be added to the ''LEFT_BRACE'' case in ''visitVariadicExpr()'': 
 +<code java [highlight_lines_extra="5"]> 
 +      case LEFT_BRACE: 
 +        Set<Object> set = new HashSet<Object>(); 
 +        for (Expr parameter : expr.parameters) { 
 +          Object value = evaluate(parameter); 
 +          checkIsValue(value); 
 +          set.add(value); 
 +        } 
 +</code> 
 + 
 +The ''ALL_MAP_TO'' case in ''visitQuantFnExpr()'': 
 +<code java [highlight_lines_extra="6"]> 
 +      case ALL_MAP_TO: { 
 +        Token param = expr.params.get(0); 
 +        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"]> 
 +import java.util.List; 
 +import java.util.Map; 
 + 
 +public class TlaPlus { 
 +</code> 
 + 
 +At this point all that remains is to handle the case of what happens when the ''Stmt.Print'' statement //does// generate possible next states. 
 +The REPL should choose one next state and make ''interpreter'' step to it; add this to the bottom of ''tryStep()'': 
 +<code java [highlight_lines_extra="8,9,10,11,12"]> 
 +    List<Map<String, Object>> nextStates = 
 +      interpreter.getNextStates(action.location, action.expression); 
 +    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> 
 + 
 +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!]]
  
-Now that we can declare variables, what value are they initialized to? +[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:closures|Next Page >]]
-We've successfully dodged this issue for a very long time, but unfortunately the initial value of these variables is undefined. +
-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.+
  
  • creating/actions.1749236051.txt.gz
  • Last modified: 2025/06/06 18:54
  • by ahelwer