Specifying multiple steps using TLA+ (Temporal Logic of Actions)

Question

Looking through here mostly shows simple examples of action specifications where you reference the next state using ', as in:

UponV1(self) ==                                 
  /\ pc[self] = "V1"                        
  /\ pc' = [pc EXCEPT ![self] = "AC"]       
  /\ sent' = sent \cup { <<self, "ECHO">> } 
  /\ nCrashed' = nCrashed
  /\ Corr' = Corr

For example, /\ nCrashed' = nCrashed is a logical statement saying "...AND next(nCrashed) == this(nCrashed)`. So basically, the above function sets a few variables "in the next state". But all this happens in one step essentially (logically at least).

What I'm wondering is how to define something that occurs over multiple steps. Say 10 steps.

UpdateWithTenSteps(self) ==                                 
  /\ foo' = foo + 1
  /\ bar'' = foo' + 1
  /\ baz''' = bar'' + 1
  /\ ...
  ....

So "in the third state ahead of now, baz will be set to bar in the second state plus one.". Something like that. But that doesn't really make sense. In an imperative language, you would just do something like this:

function updateInTenSteps() {
  incFoo()
  incBar()
  incBaz()
}

But that makes sense because each function call happens after the one before. But I don't see how to represent this in TLA+.

Wondering how you're supposed to accomplish things that take more than one step in Temporal Logic of Actions+. Another example would be a while loop.

Answer 1

TLA is designed that it considers only the current state and a successor state (or the whole behaviour). You can always split up multiple steps that depend on each other by introducing an explicit variable that tells you which assignments have already been done:

EXTENDS Naturals

Labels == { "foo", "bar", "baz", "fin" } (* just for documentation purposes *)
VARIABLE currstate, foo, baz, bar

Init == /\ currstate = "foo"
        /\ foo = 0
        /\ bar = 0
        /\ baz = 0

Next == \/ (currstate = "foo" /\ currstate' = "bar" /\ foo' = foo +1 /\ UNCHANGED <<bar,baz>>)       
        \/ (currstate = "bar" /\ currstate' = "baz" /\ bar' = foo +1 /\ UNCHANGED <<foo,baz>>)
        \/ (currstate = "baz" /\ currstate' = "fin" /\ baz' = bar +1 /\ UNCHANGED <<foo,bar>>)
        \/ (currstate = "fin" /\ UNCHANGED <<foo,bar,baz,currstate>>

If you create a model for this, set the behaviour as defined by Init and Next, and then check the invariant baz = 0, you will get a trace that shows you the states that lead to the change of baz (your last assignment). A loop just assigns the successor label as one that has already occurred (e.g. instead of defining baz' = "foo").

The Pluscal translation to TLA works similarly: every labeled line corresponds to an id and everye transition from line l to line m will change the program counter in the next state from l to m.