learning_tla/learn_tla/topics/01_general.md

General tips

Composite state

Modeling composite state as a struct requires updating all items in every action, possibly using EXCEPT.

Instead, separate each field to its own variable, and actions only update that variables.

THEOREM

THEOREM declares the properties of the spec it belongs to. However, TLC does not do anything with it, so consider it as documentation. This is only used by TLAPS.

PlusCal

Macros

Macros, rather than procedures, are the main form of statement reuse.

Avoid WHILE

While creates one state for each iteration, which can lead to an explosion of concurrency and the number of states.

That's fine when modeling queues, but better avoided for computations. Example

\* BAD
Double:
  while i <= Len(seq) do
    seq[i] := seq[i] * 2;
    i := i + 1;
  end while;

\* GOOD
[i \in 1..Len(seq) |-> seq[i] * 2]

State sweeping

The practice of having a state variable control other state variables, as in, to increase the states generated with no additional complexity.

\* Without
 variable
   seq \in [1..Size -> S]; \* Checks sequences of length 5

\* With state sweeping
 variable
   n \in 1..Size;
   seq \in [1..n -> S]; \* Checks sequences of length 1 to 5

TLA+

UNCHANGED

Since TLA+ Next actions must define every change, using UNCHANGED saves lots of typing.

Helper actions

It can be convenient to split the next-state relations across multiple actions, like this helper:

Trans(agent, a, b) ==
  /\ pc[agent] = a
  /\ pc' = [pc EXCEPT ![agent] = b]
\* used like:
Trans(agent, "state1", "state2")

@

In a function update, @ refers to the old value:

\* Verbose
f' = [f EXCEPT ![1][2].a = f[1][2].a + 1]

\* Clean
f' = [f EXCEPT ![1][2].a = @ + 1]

• @ is the original value of the selected value before replacement
• it is also available in function assignments, which PlusCal converts to EXCEPT: - counter[i] := @ + 1`

Parameterized actions

\* Not parameterized
Add ==
    \E w \in Worker: s' = s \union {w}
Remove ==
    \E w \in Worker: s' = s \ {w}
Next == Add \/ Remove

\* Parameterized
Add(w) == s' = s \union {w}
Remove(w) == s' = s \ {w}
Next ==
  \E in worker:
    \/ Add(w)
    \/ Remove(w)

This is better because we reuse the same value in multiple actions. Imagine you want to add logging to every added or removed worker. This is not easy in the first version (w may not be the same), but easy in the second:

\* Parameterized
Add(w) == s' = s \union {w}
Remove(w) == s' = s \ {w}
Log(w) == log' = Append(log, w)
Next ==
  \E in worker:
    /\ \/ Add(w)
       \/ Remove(w)
    /\ Log(w)

Secure refactorings with actions properties

\* Imagine we created an action including this:
OldAction(user) == seq' = seq \o <<user>>
\* The we refactor it:
NewAction(user) == seq' = Append(seq, user)

We can ensure these are equivalent by creating a property to check that:

\* It is always true that for all users in User the two actions return the same result,
\* all others vars remaining unchanged.
RefactorProp == [][
  \A u \in User: OldAction(user) = NewAction(user)
]_vars

But we can go beyond equality to check that an action is a supserset of the old one:$

\* It is always true that for all users in User the two actions return the same result,
\* all others vars remaining unchanged.
RefactorProp == [][
  \A u \in User: OldAction(user) => NewAction(user)
]_vars