search

tlaplus-workshops / ewd998

Distributed termination detection on a ring, due to Shmuel Safra:
https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF
MIT License
50 stars 47 forks source link

Interesting mistakes #2

Open lemmy opened 3 years ago

lemmy commented 3 years ago

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]

EWD998-BogusResetColor

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)
lemmy commented 3 years ago

Commenting a disjunct in the enablement condition of InitiateProbe causes a liveness bug, but does not violate the invariant Inv, nor the safety part of the property ATDSpec. This is a great example that Dijkstra's (inductive) invariant just defines safety; not liveness.

diff --git a/AsyncTerminationDetection.tla b/AsyncTerminationDetection.tla
index a471b3d..9c42925 100644
--- a/AsyncTerminationDetection.tla
+++ b/AsyncTerminationDetection.tla
@@ -337,7 +337,7 @@ Spec ==
      \* a  DetectTermination  eventually happens instead of repeated token rounds.
     \* TODO Convince yourself that  AsyncTerminationDetection  is still correct
      \* TODO and  EWD998  passes, i.e., rerun TLC.
-    Init /\ [][Next]_vars /\ WF_vars(DetectTermination) (*  F  *)
+    Init /\ [][Next]_vars

 Terminates ==
     \* * The behavior spec  Spec  asserts that every step/transition is a  Next  step, or
diff --git a/EWD998.tla b/EWD998.tla
index 1218c4c..9128f97 100644
--- a/EWD998.tla
+++ b/EWD998.tla
@@ -93,7 +93,7 @@ InitiateProbe ==
     /\ token.pos = 0
     /\ \* previous round inconclusive:
         \/ token.color = "black"
-        \/ color[0] = "black"
+        \* \/ color[0] = "black"
         \/ counter[0] + token.q > 0
     /\ token' = [ pos |-> N-1, q |-> 0, color |-> "white"]
lemmy commented 3 years ago

Commenting the conjunct below leads to a violation of the safety part of the property ATDSpec. The counter-example is interesting because it shows that ATDSpec is an action-property; the violation is the value of tD in state #8 reverting to false after being true in state #7. The high-level spec AsyncTerminationDetection doesn't allow behaviors where its variable terminationDetection changes from true to false.

diff --git a/EWD998.tla b/EWD998.tla
index 344ce88..3b83e66 100644
--- a/EWD998.tla
+++ b/EWD998.tla
@@ -262,7 +262,7 @@ terminationDetected ==
     /\ token.pos = 0
     /\ token.color = "white"
     /\ token.q + counter[0] = 0
-    /\ color[0] = "white"
+    \* /\ color[0] = "white"
     /\ ~ active[0]

 \* We haven't checked anything except the  TypeOK  invariant above, which does
Alias ==
    [
        active |-> active
        ,color |-> color
        ,counter |-> counter
        ,pending |-> pending
        ,token |-> token
        ,atdterm |-> ATD!terminated
        ,tD |-> terminationDetected
        ,tDExt |-> terminationDetected /\ color[0] = "white"
]
Action property line 333, col 13 to line 333, col 25 of module AsyncTerminationDetection is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "black", pos |-> 0]
/\ atdterm = FALSE
/\ tD = FALSE
/\ tDExt = FALSE
2: <InitiateProbe line 93, col 5 to line 100, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
/\ atdterm = FALSE
/\ tD = FALSE
/\ tDExt = FALSE
3: <SendMsg line 123, col 5 to line 141, col 41 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> 0 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 1 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
/\ atdterm = FALSE
/\ tD = FALSE
/\ tDExt = FALSE
4: <RecvMsg line 145, col 5 to line 151, col 26 of module EWD998>
/\ active = (0 :> TRUE @@ 1 :> FALSE @@ 2 :> TRUE)
/\ color = (0 :> "black" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
/\ atdterm = FALSE
/\ tD = FALSE
/\ tDExt = FALSE
5: <Deactivate line 160, col 5 to line 163, col 51 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ color = (0 :> "black" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
/\ atdterm = TRUE
/\ tD = FALSE
/\ tDExt = FALSE
6: <PassToken line 104, col 5 to line 113, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ color = (0 :> "black" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 1, color |-> "white", pos |-> 1]
/\ atdterm = TRUE
/\ tD = FALSE
/\ tDExt = FALSE
7: <PassToken line 104, col 5 to line 113, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ color = (0 :> "black" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 1, color |-> "white", pos |-> 0]
/\ atdterm = TRUE
/\ tD = TRUE
/\ tDExt = FALSE
8: <InitiateProbe line 93, col 5 to line 100, col 45 of module EWD998>
/\ active = (0 :> FALSE @@ 1 :> FALSE @@ 2 :> FALSE)
/\ color = (0 :> "white" @@ 1 :> "white" @@ 2 :> "white")
/\ counter = (0 :> -1 @@ 1 :> 0 @@ 2 :> 1)
/\ pending = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ token = [q |-> 0, color |-> "white", pos |-> 2]
/\ atdterm = TRUE
/\ tD = FALSE
/\ tDExt = FALSE
lemmy commented 2 years ago

Omitting color' = [ color EXCEPT ![0] = "white" ] in InitiateToken causes a liveness bug that cannot be detected by Inv or the safety-part of ATDSpec.

lemmy commented 1 year ago

Merging PassToken into Terminate, i.e., only passing the token when a node terminates, introduces a liveness bug, s.t. an inactive node will never pass the token.