Workshop Agenda

# 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](https://en.wikipedia.org/wiki/Vacuous_truth) formulas ([pitfall](https://lemmster.de/tla-liveness-review.html))
- 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](http://lemmster.de/shiviz/)  (Upstream PR at https://github.com/DistributedClocks/shiviz/pull/169)
* [EWD998ChanID_export](https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998ChanID_export.tla)
* [Screencast EWD840 Json](https://twitter.com/lemmster/status/1337264737516580867)
* [(EWD840_json.tla)](https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/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](https://github.com/lemmy/BlockingQueue/blob/ExperimentalExecutor/impl/src/org/kuppe/TLABlockingQueue.java)
 * [QSort](https://gist.github.com/lemmy/84ab674619c39c55f513ba9003151ed7)
 * https://github.com/tlaplus/CommunityModules/issues/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
* https://github.com/tlaplus/tlaplus/issues/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

Workshop Agenda #1

Description

Part A

Basics ..v02b09

TLA

First invariant TypeOK ..v02b10

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

Property Stable (Box to Box Box) ..v02b18

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

ENABLED ..v02b30

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

Leads-to ..v02b37

Inductive invariant ..v02e03

Part B

Simulate real modeling

Records ..v03a08

IF-THEN-ELSE ..v03a10

CHOOSE ..v03a14

Refinement ..v03b10

CHOOSE again! ..v03c04

Safra's inductive invariant ..03d02

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

Part C

Part D

Multiple nodes terminate simultaneously ..v04a02

Part E

Shiviz/ICG (trace expressions)

Channels

Executing spec with PlusPy & TLC

TLA+ statistics with EWD840

Animations

Activity

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions