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/19 20:44] – Rewrite Interpreter code to use simplified action method ahelwercreating:actions [2025/11/03 23:08] (current) – One more instanceof-cast ahelwer
Line 146: Line 146:
 </code> </code>
  
-===== Reading & Priming State Variables =====+===== Reading, Priming, & Setting 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: 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:
Line 171: Line 171:
 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 ''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: 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"]>+<code java [highlight_lines_extra="4,5,6,7,8,9,10,11,12,13,14"]>
   public Object visitUnaryExpr(Expr.Unary expr) {   public Object visitUnaryExpr(Expr.Unary expr) {
     switch (expr.operator.type) {     switch (expr.operator.type) {
Line 177: Line 177:
         if (primed) {         if (primed) {
           throw new RuntimeError(expr.operator,           throw new RuntimeError(expr.operator,
-              "Cannot double-prime expression nor prime initial state.");+              current == null 
 +              ? "Cannot prime expression in initial state." 
 +              : "Cannot double-prime expression.");
         } try {         } try {
           primed = true;           primed = true;
Line 191: Line 193:
 This is why the prime operator somewhat uniquely modifies the state of the ''Interpreter'' instance itself. 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. 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? We can retrieve state variable values, but what about assigning them?
Line 198: Line 198:
 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"]>
       case EQUAL:       case EQUAL:
-        if (left instanceof State.UnboundVariable) { +        if (left instanceof UnboundVariable var) {
-          UnboundVariable var = (UnboundVariable)left;+
           next.put(var.name().lexeme, right);           next.put(var.name().lexeme, right);
           return true;           return true;
Line 208: Line 207:
 </code> </code>
  
-We only modify variable values in ''next'', not ''current''; variable values in ''current'' should be considered immutable. +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.
- +
-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 ===== ===== Nondeterminism =====
Line 269: Line 235:
 </code> </code>
  
-We also update ''clearNext()'' to wipe the new ''possibleNext'' field: +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.
-<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. 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: We will write this very critical top-level loop now; create a new method ''getNextStates()'' in the ''Interpreter'' class:
Line 314: Line 273:
 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. 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:+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 void clearNext() { 
 +    possibleNext = new HashSet<>(); 
 +    next = new HashMap<>(); 
 +    for (Token variable : variables.values()) { 
 +      next.put(variable.lexeme, new UnboundVariable(variable)); 
 +    } 
 +  } 
 +</code> 
 + 
 +Now we can write the central ''getNextStates()'' loop:
 <code java [highlight_lines_extra="2,3,4,5,6,7"]> <code java [highlight_lines_extra="2,3,4,5,6,7"]>
       while (!possibleNext.isEmpty()) {       while (!possibleNext.isEmpty()) {
Line 327: Line 297:
  
 Note again the judicious use of ''HashMap<>'' copy constructors to avoid the mutable ''HashMap<>'' key bug. Note again the judicious use of ''HashMap<>'' copy constructors to avoid the mutable ''HashMap<>'' key bug.
 +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>
 +  private boolean isComplete() {
 +    return !variables.isEmpty() && next.values().stream()
 +        .noneMatch(v -> v instanceof UnboundVariable);
 +  }
 +</code>
  
 It's worth spending some time considering the ''getNextStates()'' method. It's worth spending some time considering the ''getNextStates()'' method.
Line 361: Line 338:
 Actions like ''x' \in {0, 1}'' or ''\E v \in {0, 1} : x' = v'' are equivalent to ''x' = 0 \/ x' = 1''. 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()'': 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"]>+<code java [highlight_lines_extra="3,4,5,6,7,8,9,10,11,12"]>
       case IN:       case IN:
         checkSetOperand(expr.operator, right);         checkSetOperand(expr.operator, right);
-        if (left instanceof State.UnboundVariable) { +        if (left instanceof UnboundVariable var) {
-          UnboundVariable var = (UnboundVariable)left;+
           Map<String, Object> trunk = next;           Map<String, Object> trunk = next;
           for (Object element : (Set<?>)right) {           for (Object element : (Set<?>)right) {
Line 395: Line 371:
  
 We can now generate all nondeterministic next states by calling ''getNextStates()'' with an appropriate action! 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 =====
Line 407: Line 408:
   private void checkIsValue(Object... operands) {   private void checkIsValue(Object... operands) {
     for (Object operand : 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.");         throw new RuntimeError(var.name(), "Use of unbound variable.");
       }       }
Line 417: 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. 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: 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:       case EQUAL:
-        if (left instanceof UnboundVariable) { +        if (left instanceof UnboundVariable var) {
-          UnboundVariable var = (UnboundVariable)left;+
           checkIsValue(right);           checkIsValue(right);
           next.put(var.name().lexeme, right);           next.put(var.name().lexeme, right);
Line 462: Line 461:
     Map<?, ?> function = (Map<?, ?>)callee;     Map<?, ?> function = (Map<?, ?>)callee;
 </code> </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"]>
 +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.goToState(nextState);
 +    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, ''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 >]]
  
  • creating/actions.1750365867.txt.gz
  • Last modified: 2025/06/19 20:44
  • by ahelwer