tlaplus-workshops / ewd998 Goto Github PK

View Code? Open in Web Editor NEW

47.0 67.0 47.0 2 MB

Distributed termination detection on a ring, due to Shmuel Safra:

Home Page: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF

License: MIT License

Shell 4.44% TLA 95.56%

termination detection distsys tlaplus specs model-checking theorem-proving refinement safety liveness

ewd998's Introduction

ewd998

Experience TLA+ in action by specifying distributed termination detection on a ring, due to Shmuel Safra. Each git commit introduces a new TLA+ concept. Go back to the very first commit to follow along!

v00: IDE

Click either one of the buttons to launch a zero-install IDE to give the TLA+ specification language a try:

(=> Screencast how to create the TLA+ Codespace)

v01: Problem statement - Termination detection in a ring

v01a: Termination of pleasingly parallel

For this tutorial, we assume that the distributed system nodes are organized as a ring, with one the (unique) leader[^1]. If we further assume that nodes execute independent computations, (global) termination detection becomes trivial--the leader initiates a token transfer around the ring, and each node passes the token to its next neighbor, iff the node finished its computation. When the initiator receives back the token, it knows that all (other) nodes have terminated.

This problem is too simple, and we don't need TLA+ to model it.

[^1] Perhaps by some leader election algorithm.

v01b: Termination of collaborative computation

A more interesting problem is to look at a "collaborative" computation, which implies that nodes can re-activate each other. For example, the result of a computation at node 23 is (atomically!) sent to and further processed at node 42. With the previous protocol, node 42 might have already passed on the token, causing the initiator to eventually detect (global) termination; a bug that is at least difficult to reproduce with testing! A solution is offered in EWD840:

Initiator sends a "stateful" token around the ring
Each node remembers if it activated another node
Activation taints the token (when the activator gets the token)
Initiator keeps running rounds until it receives an untainted token

v01c: Termination detection with asynchronous message delivery

What happens if we loosen the restriction that message delivery is atomic (it seldom is)? Clearly, we are back at square one:

Node 23 sends a message to 42
23 taints the token
Initiator starts a new round
Node 42 received the fresh token before receiving the activation message from 23
Boom!

The fix proposed in Shmuel Safra's EWD998, is to count in-flight messages. But will this work?

Throughout the chapters of this tutorial, we will use the TLA+ specification language to model EWD998, and check interesting properties.

v02: High-level spec AsyncTerminationDetection

TLA+ is all about abstraction, and, as we will later see, has first-class support to connect different levels of abstraction. Let's use this and write a basic spec that either falsifies our design above, or gives us sufficient confidence to invest in writing a more detailed spec.

(Credit: Stephan Merz wrote AsyncTerminationDetection)

v02a: Spec skeleton

Instead of modeling message channels, let alone modeling the transport layer, we will write a spec that models:

A ring of N nodes
The activation status of each node
The number of messages pending[^2] at a node
A send action
A receive action
A terminate action
The initial configuration of the system

Please switch to AsyncTerminationDetection.tla and read its comments. From here on, the tutorial continues there...

[^2] It's difficult to (efficiently) count pending messages in an implementation. In a TLA+ spec, we don't care about that notion of efficiency. Also, all variables are global.

ewd998's People

Contributors

Stargazers

Watchers

ewd998's Issues

Workshop Agenda

Part A

Basics
Actions
Invariants
Implication
Implied Init & Box/Always
[A]_v
Temporal Formual: Spec
ENABLED
<<A>>_v
Diamond/Eventually (liveness)
Stuttering
<>[] and []<>
Fairness
Weak Fairness
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 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

TLA+ statistics with EWD840

Animations

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

Interesting mistakes

The bug below only causes a safety violation on Dijkstra's invariant Inv with N >= 4 and not with N=3, unless Init defines token.pos \in Node. It is also caught by ATDSpec with N=4 iff the CHOOSE in SendMsg is replaced with existential quantification (\E n \in Node: pending' = ...). Note that EWD840 (synchronous msg delivery) catches the corresponding bug with N=3.

However, it can be found with N=3 when checking Inv with MCEWD998!IInit as the initial-state predicate, or with high probability with SmokeEWD998 (starting with commit "v03d06").

diff --git a/EWD998.tla b/EWD998.tla
index 1218c4c..7ad9eab 100644
--- a/EWD998.tla
+++ b/EWD998.tla
@@ -107,7 +107,8 @@ PassToken(i) ==
     \* Wow, TLA+ has an IF-THEN-ELSE expressions.
     /\ token' = [ token EXCEPT !.pos = @ - 1,
                                !.q   = @ + counter[i],
-                               !.color = IF color[i] = "black" THEN "black" ELSE @ ]
+                               \* Let a node that is not the initiator reset the token
+                               \* color from white to black.
+                               !.color = color[i] ]
     \* Rule 7
     /\ color' = [ color EXCEPT ![i] = "white" ]
     /\ UNCHANGED <<active, pending, counter>>

Invariant Inv is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "black", pos |-> 0]
2: <InitiateProbe line 93, col 5 to line 100, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 3]
3: <PassToken line 104, col 5 to line 114, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
4: <SendMsg line 124, col 5 to line 142, col 41 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 1)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
5: <RecvMsg line 146, col 5 to line 152, col 26 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> -1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
6: <SendMsg line 124, col 5 to line 142, col 41 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
7: <RecvMsg line 146, col 5 to line 152, col 26 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
8: <Deactivate line 156, col 5 to line 158, col 51 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "black" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
9: <PassToken line 104, col 5 to line 114, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "black", pos |-> 1]
10: <PassToken line 104, col 5 to line 114, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE @@ 3 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white" @@ 3 :> "black")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 0]

Apalache

diff --git a/MCEWD998.cfg b/MCEWD998.cfg
index d998f17..bf37484 100644
--- a/MCEWD998.cfg
+++ b/MCEWD998.cfg
@@ -1,6 +1,6 @@
-CONSTANT N = 3
+CONSTANT N = 4
 SPECIFICATION Spec
-INVARIANT TypeOK
-INVARIANT Inv
-CONSTRAINT StateConstraint
-PROPERTY ATDSpec
\ No newline at end of file
+\* INVARIANT TypeOK
+INVARIANT InvA
+\* CONSTRAINT StateConstraint
+\* PROPERTY ATDSpec
\ No newline at end of file

$ apalache-mc check --config=MCEWD998.cfg APEWD998.tla
# APALACHE
# version: 0.23.1
# build  : eec2386
#
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Output directory: /workspaces/ewd998/_apalache-out/APEWD998.tla/2022-04-11T21-13-41_1792518047804052883
Checker options: check --config=MCEWD998.cfg APEWD998.tla         I@21:13:41.927
Tuning:                                                           I@21:13:41.930
PASS #0: SanyParser                                               I@21:13:41.938
Parsing file /workspaces/ewd998/APEWD998.tla
Parsing file /workspaces/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
Parsing file /workspaces/ewd998/AsyncTerminationDetection.tla
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@21:13:42.451
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.453
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.462
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@21:13:42.528
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@21:13:42.528
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.564
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.565
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.572
Substitution of ENABLED needs care. The current implementation may fail to work. W@21:13:42.572
PASS #1: TypeCheckerSnowcat                                       I@21:13:42.629
 > Running Snowcat .::.                                           I@21:13:42.629
 > Your types are purrfect!                                       I@21:13:43.680
 > All expressions are typed                                      I@21:13:43.680
PASS #2: ConfigurationPass                                        I@21:13:43.681
  > MCEWD998.cfg: Loading TLC configuration                       I@21:13:43.684
Fairness constraints are ignored by Apalache: WF_vars()(System()) W@21:13:43.732
  > MCEWD998.cfg: Using SPECIFICATION Spec                        I@21:13:43.733
  > Using the init predicate Init from the TLC config             I@21:13:43.733
  > Using the next predicate Next from the TLC config             I@21:13:43.733
  > MCEWD998.cfg: found INVARIANTS: InvA                          I@21:13:43.733
  > Set the initialization predicate to Init                      I@21:13:43.734
  > Set the transition predicate to Next                          I@21:13:43.735
  > Set an invariant to InvA                                      I@21:13:43.735
  > Replaced CONSTANT N with 4                                    I@21:13:43.737
PASS #3: DesugarerPass                                            I@21:13:43.753
  > Desugaring...                                                 I@21:13:43.754
PASS #4: UnrollPass                                               I@21:13:43.771
  > Unroller                                                      I@21:13:43.822
PASS #5: InlinePass                                               I@21:13:43.843
  > InlinerOfUserOper                                             I@21:13:43.844
  > Wrap                                                          I@21:13:43.913
  > CallByNameOperatorEmbedder                                    I@21:13:43.924
  > LetInExpander                                                 I@21:13:43.930
  > Unwrap                                                        I@21:13:43.938
  > InlinerOfUserOper                                             I@21:13:43.945
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, InvA, Next I@21:13:43.962
PASS #6: PrimingPass                                              I@21:13:43.963
  > Introducing InitPrimed for Init'                              I@21:13:43.966
PASS #7: VCGen                                                    I@21:13:43.967
  > Producing verification conditions from the invariant InvA     I@21:13:43.968
  > VCGen produced 2 verification condition(s)                    I@21:13:43.977
PASS #8: PreprocessingPass                                        I@21:13:43.979
  > Before preprocessing: unique renaming                         I@21:13:43.979
 > Applying standard transformations:                             I@21:13:43.988
  > PrimePropagation                                              I@21:13:43.989
  > Desugarer                                                     I@21:13:43.995
  > UniqueRenamer                                                 I@21:13:44.004
  > Normalizer                                                    I@21:13:44.025
  > Keramelizer                                                   I@21:13:44.037
  > After preprocessing: UniqueRenamer                            I@21:13:44.064
PASS #9: TransitionFinderPass                                     I@21:13:44.097
  > Found 1 initializing transitions                              I@21:13:44.167
  > Found 5 transitions                                           I@21:13:44.206
  > No constant initializer                                       I@21:13:44.208
  > Applying unique renaming                                      I@21:13:44.209
PASS #10: OptimizationPass                                        I@21:13:44.227
 > Applying optimizations:                                        I@21:13:44.237
  > ConstSimplifier                                               I@21:13:44.238
  > ExprOptimizer                                                 I@21:13:44.250
  > SetMembershipSimplifier                                       I@21:13:44.258
  > ConstSimplifier                                               I@21:13:44.263
PASS #11: AnalysisPass                                            I@21:13:44.272
 > Marking skolemizable existentials and sets to be expanded...   I@21:13:44.275
  > Skolemization                                                 I@21:13:44.276
  > Expansion                                                     I@21:13:44.277
  > Remove unused let-in defs                                     I@21:13:44.282
 > Running analyzers...                                           I@21:13:44.289
  > Introduced expression grades                                  I@21:13:44.294
PASS #12: PostTypeCheckerSnowcat                                  I@21:13:44.294
 > Running Snowcat .::.                                           I@21:13:44.295
 > Your types are purrfect!                                       I@21:13:45.457
 > All expressions are typed                                      I@21:13:45.458
PASS #13: BoundedChecker                                          I@21:13:45.458
State 0: Checking 2 state invariants                              I@21:13:45.882
Step 0: picking a transition out of 1 transition(s)               I@21:13:46.058
State 1: Checking 1 state invariants                              I@21:13:46.077
Step 1: Transition #1 is disabled                                 I@21:13:46.178
Step 1: Transition #2 is disabled                                 I@21:13:46.226
State 1: Checking 2 state invariants                              I@21:13:46.256
State 1: Checking 1 state invariants                              I@21:13:46.444
Step 1: picking a transition out of 3 transition(s)               I@21:13:46.486
State 2: Checking 1 state invariants                              I@21:13:46.522
State 2: Checking 1 state invariants                              I@21:13:46.603
State 2: Checking 2 state invariants                              I@21:13:46.698
State 2: Checking 2 state invariants                              I@21:13:46.904
State 2: Checking 1 state invariants                              I@21:13:47.203
Step 2: picking a transition out of 5 transition(s)               I@21:13:47.281
State 3: Checking 1 state invariants                              I@21:13:47.322
State 3: Checking 1 state invariants                              I@21:13:47.406
State 3: Checking 2 state invariants                              I@21:13:47.522
State 3: Checking 2 state invariants                              I@21:13:48.006
State 3: Checking 1 state invariants                              I@21:13:50.544
Step 3: picking a transition out of 5 transition(s)               I@21:13:50.598
State 4: Checking 1 state invariants                              I@21:13:50.636
State 4: Checking 1 state invariants                              I@21:13:50.696
State 4: Checking 2 state invariants                              I@21:13:50.852
State 4: Checking 2 state invariants                              I@21:13:59.775
State 4: Checking 1 state invariants                              I@21:14:44.987
Step 4: picking a transition out of 5 transition(s)               I@21:14:45.091
State 5: Checking 1 state invariants                              I@21:14:45.149
State 5: Checking 1 state invariants                              I@21:14:45.212
State 5: Checking 2 state invariants                              I@21:14:45.569
State 5: Checking 2 state invariants                              I@21:18:26.774
State 5: Checking 1 state invariants                              I@21:28:34.318
Step 5: picking a transition out of 5 transition(s)               I@21:28:34.730
State 6: Checking 1 state invariants                              I@21:28:34.851
State 6: Checking 1 state invariants                              I@21:28:34.930
State 6: Checking 2 state invariants                              I@21:28:36.108
State 6: Checking 2 state invariants                              I@22:35:41.744
State 6: Checking 1 state invariants                              I@01:17:45.200
Step 6: picking a transition out of 5 transition(s)               I@01:17:46.201
State 7: Checking 1 state invariants                              I@01:17:46.364
State 7: Checking 1 state invariants                              I@01:17:46.454
State 7: Checking 2 state invariants                              I@01:17:49.560
^C<unknown>: error when rewriting to SMT: SMT 0: z3 reports UNKNOWN. Maybe, your specification is outside the supported logic. E@01:23:53.686
at.forsyte.apalache.tla.bmcmt.SmtEncodingException: SMT 0: z3 reports UNKNOWN. Maybe, your specification is outside the supported logic.
        at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.sat(Z3SolverContext.scala:457)
        at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.satOrTimeout(Z3SolverContext.scala:464)
        at at.forsyte.apalache.tla.bmcmt.smt.RecordingSolverContext.satOrTimeout(RecordingSolverContext.scala:204)
        at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.sat(TransitionExecutorImpl.scala:312)
        at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.sat(FilteredTransitionExecutor.scala:143)
        at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.sat(ConstrainedTransitionExecutor.scala:108)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2(SeqModelChecker.scala:280)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2$adapted(SeqModelChecker.scala:266)
        at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
        at scala.collection.immutable.List.foreach(List.scala:431)
        at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:266)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6(SeqModelChecker.scala:184)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6$adapted(SeqModelChecker.scala:148)
        at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
        at scala.collection.immutable.List.foreach(List.scala:431)
        at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:148)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:70)
        at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:58)
        at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:131)
        at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:87)
        at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
        at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$3(PassChainExecutor.scala:44)
        at scala.Option.flatMap(Option.scala:271)
        at at.forsyte.apalache.infra.passes.PassChainExecutor.$anonfun$run$1(PassChainExecutor.scala:43)
        at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
        at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
        at scala.collection.immutable.List.foldLeft(List.scala:91)
        at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
        at at.forsyte.apalache.tla.Tool$.runAndExit(Tool.scala:169)
        at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:248)
        at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:115)
        at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:115)
        at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:404)
        at at.forsyte.apalache.tla.Tool$.runForModule(Tool.scala:394)
        at at.forsyte.apalache.tla.Tool$.run(Tool.scala:115)
        at at.forsyte.apalache.tla.Tool$.main(Tool.scala:53)
        at at.forsyte.apalache.tla.Tool.main(Tool.scala)
Please report an issue at [https://github.com/informalsystems/apalache/issues]: at.forsyte.apalache.tla.bmcmt.SmtEncodingException: SMT 0: z3 reports UNKNOWN. Maybe, your specification is outside the supported logic.
A bug report template has been generated at [/workspaces/ewd998/_apalache-out/APEWD998.tla/2022-04-11T21-13-41_1792518047804052883/BugReport.md].
If you choose to use it, please complete the template with a description of the expected behavior.
It took me 0 days  4 hours 10 min 12 sec                          I@01:23:53.708
Total time: 15012.350 sec                                         I@01:23:53.709
EXITCODE: ERROR (255)

Warmup exercises

Set theory refresher
https://github.com/tlaplus-workshops/ewd998/blob/main/F.tla

Meta reading

New VSCode Dev Container for TLA+

I have a vague memory of you asking for help to produce a VSCode dev container for TLA+. I've created one, borrowing the basic set-up (but not your commit history) from your installer shell script. The container runs Ubuntu 22.04 and supports auto-reparse-on-file-save, LaTeX pretty printing and preview, graphviz visualization, all the usual tools, etc.

I did this mainly for my own students' use, but figured you might be interested in having a look. It's on GitHub if you want to take a look: https://github.com/kevinsullivan/TLAPlusDocker. Fork it, clone your fork into a container in VSCode, let the container build, and you're up and running. Comes with working red light example.

Kevin Sullivan
University of Virginia Computer Science
[email protected]

Plot histogram for variable counter

diff --git a/MCEWD998.cfg b/MCEWD998.cfg
index d998f17..75f0f3d 100644
--- a/MCEWD998.cfg
+++ b/MCEWD998.cfg
@@ -1,6 +1,9 @@
 CONSTANT N = 3
+CONSTANT Init <- StatsInit
 SPECIFICATION Spec
+CONSTRAINT Stats
 CONSTRAINT StateConstraint
\ No newline at end of file
+CONSTRAINT Plot
\ No newline at end of file
diff --git a/MCEWD998.tla b/MCEWD998.tla
index 4ce9ddd..8540b60 100644
--- a/MCEWD998.tla
+++ b/MCEWD998.tla
@@ -1,5 +1,38 @@
 ------------------------------- MODULE MCEWD998 -------------------------------
-EXTENDS EWD998
+EXTENDS EWD998, CSV, TLC, FiniteSets, Sequences, IOUtils
+
+-----------------------------------------------------------------------------
+
+StatsInit ==
+    (* Just a single initial state. *)
+    /\ active \in [Node -> {TRUE}]
+    /\ pending = [i \in Node |-> 0]
+    (* Rule 0 *)
+    /\ color \in [Node -> {"black"}]
+    /\ counter = [i \in Node |-> 0]
+    /\ pending = [i \in Node |-> 0]
+    /\ token = [pos |-> 0, q |-> 0, color |-> "black"]
+
+
+CSVFile ==
+    "MCEWD998.csv"
+
+ASSUME
+    (* Write CSV header at startup *)
+    CSVRecords(CSVFile) = 0 => CSVWrite("n#counter", <<>>, CSVFile)
+
+Stats ==
+    \* Cfg: CONSTRAINT Stats
+    \A n \in Node: CSVWrite("%1$s#%2$s", <<n, counter[n]>>, CSVFile)
+
+Plot ==
+    \* Cfg: CONSTRAINT Plot
+    \* level 2 and not 1 because all initial states are generated at startup.
+    TLCGet("level") = 2 =>
+        IOExec(<<
+            "/usr/bin/env", "Rscript",
+            "MCEWD998.R", CSVFile>>).exitValue = 0
+-----------------------------------------------------------------------------
 
 (***************************************************************************)
 (* Bound the otherwise infinite state space that TLC has to check.         *)

MCEWD998.R

#!/usr/bin/env Rscript
args = commandArgs(trailingOnly=TRUE)

svg("MCEWD998.svg")

d <-
  read.csv(
    header = TRUE, sep = '#', 
       file = args[1])

hist(d$counter, 
     main='EWD840!counter', 
     xlab ='Number of Messages', 
     xlim = c(min(d$counter), max(d$counter)))

dev.off()

Errata, Typos & Improvements

Rename InitiateProbe to something that conveys that multiple rounds get initiated
Rename Terminate actions to GoIdle to convey that nodes do not shut down
Remove superfluous pending = ... conjunct in EWD998!Init
Alternative to "inconclusive round" would be a "failed probe"
Add _apalache-out to hidden files in .vscode/settings.json

[Accessibility] Handwriting in EWD998 is difficult to read

The handwriting in EWD998 is difficult to read and has zero accessibility.

https://twitter.com/lemmster/status/1580294056105893889

/cc @alzarei

EWD998 in Webexplorer

https://lemmster.de/tla-web/?specpath=.%2Fspecs%2FEWD998.tla#

TLA+ cheat sheet

Incremental cheat sheet showing the ASCII syntax.

Prior Work:

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.