Differences

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

--- creating:actions [2025/06/19 20:44] – Rewrite Interpreter code to use simplified action method ahelwer
+++ creating:actions [2025/06/19 21:36] (current) – Finished probable final draft of actions tutorial ahelwer
@@ Line 395: / Line 395: @@
 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 =====
@@ Line 462: / Line 487: @@
     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!]]
+[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:closures|Next Page >]]