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. The interpreter must keep track of only two states: the current state, and the next state. Each state is a mapping from strings - representing variables - to values. The interpreter also must keep track of the set of declared variables. For this we add three new fields near the top of the Interpreter class:

class Interpreter implements Expr.Visitor<Object>,
                             Stmt.Visitor<Void> {
  final Environment globals;
  private Environment environment;
 
  private final Map<String, Token> variables = new HashMap<>();
  private Map<String, Object> current = null;
  private Map<String, Object> next = new HashMap<>();

We choose to initialize the current state to null because when the interpreter is created, the system's initial state has not yet been defined. The system's initial state will be built in next, which then eventually becomes current.

The new fields are enough to implement visitVarDeclStmt() in the Interpreter class:

  @Override
  public Void visitVarDeclStmt(Stmt.VarDecl stmt) {
    checkNotDefined(stmt.names);
    for (Token name : stmt.names) {
      variables.put(name.lexeme, name);
      next.put(name.lexeme, new UnboundVariable(name));
    }
 
    return null;
  }

This requires a new datatype! What is the value of a variable when it is declared but not yet bound to a value? It must be a new null type, which we will call UnboundVariable. Add UnboundVariable as a new record type near the top of the Interpreter class:

class Interpreter implements Expr.Visitor<Object>,
                             Stmt.Visitor<Void> {
 
  private record UnboundVariable(Token name) {
    @Override
    public String toString() {
      return name.lexeme;
    }
  }
 
  final Environment globals;

It's important to keep variable declarations & operator definitions disjoint. In interpreter mode we continue to support redefining operators, but should produce an error if the user attempts to redefine an operator as a state variable or vice versa. Add the highlighted code to visitOpDefStmt() in the Interpreter class:

  public Void visitOpDefStmt(Stmt.OpDef stmt) {
    checkNotDefined(stmt.params);
    for (Token param : stmt.params) {
      if (param.lexeme.equals(stmt.name.lexeme)) {
        throw new RuntimeError(param, "Identifier already in use.");
      }
    }
 
    if (variables.containsKey(stmt.name.lexeme)) {
      throw new RuntimeError(stmt.name, "State variable redeclared as operator.");
    }
 
    TlaOperator op = new TlaOperator(stmt);

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 (variables.containsKey(name.lexeme)) {
        throw new RuntimeError(name, "Name conflicts with state variable.");
      }
    }

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:

  public Object visitVariableExpr(Expr.Variable expr) {
    Object referent =
      variables.containsKey(expr.name.lexeme)
      ? (primed ? next : current).get(expr.name.lexeme)
      : environment.get(expr.name);
 
    if (!(referent instanceof TlaCallable)) {

This makes use of yet another field we must add to the Interpreter class, primed:

  private Map<String, Object> next = new HashMap<>();
  private boolean primed = true;
 
  public Interpreter(boolean replMode) {

The primed field controls whether variable values are pulled from the current or next states. When inside a primed expression, variables are pulled from next; when outside of primed expressions, variables are pulled from current. 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:

  public Object visitUnaryExpr(Expr.Unary expr) {
    switch (expr.operator.type) {
      case PRIME: {
        if (primed) {
          throw new RuntimeError(expr.operator,
              "Cannot double-prime expression nor prime initial state.");
        } try {
          primed = true;
          return evaluate(expr.expr);
        } finally {
          primed = false;
        }
      } case ENABLED: {

Double-priming an expression or priming an expression in the initial state are both fatal errors in TLA⁺. The meaning of priming an expression is that all state variables within that expression are primed, so the way the expression is evaluated is fundamentally changed. 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.

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. 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 State.UnboundVariable) {
          UnboundVariable var = (UnboundVariable)left;
          next.put(var.name().lexeme, right);
          return true;
        }
        return left.equals(right);

We only modify variable values in next, not current; variable values in current should be considered immutable.

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():

  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));
    }
  }

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.

In TLA⁺, states generally do not have only one successor state. Instead, there are usually multiple possible states to transition to. This is called nondeterminism, and is a key TLA⁺ feature enabling modeling of concurrent scheduling & much more. Nondeterminism is expressed in TLA⁺ through the use of disjunction; for example:

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

The Action predicate matches next states where x is either 0 or 1. This means Action represents a nondeterministic step where the system can arbitrarily move to a state where x is 0, or a state where x is 1.

Currently, we store the next state in a single field in the Interpreter class. How can we represent & compute with multiple possible next states? The answer is to add another field to the Interpreter class, holding the set of identified possible next states:

  private Map<String, Object> current = null;
  private Map<String, Object> next = new HashMap<>();
  private Set<Map<String, Object>> possibleNext = new HashSet<>();
  private boolean primed = true;
 
  public Interpreter(boolean replMode) {

We also update clearNext() to wipe the new possibleNext field:

  private void clearNext() {
    possibleNext = new HashSet<>();
    next = new HashMap<>();

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. We will write this very critical top-level loop now; create a new method getNextStates() in the Interpreter class:

  List<Map<String, Object>> getNextStates(Token location, Expr action) {
 
  }

getNextStates() will use the following algorithm:

1. Clear the next state and push it onto possibleNext
2. While states remain in possibleNext, choose one, set it as next, and evaluate action
3. If action evaluates to true and also results in a complete next state with all variables bound to values, add next to a set of confirmed next states
4. Evaluating action might have pushed more states onto possibleNext, so repeat the process until possibleNext is empty
5. Return the set of confirmed next states

Here's how we set up everything outside of the central loop:

  List<Map<String, Object>> getNextStates(Token location, Expr action) {
    Set<Map<String, Object>> confirmedNext = new HashSet<>();
    clearNext();
    possibleNext.add(new HashMap<>(next));
    try {
      while (!possibleNext.isEmpty()) {
 
      }
    } finally {
      clearNext();
    }
 
    return new ArrayList<>(confirmedNext);
  }

We use the familiar try/finally approach when evaluating expressions within a modified Interpreter state to ensure runtime exceptions do not corrupt the Interpreter instance. We also use the new HashMap<>(next) copy constructor to copy next before putting it in possibleNext, which avoids a very subtle bug: since evaluating the action modifies the values in next, and we put next into a HashMap<> which records its position by calculating a hash of the value of next, if we subsequently modify the same object put into the HashMap<> then that value will get "lost" in the datastructure, because its hash value changed. For more on this peculiar issue, consult the Java Map<> documentation which warns against using mutable objects as keys.

Now we can write the central loop:

      while (!possibleNext.isEmpty()) {
        Map<String, Object> trunk = possibleNext.iterator().next();
        next = new HashMap<>(trunk);
        Object satisfied = evaluate(action);
        checkBooleanOperand(location, satisfied);
        if ((boolean)satisfied && isComplete()) confirmedNext.add(next);
        possibleNext.remove(trunk);
      }

Note again the judicious use of HashMap<> copy constructors to avoid the mutable HashMap<> key bug.

It's worth spending some time considering the getNextStates() method. From a pure functional perspective the approach is quite displeasing; our interpreter isn't just evaluating expressions anymore, it's also spewing out a bunch of half-baked states on the side. This side-effectful method makes it quite a bit harder to reason about the current state of our interpreter, but within the limitations of the Java language the method is appropriate.

There is also the question of termination. What is preventing getNextStates() from entering an infinite loop? The answer is that we only add a state to possibleNext if either it is already in possibleNext (in which case it is de-duplicated) or after binding the value of at least one more variable than is bound in the next state under consideration. Thus the number of variables bound to concrete values in possibleNext increases monotonically, eventually encompassing all declared variables and terminating the loop.

Let's get concrete. How do we add states to possibleNext while evaluating disjunction? For each disjunct, we use a fresh copy of the next state, then evaluate the disjunct and add the resulting modified next state to possibleNext. As described above, this state will either already be in possibleNext (so be de-duplicated) or have bound the value of at least one more state variable. We need to evaluate every disjunct to ensure we find all possible next states, which is why TLA⁺ disjunction does not short-circuit. Modify the OR handling code in visitVariadicExpr() as highlighted:

      case OR:
        boolean result = false;
        Map<String, Object> trunk = next;
        for (Expr disjunct : expr.parameters) {
          next = new HashMap<>(trunk);
          Object junctResult = evaluate(disjunct);
          checkBooleanOperand(expr.operator, junctResult);
          possibleNext.add(new HashMap<>(next));
          result |= (boolean)junctResult;
        }
        return result;
      default:

There are two other operators to support for binding state variables: the set membership \in operator, and the \E existential quantification operator. 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():

      case IN:
        checkSetOperand(expr.operator, right);
        if (left instanceof State.UnboundVariable) {
          UnboundVariable var = (UnboundVariable)left;
          Map<String, Object> trunk = next;
          for (Object element : (Set<?>)right) {
            next = new HashMap<>(trunk);
            next.put(var.name().lexeme, element);
            left = element;
            possibleNext.add(new HashMap<>(next));
          }
          return true;
        }
        return ((Set<?>)right).contains(left);

Then update the EXISTS case of visitQuantFnExpr() as highlighted:

      } case EXISTS: {
        boolean result = false;
        State current = state;
        Map<String, Object> trunk = next;
        for (Environment binding : bindings) {
          next = new HashMap<>(trunk);
          Object junctResult = executeBlock(expr.body, binding);
          checkBooleanOperand(expr.op, junctResult);
          possibleNext.add(new HashMap<>(next));
          result |= (boolean)junctResult;
        }
        return result;

We can now generate all nondeterministic next states by calling getNextStates() with an appropriate action!

Our code is nice & simple, but unfortunately it has more holes than Swiss cheese. Let's add some 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 checkIsValue():

  private void checkIsValue(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;
          checkIsValue(right);
          next.put(var.name().lexeme, right);
          return true;
        }
        checkIsValue(left, right);
        return left.equals(right);

A null check must also must be added to the LEFT_BRACE case in visitVariadicExpr():

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

The ALL_MAP_TO case in visitQuantFnExpr():

      case ALL_MAP_TO: {
        Token param = expr.params.get(0);
        Map<Object, Object> function = new HashMap<>();
        for (Environment binding : bindings) {
          Object value = executeBlock(expr.body, binding);
          checkIsValue(value);
          function.put(binding.get(param), value);
        }
        return function;

And also the visitFnApplyExpr() method:

  public Object visitFnApplyExpr(Expr.FnApply expr) {
    Object callee = evaluate(expr.fn);
    checkFunctionOperand(expr.bracket, callee);
    Object argument = evaluate(expr.argument);
    checkIsValue(argument);
    Map<?, ?> function = (Map<?, ?>)callee;