learning_tla/learn_tla/core/11-tla.md

11. TLA+

From PlusCal to TLA+

Everything must be defined

In TLA+, a boolean operator that contains primed variables is called an action.

In a temporal formula, anything outside a temporal operator is tested as TRUE in the initial (non-primed) state.

Considering the 11.1 Clock example,

Spec == Init /\ [][Next]_vars means Spec == Init /\ [](Next \/ UNCHANGED vars)

So the spec is only true when both Init is initially true, and Next \/ UNCHANGED vars is true at every step, requiring Next to always be true when not stuttering

This formula is called the Next State Relationship. It must always describe ALL variables.

TLC only generates a subset of behaviors for a spec

Consdering this example:

Init == x = 1
Next == x' >= x
Spec == Init /\ [][Next]_x

The behavior 1 -> 9 -> 17 -> 17.1 -> 84 is valid for this spec, but TLC will never generate something like it (floats).

Except

VARIABLE s
Init == s = <<TRUE, FALSE>>
Next == s[1]' = FALSE
Spec == Init /\ [][Next]_s

This fails because s is not defined or is not an operator. That happens because Next only defines the first element of s' not the second. We need to define it completely, and EXCEPT allows us to reuse the initial value and change just what we want:

• Next == s' = [s EXCEPT ![1] = FALSE]
  • ! is called the selector and matches the left argument to EXCEPT
• Next == s' = [s EXCEPT ![1] = FALSE, ![2] = 17]
  • Two (or more) exceptions instead of one
• IncCounter(c) == counter' = [counter EXCEPT ![c] = @ + 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

Modeling concurrency

In the single-label threads example, concurrency is “just” saying there exists an element of the Thread set where thread is true, and thread is just IncCounter because that is the only label.

await P translates to just P.

Fairness in TLA+

• ENABLED means an action can be true. In practice, this is often used to validate that the next step can be taken
• <<A>>_v means that A is true AND v changes.
• Weak fairness means:
  • WF_v(A) == <>[](ENABLED <<A>>_v) => []<><<A>>_v
  • If it is eventually always true that A can happen, then it will happen and change v
• Strong fairness means:
  • SF_v(A) == []<>(ENABLED <<A>>_v) => []<><<A>>_v
  • If it is always eventually true that A can happen, then it will happen and change v
• One consequence of fairness is forbidding infinite stutters.

The fairness constraints are added during PlusCal translation at the end of the definition of Spec.

Fairness beyond processes

In PlusCal, fairness conditions defined on processes apply to labels, which are top-level actions.

In TLA+ they can apply to any action.