Interesting mistakes #2
Comments
|
Commenting a disjunct in the enablement condition of 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"] |
|
Commenting the conjunct below leads to a violation of the safety part of the property 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 doesAlias ==
[
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 |
|
Omitting |
|
Merging |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The bug below only causes a safety violation on Dijkstra's invariant
InvwithN >= 4and not withN=3, unlessInitdefinestoken.pos \in Node. It is also caught byATDSpecwithN=4iff theCHOOSEinSendMsgis replaced with existential quantification (\E n \in Node: pending' = ...). Note that EWD840 (synchronous msg delivery) catches the corresponding bug withN=3.However, it can be found with
N=3when checkingInvwithMCEWD998!IInitas the initial-state predicate, or with high probability withSmokeEWD998(starting with commit "v03d06").Apalache
The text was updated successfully, but these errors were encountered: