# Multistep Invariants

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 `actions`.

``````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;
``````

``````MoveInvariant ==