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:40] – Use goToState() instead of setNextState() and step() ahelwercreating:actions [2025/11/03 23:08] (current) – One more instanceof-cast ahelwer
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 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 339: 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 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 410: 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 420: 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 476: 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 571: 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.1756248051.txt.gz
  • Last modified: 2025/08/26 22:40
  • by ahelwer