Variables, States, and Actions

Currently, our implementation is not significantly different from any other ordinary programming language. However, TLA⁺ is not an ordinary language - it isn't even a programming language! TLA⁺ specifications are not programs. Properly speaking, a TLA⁺ specification is a predicate over an infinite sequence of states, where states are an assignment of values to variables. TLA⁺ specs' closest analogue to program execution is enumerating the set of all unique reachable states, over which state traces occur. The focus of this chapter is thus to introduce states and how to transition between them using actions.

Every model-checkable TLA⁺ specification contains variables. These variables are different from the identifiers associated with operators in past chapters. The variables constitute a static set of identifiers associated with values in each system state. TLA⁺ also has actions, which are expressions containing the prime operator. The prime operator is used to specify the value of variables in the next state. For example:

VARIABLE x
Action ==
  /\ x = 0
  /\ x' = x + 1

This spec declares a single variable, x, and a single action. The action is only enabled for states where x has value 0, and generates a new state where x has value x + 1, or 1.

It's worth taking a moment here to think about what actions actually mean. Actions are predicates, meaning logical expressions evaluating to true or false. Strictly speaking actions don't "generate" new states, or "assign" values to variables; actions are true or false of a pair of states, called the current & next states. This is the actual semantic meaning of a TLA⁺ action: a predicate which is satisfied (or not) by a pair of arbitrary states pulled from the mathematical ether. However, here at the implementation level we don't have the luxury of being able to identify next states by checking an infinite number of arbitrary states pulled from the mathematical ether. We have to be smart, and pull clues about next state values directly from the action itself. What this means is that we only support certain types of expressions incorporating primed variables, so we restrict ourselves to only model-checking TLA⁺ specs written in a particular idiom.

Let's start by supporting a simple operation on primed variables, expressions of the form x' = expr. There is a fair bit of groundwork necessary to reach that point.

First off we have to add support for variable declarations; these are top-level syntactic constructs that look like VARIABLES x, y, z. Create a new statement type for them in the GenerateAst class:

    defineAst(outputDir, "Stmt", Arrays.asList(
      "VarDecl  : List<Token> names",
      "Print    : Token location, Expr expression",
      "OpDef    : Token name, List<Token> params, Expr body"
    ));

Then use the old do/while trick to parse comma-separated variable names in the declaration() method of the Parser class:

  private Stmt declaration() {
    try {
      if (lookahead().isAtOpDefStart()) return operatorDefinition();
      if (match(VARIABLES)) {
        List<Token> names = new ArrayList<>();
        do {
          names.add(consume(IDENTIFIER, "Require variable name."));
        } while (match(COMMA));
        return new Stmt.VarDecl(names);
      }
 
      return statement();

Before we can define a Stmt.VarDecl visitor, we need to come up with a way to manage variables & states. It's simplest to copy the Environment approach and record the current state as a field in the Interpreter class:

class Interpreter implements Expr.Visitor<Object>,
                             Stmt.Visitor<Void> {
  final Environment globals;
  private Environment environment;
  private final PrintStream out;
  private State state = new State();

This requires a new class! Create a file called State.java; for now, this just supports the ability to declare variables; it also produces an error if the user attempts to declare the same variable twice:

package tla;
 
import java.util.HashMap;
import java.util.Map;
 
class State {
  private Map<String, Token> variables = new HashMap<>();
 
  boolean isDeclared(Token name) {
    return variables.containsKey(name.lexeme);
  }
 
  void declareVariable(Token name) {
    if (isDeclared(name)) {
      throw new RuntimeError(name, "Redeclared state variable.");
    }
 
    variables.put(name.lexeme, name);
  }
}

That's enough to implement visitVarDeclStmt() in the Interpreter class:

  @Override
  public Void visitVarDeclStmt(Stmt.VarDecl stmt) {
    checkNotDefined(stmt.names);
    for (Token name : stmt.names) {
      state.declareVariable(name);
    }
 
    return null;
  }

In intepreter mode we continue to support redefining operators, but will produce an error if the user attempts to redefine an operator as a state variable or vice versa. Add this check to the visitOpDefStmt() method of the Interpreter class:

  public Void visitOpDefStmt(Stmt.OpDef stmt) {
    if (state.isDeclared(stmt.name)) {
      throw new RuntimeError(stmt.name, "State variable redeclared as operator.");
    }
 
    TlaOperator op = new TlaOperator(stmt);
    environment.define(stmt.name, op);

Also augment the checkNotDefined() helper method, so state variables cannot be shadowed by operator parameters:

  private void checkNotDefined(List<Token> names) {
    for (Token name : names) {
      if (environment.isDefined(name)) {
        throw new RuntimeError(name, "Identifier already in use.");
      }
 
      if (state.isDeclared(name)) {
        throw new RuntimeError(name, "Name conflicts with state variable.");
      }
    }

Now that we can declare variables, what value are they initialized to? We've successfully dodged this issue for a very long time in this tutorial series, but unfortunately the initial value of these variables is undefined. That means we will need a null value type. We've avoided null types thus far, which means we haven't had to do as many checks before using values in the interpreter - a real luxury! Alas we now depart this wonderful land. Create a new class, UnboundVariable.java:

package tla;
 
record UnboundVariable(Token name, boolean primed) {
  @Override
  public String toString() {
    return name.lexeme + (primed ? "'" : "");
  }
}

In the State class, we need to track variable values for the current & next states; add one Map<> instance for each:

class State {
  private Map<String, Token> variables = new HashMap<>();
  private Map<String, Object> current = new HashMap<>();
  private Map<String, Object> next = new HashMap<>();

Then, in declareVariable(), initialize the variables to instances of UnboundVariable:

    variables.put(name.lexeme, name);
    current.put(name.lexeme, new UnboundVariable(name, false));
    next.put(name.lexeme, new UnboundVariable(name, true));
  }

To retrieve variable values, modify the ever-more-complicated visitVariableExpr() method of the Interpreter class to call a new getValue() helper; if the value resolves to an UnboundVariable instance, return it immediately:

  public Object visitVariableExpr(Expr.Variable expr) {
    Object referent = getValue(expr.name);
 
    if (referent instanceof UnboundVariable) {
      return referent;
    }
 
    if (!(referent instanceof TlaCallable)) {

The new getValue() helper merges lookup logic for state variables & operators; these should be disjoint, although state variable values are checked first:

  private Object getValue(Token name) {
    if (state.isDeclared(name)) {
      return state.getValue(name);
    }
 
    return environment.get(name);
  }

To define getValue() in the State class we need to determine whether to pull state variable values from current or next. For this there must be some way of tracking whether we are currently inside a primed expression. Not just variables can be primed in TLA⁺, entire expressions can be! The meaning of a primed expression is that every state variable within that expression is primed. This is tracked with a boolean class variable in State, which is initialized to false:

class State {
  private boolean primed = false;
  private Map<String, Token> variables = new HashMap<>();

Now define getValue() in the State class. If primed is true, we retrieve the state variable value from next; if false, we retrieve it from current:

  Object getValue(Token name) {
    return (primed ? next : current).get(name.lexeme);
  }

We can retrieve state variable values, but what about assigning them? To start, let's handle the simple case of expressions of the form x = expr or x' = expr. 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:

      case EQUAL:
        if (left instanceof UnboundVariable) {
          UnboundVariable var = (UnboundVariable)left;
          state.bindValue(var, right);
          return true;
        }
        return left.equals(right);

Define bindValue() in the State class, which binds the variable's value in next if the UnboundVariable instance is primed and current if it is not:

  void bindValue(UnboundVariable var, Object value) {
    (var.primed() ? next : current).put(var.name().lexeme, value);
  }

We now have everything necessary to define the prime operator. Here's how it should work: in visitUnaryExpr() in the Interpreter class, detect that we are evaluating the prime operator; if so, prime the current state, evaluate the operand as a primed expression, then unprime the state and return the value of the operand.

  public Object visitUnaryExpr(Expr.Unary expr) {
    if (TokenType.PRIME == expr.operator.type) {
      state.prime(expr.operator);
      try {
        return evaluate(expr.expr);
      } finally {
        state.unprime();
      }
    }

Note that we wrap the evaluation in a try/finally similar to in executeBlock(), to restore the interpreter to an ordinary state if the evaluation results in an exception.

We need to put the code at the top of visitUnaryExpr() because the other unary operators evaluate the operand first, but the prime operator changes how the operand is evaluated - it calls state.prime() beforehand! Let's define the prime() and unprime() methods in the State class:

  void prime(Token op) {
    if (primed) {
      throw new RuntimeError(op, "Cannot double-prime expression.");
    }
 
    primed = true;
  }
 
  void unprime() {
    primed = false;
  }

Double-priming an expression is illegal in TLA⁺, so results in a runtime error.

Our code is nice & simple, but unfortunately it has more holes than Swiss cheese. Let's muddy it up with a bunch of error checks.

Null value types like UnboundVariable produce a major annoyance: we now need to sprinkle null checks throughout our evaluation code! Thankfully many null checks are already handled by our existing stable of check-Operand() helpers, but some cases still remain Near the bottom of the Interpreter class, create a new helper method checkIsDefined():

  private void checkIsDefined(Object... operands) {
    for (Object operand : operands) {
      if (operand instanceof UnboundVariable) {
        UnboundVariable var = (UnboundVariable)operand;
        throw new RuntimeError(var.name(), "Use of unbound variable.");
      }
    }
  }

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:

      case EQUAL:
        if (left instanceof UnboundVariable) {
          UnboundVariable var = (UnboundVariable)left;
          checkIsDefined(right);
          state.bindValue(var, right);
          return true;
        }
        checkIsDefined(left, right);
        return left.equals(right);

A null check also must be added to the LEFT_BRACE case of visitVariadicExpr(); we can't let the user construct sets full of undefined values!

      case LEFT_BRACE:
        Set<Object> set = new HashSet<Object>();
        for (Expr parameter : expr.parameters) {
          Object value = evaluate(parameter);
          checkIsDefined(value);
          set.add(value);
        }

First, we have to think about initial states. Not all components of a TLA⁺ spec are actions; the initial state is a predicate only on unprimed variables. What if we are in the initial state and process an expression containing a primed variable? It should result in an error. Add another field to State indicating whether the interpreter is in the initial state; as you might expect, this is initially true:

class State {
  private boolean initialState = true;
  private boolean primed = false;

In bindValue(), raise an error if the user attempts to bind the value of a primed variable in the initial state:

 void bindValue(UnboundVariable var, Object value) {
    if (var.primed() && initialState) {
      throw new RuntimeError(var.name(),
          "Cannot prime variable in initial state.");
    }

Later we'll look at how to transition beyond the initial state.