If we want to check an invariant only after a specific action, we can use
assert. But what if we want to check an invariant only after a specific sequence of actions? For example, if we move forward and then backwards, we should be in the same position as we started. TLA+ doesn’t provide a native way to test those, but we can use sequences to write our own.
Let’s begin with some framework code:
variables xpos = 0, t = 0 begin Move: while t < 10 do either xpos := xpos + 1 or xpos := xpos - 1 end either; t := t + 1; end while;
In order to test our invariant, we need some way of knowing the previous action, as well as how it changed the position. We can do this by adding a “history” variable, and then appending the last action and state with each step. In the following example, the history variable is named
EXTENDS Integers, TLC, Sequences CONSTANTS EAST, WEST, INIT Action(action, state) == [action |-> action, state |-> state] (* --algorithm alg variables xpos = 0, t = 0, action = INIT actions = <<Action(action, xpos)>>; begin Move: while t < 10 do either xpos := xpos + 1; action := EAST; or xpos := xpos - 1; action := WEST; end either; actions := Append(actions, Action(action, xpos)); t := t + 1; end while; end algorithm; *)
Our invariant is now definable over pairs of the most recent action.
define MoveInvariant == IF Len(actions) > 2 THEN \* require two after init LET len == Len(actions) recent == SubSeq(actions, len-2, len) from == recent.state to == recent.state a == <<recent.action, recent.action>> IN CASE a = <<EAST, EAST>> -> TRUE a = <<EAST, WEST>> -> from = to a = <<WEST, EAST>> -> from = to a = <<WEST, WEST>> -> TRUE ELSE TRUE end define;
We could have replaced two of the cases with
 OTHERWISE -> TRUE, but by enumerating them explicitly, any missed cases will raise an error. Pattern matching!
With a full history, we can also write more sophisticated invariants. For example, in this case, we don’t need to compare the last two actions, since we can operate over the whole history:
MoveInvariant == LET count(token) == Len(SelectSeq(actions, LAMBDA y: y.action = token)) IN xpos = count(EAST) - count(WEST)
Multistep invariants get clunky when you have multiple processes, since you have to store the state, action, and process. Additionally, it gets less useful when applying invariants to complex states.