Agenda/Outline

[lemmy]

Part A

1. Basics
2. Actions
3. Invariants
4. Implication
5. Implied Init & Box/Always
6. [A]_v
7. Temporal Formual: Spec
8. ENABLED
9. <<A>>_v
10. Diamond/Eventually (liveness)
11. Stuttering
12. <>[] and []<>
13. Fairness
14. Weak Fairness
15. Leads-to

Basics ..v02b09

• CONSTANT, VARIABLES, definitions
• set-theory refresher
• Initial predicates and actions
• Functions (arrays), boolean connectives (lists), unchanged and prime
• Predicate logic/FOL - Quantification and non-determinism
• deadlocks, state-space explosion, and small-model hypothesis
• Specs vs. model-checking (MCInit)

TLA

First invariant TypeOK ..v02b10

• Find bug in Wakeup action: @-2
• Variable terminationDetected , priming operators

Property Stable (Implication, Implied Inits and Box) ..v02b13

• Introduce Implication
• P: Rewrite terminated to FALSE and check with TLC to show vacuously true formulas (pitfall)
• P: Revert to original terminated and show that it holds
• V: Add FALSE to MCInit and show that it doesn't actually hold because the current formula is just an Implied Init
• Verification doesn't find the bug unless the faulty state is an initial state
• This is why we need the box operator to say that Stable holds in every state of a behavior; not just the initial states

Property Stable (Box to Box Box) ..v02b18

• V: [](t => td)
  • violated by a behavior of two states (this is an invariant and checked as such)
• V: [](t => []td)
  • we strengthen Stable to turn the invariant into a property to show that TLC checks it differently and hint at "stuttering"
• Have we found flaw?
• P: [](td => []t
  • No, reverse td and t , which is what we actually meant

Be suspicious of success aka non-properties, and Spec ..v02b20

• Run simulation mode to find bogus action constraint (Always be suspicious of success)
• Property OnlyTerminates (subscript of [N]_v <=> N \/ v'=v)
  • Every step is a Termiation step
• These commits bridge to Spec by adding the disjunct of all actions
• Once we arrive at Init /\ [][Next]_vars, we will revisit the implied inits and why it is useful

ENABLED ..v02b30

• P: []ENABLED Next
  • because DetectTermination is permanently enabled and allows vars to remain unchanged)
• V: []ENABLED Next
  • Violation after enablement of DetectTermination is changed
• P: []ENABLED [Next]_v
  • This is a tautology
• V: []ENABLED <<Next>>_vars
  • Violated even with UNCHANGED vars because vars don't change anymore which is stipulated by "Angle A sub variables"
  • This property is violated even with the original definition of DetectTermination that allowed infinite stuttering.

Diamond operator <>, fairness, and machine closure (prophecy) ..v02b35

• V: <>terminationDetected and <>terminated
  • both violated because of lack of fairness
  • Talk about comibining <> and [] into []<> and <>[] to grok (weak fairness below)
• P: F == <>t /\ <>td
  • Turn both properties into fairness properties (not machine closed)
• V: <>[](ENABLED <<Next>>_vars) => []<><<Next>>_vars
  • because fairness is on Next causing a lasso between Send and Wakeup
• V: WF_vars(Next)
  • just syntactic sugar for previous property. The liveness properties are too strong, because we want to allow infinite computations, no?

Leads-to ..v02b37

• P: [](terminated => <>terminationDetected
• P: terminated ~> terminationDetected
  • just syntactic sugar

---

Inductive invariant ..v02e03

• Validate TypeOK with Apalache
• Prove TypeOK
• Validate Stable with Apalache
• Prove Stable

---

Part B

Simulate real modeling

Records ..v03a08

IF-THEN-ELSE ..v03a10

CHOOSE ..v03a14

Refinement ..v03b10

CHOOSE again! ..v03c04

• Meet the TLA+ debugger

Safra's inductive invariant ..03d02

Recursion functions vs. operators and folds (community modules) ..v03d05

---

Part C

Validating inductive invariants (again) ..v03d07

Sketch a real Prove ..v03d08

Proof of refinement of ATD => STD (which is implemented by EWD480) ..v03e01

• Refinement proof EWD998 => AsyncTerminationDetection (inspired by https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_proof.tla)

---

Part D

Multiple nodes terminate simultaneously ..v04a02

---

Part E

Shiviz/ICG (trace expressions)

• EWD998 in Shiviz (Upstream PR at Example log of Safra's EWD998 termination detection in a ring modeled with TLA+ DistributedClocks/shiviz#169)
• EWD998ChanID_export
• Screencast EWD840 Json
• (EWD840_json.tla)

Channels

• Singleton
• refinement can
  • deconstruct variables (token changed from a (record) variable to a message kept in an inbox variable)
  • drop state (payload messages)
• Seq in [Node -> Seq(Message)]

Executing spec with PlusPy & TLC

• TLABlockingQueue
• QSort
• Add PlusPy's Messaging.tla tlaplus/CommunityModules#41
• https://github.com/lemmy/AsyncGameOfLife
• https://github.com/tlaplus/Examples/tree/mku-ewd998/specifications/ewd998
• https://github.com/tlaplus/Examples/commits/mku-ewd998

TLA+ statistics with EWD840

• Evaluate (const- or state-level) expression after generating a behavior in simulation mode tlaplus/tlaplus#601
• https://github.com/lemmy/ewd840/blob/mku-simulate-new/README.md#results

Animations

https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_anim.tla