======= 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.
===== Declaring State Variables =====
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 names",
"Print : Token location, Expr expression",
"OpDef : Token name, List 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 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
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
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 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.");
}
}
===== Reading & Priming 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:
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 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.
===== Setting State Variables =====
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.
===== Nondeterminism =====
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 current = null;
private Map next = new HashMap<>();
private Set> 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> getNextStates(Token location, Expr action) {
}
''getNextStates()'' will use the following algorithm:
- Clear the ''next'' state and push it onto ''possibleNext''
- While states remain in ''possibleNext'', choose one, set it as ''next'', and evaluate ''action''
- 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
- Evaluating ''action'' might have pushed more states onto ''possibleNext'', so repeat the process until ''possibleNext'' is empty
- Return the set of confirmed next states
Here's how we set up everything outside of the central loop:
List> getNextStates(Token location, Expr action) {
Set> 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 ''[[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:
while (!possibleNext.isEmpty()) {
Map 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 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 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 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!
===== The ENABLED Operator =====
Now that we've written ''getNextStates()'', we can fully define the ''ENABLED'' prefix operator!
An expression ''ENABLED Action'' evaluates to ''true'' if ''Action'' produces at least one possible next state.
So, as simple as a quick call to ''getNextStates()'' to see whether it returns an empty list or not!
Well, not quite - the ''ENABLED'' operator can possibly be evaluated //inside// an action, so inside a call to ''getNextStates()''!
This means we need some extra ceremony to stash the current values of ''next'' and ''possibleNext'', then restore them using the standard ''try''/''finally'' block method.
Add the highlighted code to the ''ENABLED'' case in ''visitUnaryExpr()'':
} case ENABLED: {
Map oldNext = next;
Set> oldPossibleNext = possibleNext;
try {
clearNext();
return !getNextStates(expr.operator, expr.expr).isEmpty();
} finally {
next = oldNext;
possibleNext = oldPossibleNext;
}
} case NOT: {
This is a big milestone: we now have fully defined //everything// in our minimal TLA⁺ language subset!
We aren't at the end yet, but it's well within sight.
===== Error Checking =====
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
The ''ALL_MAP_TO'' case in ''visitQuantFnExpr()'':
case ALL_MAP_TO: {
Token param = expr.params.get(0);
Map 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;
===== Hooking Up the Interpreter =====
It takes a bit of thought to consider how we should expose our new state-stepping capabilities through the REPL.
One decent approach is to hijack ''Stmt.Print'' statements to trigger steps if they happen to define possible next states.
For this, add the following code to the bottom of the ''run()'' method in the ''TlaPlus'' class:
// Stop if there was a syntax error.
if (hadError) return;
if (replMode && statements.size() == 1
&& statements.get(0) instanceof Stmt.Print) {
tryStep((Stmt.Print)statements.get(0));
} else {
interpreter.interpret(statements);
}
}
This calls a method we'll define in ''TlaPlus'' called ''tryStep()''.
The ''tryStep()'' method should first speculatively execute ''action'' to see what sort of value it returns; if it doesn't return a ''Boolean'', treat it as an ordinary ''Stmt.Print'' statement.
However, if ''action'' //does// return a ''Boolean'', it might be a valid action leading to new states, so call ''getNextStates()''.
If this generates no new states, again treat ''action'' as an ordinary ''Stmt.Print'' statement:
private static void tryStep(Stmt.Print action) {
Object result = interpreter.executeBlock(action.expression, interpreter.globals);
if (!(result instanceof Boolean)) {
action.accept(interpreter);
return;
}
List> nextStates =
interpreter.getNextStates(action.location, action.expression);
if (nextStates.isEmpty()) {
action.accept(interpreter);
return;
}
}
The ''java.util.Map'' class must be imported at the top of the file:
import java.util.List;
import java.util.Map;
public class TlaPlus {
At this point all that remains is to handle the case of what happens when the ''Stmt.Print'' statement //does// generate possible next states.
The REPL should choose one next state and make ''interpreter'' step to it; add this to the bottom of ''tryStep()'':
List> nextStates =
interpreter.getNextStates(action.location, action.expression);
if (nextStates.isEmpty()) {
System.out.println(false);
return;
}
Map nextState = pickNext(nextStates);
interpreter.setNextState(nextState);
interpreter.step(action.location);
System.out.println(true);
System.out.println(nextState);
}
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'':
void setNextState(Map next) {
this.next = next;
}
The other, in ''TlaPlus'', picks the next state to step to.
If there are multiple possible next states, the user is prompted to choose one:
private static Map pickNext(List> nextStates) {
if (nextStates.size() == 1) {
return nextStates.get(0);
} else {
System.out.println("Select next state (enter number): ");
for (int i = 0; i < nextStates.size(); i++) {
System.out.println(i + ": " + nextStates.get(i));
}
System.out.print("> ");
try (java.util.Scanner in = new java.util.Scanner(System.in)) {
return nextStates.get(in.nextInt());
}
}
}
And that's it!
You can now run the REPL and step through the state space!
Try entering expressions like the following:
- ''VARIABLE x''
- ''x = 0''
- ''x' \in 0 .. 5''
This was a pivotal chapter; excellent work making it to the end.
You can find the expected state of the codebase in [[https://github.com/tlaplus/devkit/tree/main/8-actions|this repository]].
See you in the [[creating:closures|next chapter on closures!]]
[[creating:operators|< Previous Page]] | [[creating:start#table_of_contents|Table of Contents]] | [[creating:closures|Next Page >]]