Search code examples
functionspecificationstla+

How to use TLA+ to define sequential actions?

Say I have a simple set of sequential actions (which I will first define imperatively):

start(a, 1)
move(a, 3)
move(a, 5)
move(a, 4)
move(a, 2)

That is, we have a game piece a and start it at position 1. Then we move it sequentially first to 3, then to 5, then 4, then 2. Once per step.

How would you define this using TLA+? Trying to wrap my mind around how to specify complicated imperative action sequences in TLA+.

Solution

  • The behaviours sketched in the question could be described in TLA+ as follows:

    ---- MODULE Steps ----

VARIABLE a


Init == a = 1
Next == \/ /\ a = 1
           /\ a' = 3
        \/ /\ a = 3
           /\ a' = 5
        \/ /\ a = 5
           /\ a' = 4
        \/ /\ a = 4
           /\ a' = 2

Spec == Init /\ [][Next]_a /\ WF_a(Next)

=====================

    The behavior of variable a is specified by the temporal formula Spec (other variables can behave in arbitrary ways).

    The variable a starts equal to 1 (by the conjunct Init), and a temporal step either leaves a unchanged, or it changes it from 1 to 3. If this change occurs, then the following temporal steps either leave a unchanged, or change it from 3 to 5. The changes of value to a may continue until a equals 2. Further changes to a are impossible. Once a becomes equal to 2, it remains forever equal 2. These are the possible changes of a, as specified by the conjunct [][Next]_a, which means [](Next \/ UNCHANGED a), i.e., [](Next \/ (a' = a)), with the symbol [] meaning "always".

    The conjuncts Init and [][Next]_a specify a safety property. Safety is about what can happen, not what must happen. Liveness (what must happen) is specified with the conjunct WF_a(Next), which describes weak fairness. The formula WF_a(Next) requires that if a step that satisfies the formula Next and changes the value of variable a is enabled uninterruptedly, then such a step must eventually occur.

    In other words, if it is possible to change variable a by taking a step that satisfies Next (a <<Next>>_a-step), then a cannot remain forever unchanged, but must eventually change in a way that is described by Next. Indeed, while a is not 2, but 1, 3, 5, or 4, action <<Next>>_a (which means Next /\ (a' # a), i.e., Next and a changes value) is enabled, so a will keep changing until it reaches the value 2. When a is 2, <<Next>>_a becomes disabled.