learning_tla/learn_tla/core/10-action-properties.md

10. Action properties

Box action formula

The notation [][Next]_vars is called the box action formula.

bar == <<a, b>
[][Foo]_bar = Foo \/ UNCHANGED bar
            = Foo \/ (a' = a /\ b' = b)
           

Quantified action properties

This notation is not supported by TLC:

 define
CounterOnlyIncreases == 
  \A c \in Counters:
    [][values[c]' >= values[c]]_values[c]
end define;  

However, the box operator and universal quantifier are commutative: \A x: []P(x) = [](\A x: P(x))

 define
CounterOnlyIncreases == 
  \A c \in Counters:
    [values[c]' >= values[c]]_values[c]
end define;  

Using action properties

• most specs have
  • more invariants than action properties
  • more action properties than liveness properties
• every spec needs at least one liveness property, while action properties are powerful but optional