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/08/26 22:13] – Improve double-priming error message, remove ambiguous usage of "current" 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 193: 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 200: 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 210: 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 233:
  
   public Interpreter(boolean replMode) {   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> </code>
  
Line 316: 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 329: 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 363: 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 434: 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 444: 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 500: Line 472:
  
     if (replMode && statements.size() == 1     if (replMode && statements.size() == 1
-        && statements.get(0) instanceof Stmt.Print) { +        && statements.get(0) instanceof Stmt.Print action) { 
-      tryStep((Stmt.Print)statements.get(0));+      tryStep(action);
     } else {     } else {
       interpreter.interpret(statements);       interpreter.interpret(statements);
Line 548: Line 520:
  
     Map<String, Object> nextState = pickNext(nextStates);     Map<String, Object> nextState = pickNext(nextStates);
-    interpreter.setNextState(nextState); +    interpreter.goToState(nextState);
-    interpreter.step(action.location);+
     System.out.println(true);     System.out.println(true);
     System.out.println(nextState);     System.out.println(nextState);
Line 556: Line 527:
  
 We also print out ''true'' - the value ''Stmt.Print'' would have printed - and display the value of the next state for the user. 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'':+This called two methods; one, ''goToState()'' in ''Interpreter'', sets the ''current'' state to the one given:
 <code java> <code java>
-  void setNextState(Map<String, Object> next) { +  void goToState(Map<String, Object> state) { 
-    this.next = next;+    current = state; 
 +    primed = state == null; 
 +    clearNext();
   }   }
 </code> </code>
Line 594: Line 567:
 Now we can put it all together and build a real model checker in [[creating:safety|the next chapter]]! 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:closures|Next Page >]]+[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:safety|Next Page >]]
  
  • creating/actions.1756246387.txt.gz
  • Last modified: 2025/08/26 22:13
  • by ahelwer