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 18:37] – Change next chapter to model checker 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 432: 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 442: 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 498: 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 546: 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 554: 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 592: 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.1756233436.txt.gz
  • Last modified: 2025/08/26 18:37
  • by ahelwer