learning_tla/notation.md

• Comments
  • Line comments start with a * comment
  • Multiline comments use (* comment *)
  • In PlusCal algorithms: (* --algorithm ... *)
  • Repeated dashes, at least four, are ignored, used just for readability, except to mark the start of a --- MODULE <name> ----
  • Repeated equal signs, at least four, terminate a MODULE definition
• Every value in TLA+ is a set. So every element of a set is also a set, so every set is a set of sets.
  • 1..3 is a set of three elements, but we don't know what their elements are.
• BOOLEAN = {TRUE, FALSE}
• ∈ can be written \in
• Quantifiers
  • ∀ can be written \A (any)
  • ∃ can be written \E (exists)
  • Combinations:
    • ∀ x ∈ S, ∀ y ∈ S : can be written ∀ x, y ∈ S
    • ∀ x ∈ S : ∀ y ∈ T : can be written ∀ x ∈ S, y ∈ T
    • ∀ x ∈ S : ∀ y ∈ T : ∀ z ∈ T : ∀ p ∈ U : ∀ q ∈ V : can be written
      ∀ x ∈ S, y, z ∈ T, p ∈ U , q ∈ V :
• Sets

  • Simple: {e : x ∈ S}

  • Union is the union of all given sets:
    

    UNION {1..3, {0, 5}, 2..7, {6, 7}} 
    * equals
    1..3 ∪ {0,5} ∪ 2..7 ∪ {6,8}
    * equals
    0..8
    

  • UNION (SUBSET S) = S

  • S ⊆ SUBSET (UNION S)

  • SUBSET S is the set of all subsets of S

    • In math
      • this is called the powerset of S
      • this is written 𝒫(S)
    • 𝒫 is not recognized or rendered by TLA+
• CONSTANT Op(_, _) defines dyadic operator Op. In TLC we will be able to tell Toolbox that it is an operator such that e.g. Op(a, b) is a+2*b