ewd998
ewd998 copied to clipboard
Published
20 hours ago •
tlaplus-workshops
tlaplus-workshops
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)
