learning_tla/learn_tla/core/08-temporal-properties.md

8. Temporal properties

• Invariants are not part of TLA+
• They are part of TLC to simplify thinking of a specific kind of properties
• These properties are described with temporal operators, and are called temporal properties
• 2 kinds of temporal properties
  • safety ones check that the system doesn't do some specific thing badly (e.g. "does not violate DB constraints")
    • Invariants are safety properties
    • Not all safety properties are invariants
  • liveness ones say if always does a specific good thing (e.g. "all transactions either complete or roll back")

[] box operator: always

• []P means that P is true in every state (always true)
• Making P an in variant is actually declaring []P as a property of the model, and that is how TLC actually defines invariants
  • Making P a property rather than []P only checks it in the initial state
• []P \/ []Q means that either P or Q is an invariant, but the behaiour doesn't need to have both.
• []P => []Q declares that P is a stronger invariant than Q
• []<>: always eventually

In the 8.1 orchestrator example, saying that "In every behavior, there is a particular server, and that server is online at all points in time." can be written:

---- MODULE orchestrator ----
Safety == \E s \in Servers: [](s \in online) 
====

We can check that it is being violated if we define it in the CFG as PROPERTY Safety

More generally, the box operator lets us represent all invariants, and many other properties too.

Fairness

[] is just an operator, so can be combined with other ones.

• []~P means P is always not true
• ~[]P is a bit more ambiguous. It could mean two different things:
  • either: in EVERY behaviour, there exists at least one state where P is false
  • or: in AT LEAST ONE behavior, there exists at least one state where P is false
  • Because the EVERY version is more often useful, although the second version is more intuitive, this is how TLA+ interprets it.

Liveness properties must also work when stuttering, and this fails in the orchestrator model when running with the CFG having PROPERTY Liveness: with Liveness == ~[](online = Servers)

Indeed, in the behavior where the model remains on the initial state, stuttering indefinitely, there is never a state where online # Servers, so Liveness is false.

Note that It would not be if TLA+ used the AT LEAST ONE version.

If we do not declare that the system cannot crash (i.e. stutter indefinitely), the model will assume it can.

We declare systems that cannot crash (stop forever) as fair process instead of just process.

This is a weak fairness, just forbidding infinite stuttering, by guaranteeing that if a process can ALWAYS make progress, it will eventually make progress. But it may spinlock.

strong fairness is a more advanced topic, best used in TLA+ than PlusCal, stating that is that if a process can ALWAYS INTERMITTENTLY make progress, it will eventually make progress (not spinlock).

Strong fairness can be declared:

• at the process level using fair+ process <value>
• at the action level, by writing: <label>:+

Note: the examples in that section NEED a SPECIFICATION in the CFG file, else fairness is ignored.

<> diamond operator: eventually

In practice, ~[]P is rarely useful. ~[]~P (sometimes, P is true) is more often useful: this means that P isn't an invariant, but must hold in at least one state.

Note: the examples in that section NEED a SPECIFICATION in the CFG file, else fairness is ignored.

<>[] diamond box: eventually always

• []P means P is ALWAYS true
• <>P means P is EVENTUALLY true
• <>[]P means
  • []P is eventually true
  • P is always eventually true, or eventually P is always true
• []<>: eventually always is equivalent for the threads example, but may be broader in other cases.

This means P can start false, but may switch to true and remain there forever after.

Note: the examples in that section NEED a SPECIFICATION in the CFG file, else fairness is ignored.

~>: leads to operator

Much like P => Q preconditions Q on P, P ~> Q means that if P is true, Q will eventually be true at some point, either immediately or in a future state.

Example for a worker pool, where workers is the set of task sets for each worker:

VARIABLE
  inbound \in SUBSET TaskType

Liveness ==
  \A t \in TaskType:
    t \in inbound 
      ~> \E w in workers:
        t \in worker_pool[w]

This means that every inbound task t will eventually be processed by a worker, (represented by being part of the worker's task set).

When to use liveness

Rarely.

• they are slower than invariants and less fine-grained
• they are harder to write than invariants
• they cannot be used with symmetry sets (cf. 04 parameterizing specs)
• Most systems will have lots of invariants but only a couple of liveness properties
• TLC is currently unable to
  • tell which property is being broken, only that "Temporal properties were violated."
  • provide the shortest trace to an error violation: it may be useful to rerun the model with smaller constants