From 59f691f8b5d74f1ab545c64595d02715a26596b8 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 3 Oct 2023 09:59:01 +0000 Subject: [PATCH] EOD1 --- AsyncTerminationDetection.cfg | 5 ++ AsyncTerminationDetection.tla | 72 +++++++++++++----- EWD998.cfg | 9 +++ EWD998.tla | 138 ++++++++++++++++++++++++++++++++++ 4 files changed, 206 insertions(+), 18 deletions(-) create mode 100644 AsyncTerminationDetection.cfg create mode 100644 EWD998.cfg create mode 100644 EWD998.tla diff --git a/AsyncTerminationDetection.cfg b/AsyncTerminationDetection.cfg new file mode 100644 index 0000000..30cfb4d --- /dev/null +++ b/AsyncTerminationDetection.cfg @@ -0,0 +1,5 @@ +INIT Init +NEXT Next +CONSTANT N = 2 +CONSTRAINT OnlyThreeMsgs +INVARIANT Inv \ No newline at end of file diff --git a/AsyncTerminationDetection.tla b/AsyncTerminationDetection.tla index f9bfc70..01daa37 100644 --- a/AsyncTerminationDetection.tla +++ b/AsyncTerminationDetection.tla @@ -24,24 +24,60 @@ CONSTANT N \* * upon startup. ASSUME NIsPosNat == N \in Nat \ {0} -\* TODO Fire up the TLA+ repl (`tlcrepl` in the Terminal > New Terminal) and - \* TODO find out what TLC returns for the following expressions: - \* TODO 23 = "frob" - \* TODO 23 # "frob" \* # is pretty-printed as ≠ - \* TODO {1,2,2,3,3} = {3,1,1,2,3,1} - \* TODO 1 \div 4 - \* TODO 1 \div 0 - \* TODO {1,2,3} \cap {2,3,4} \* \cap pp'ed as ∩ - \* TODO {1,2,3} \cup {2,3,4} \* \cap pp'ed as ∪ - \* TODO {1,2,3} \ {2,3,4} - \* TODO 23 \in {0} \* \in pp'ed as ∈ - \* TODO 23 \in {23, "frob"} - \* TODO 23 \in {"frob", 23} - \* TODO 23 \in {23} \ 23 - \* TODO 23 \in {23} \ {23} - \* TODO 23 \notin {23} \ {23} - \* TODO 10 \in 1..10 - \* TODO 1 \in 1..0 +Nodes == + 0 .. N-1 + +VARIABLE messages, active, terminationDetected + +termination == + \A n \in Nodes: active[n] = FALSE /\ messages[n] = 0 + +Init == + /\ active = [ n \in Nodes |-> TRUE ] + /\ messages = [ n \in Nodes |-> 0] + \* /\ terminationDetected \in {FALSE, termination} + /\ \/ terminationDetected = FALSE + \/ terminationDetected = termination + +Idle(node) == + /\ active' = [ n \in Nodes |-> IF n = node THEN FALSE ELSE active[n]] + /\ active' = [ active EXCEPT ![node] = FALSE' ] + /\ messages' = messages + /\ \/ terminationDetected' = termination' + \/ terminationDetected' = terminationDetected + +SendMsg(snd, rcv) == + /\ active[snd] = TRUE + /\ messages' = [ n \in Nodes |-> IF n = rcv THEN messages[n] + 1 ELSE messages[n] ] + /\ messages' = [ messages EXCEPT ![rcv] = messages[rcv] + 1 ] + /\ messages' = [ messages EXCEPT ![rcv] = @ + 1 ] + /\ active' = active + /\ terminationDetected' = terminationDetected + +RecvMsg(rcv) == + /\ messages[rcv] > 0 + /\ messages' = [ n \in Nodes |-> IF n = rcv THEN messages[n] - 1 ELSE messages[n] ] + /\ active' = [ n \in Nodes |-> IF n = rcv THEN TRUE ELSE active[n]] + /\ terminationDetected' = terminationDetected + +Next == + \E n, m \in Nodes: + \/ Idle(n) + \/ SendMsg(n,m) + \/ RecvMsg(n) + +---- + +Inv == + \* IF terminationDetected THEN termination ELSE TRUE + terminationDetected => termination + \* terminationDetected = termination + +Gooood == + termination => <>terminationDetected + +OnlyThreeMsgs == + \A n \in Nodes: messages[n] < 4 ============================================================================= \* Modification History diff --git a/EWD998.cfg b/EWD998.cfg new file mode 100644 index 0000000..d72b2b1 --- /dev/null +++ b/EWD998.cfg @@ -0,0 +1,9 @@ +INIT Init +NEXT Next +INVARIANT Inv +INVARIANT + TypeOK + \* NeverTermination +CONSTANT N = 2 +CONSTRAINT OnlyThreeMsgs +ALIAS Alias \ No newline at end of file diff --git a/EWD998.tla b/EWD998.tla new file mode 100644 index 0000000..afbc3cc --- /dev/null +++ b/EWD998.tla @@ -0,0 +1,138 @@ +----- MODULE EWD998 ----- + +EXTENDS Naturals, Integers + +\* * A constant is a parameter of a specification. In other words, it is a + \* * "variable" that cannot change throughout a behavior, i.e., a sequence + \* * of states. Below, we declares N to be a constant of this spec. + \* * We don't know what value N has or even what its type is; TLA+ is untyped and + \* * everything is a set. In fact, even 23 and "frob" are sets and 23="frob" is + \* * syntactically correct. However, we don't know what elements are in the sets + \* * 23 and "frob" (nor do we care). The value of 23="frob" is undefined, and TLA+ + \* * users call this a "silly expression". +CONSTANT N + +\* * We should declare what we assume about the parameters of a spec--the constants. + \* * In this spec, we assume constant N to be a (positive) natural number, by + \* * stating that N is in the set of Nat (defined in Naturals.tla) without 0 (zero). + \* * Note that the TLC model-checker, which we will meet later, checks assumptions + \* * upon startup. +ASSUME NIsPosNat == N \in Nat \ {0} + +Black == "b" +White == "w" + +Color == {Black, White} + +Initiator == 0 + +Nodes == + 0 .. N-1 + +VARIABLE messages, active, color, counter, token + +TypeOK == + /\ messages \in [ Nodes -> Nat ] + /\ active \in [Nodes -> BOOLEAN ] + /\ counter \in [Nodes -> Int ] + /\ color \in [Nodes -> Color] + /\ token \in [ pos: Nodes, color: Color, q: Int ] + +termination == + \A n \in Nodes: active[n] = FALSE /\ messages[n] = 0 + +TerminationDetected == + /\ token.pos = 0 + /\ token.color = White + /\ token.q + counter[0] = 0 + /\ active[0] = FALSE + /\ color[0] = White + +Init == + /\ messages = [ n \in Nodes |-> 0] + /\ active = [ n \in Nodes |-> TRUE ] + /\ color = [ n \in Nodes |-> White ] + /\ counter = [ n \in Nodes |-> 0 ] + /\ token = [ pos |-> 0, q |-> 0, color |-> Black ] \* ???? N-1 + +InitiateToken == + /\ token.pos = 0 + /\ token' = [ token EXCEPT !["pos"] = N - 1, !.q = 0, !.color = White] + /\ color' = [color EXCEPT ![0] = White] + /\ UNCHANGED <> + +PassToken == + /\ ~ active[token.pos] + /\ token.pos # 0 + /\ color' = [ color EXCEPT ![token.pos] = White] + /\ token' = [ token EXCEPT !.pos = @ - 1, + !.color = IF color[token.pos] = Black THEN Black ELSE @, + !.q = @ + counter[token.pos] ] + /\ UNCHANGED <> + +Idle(node) == + \* /\ active' = [ n \in Nodes |-> IF n = node THEN FALSE ELSE active[n]] + /\ active' = [ active EXCEPT ![node] = FALSE ] + /\ UNCHANGED <> + +SendMsg(snd, rcv) == + /\ active[snd] = TRUE + \* /\ messages' = [ n \in Nodes |-> IF n = rcv THEN messages[n] + 1 ELSE messages[n] ] + \* /\ messages' = [ messages EXCEPT ![rcv] = messages[rcv] + 1 ] + /\ messages' = [ messages EXCEPT ![rcv] = @ + 1 ] + /\ counter' = [ counter EXCEPT ![snd] = @ + 1] + /\ UNCHANGED <> + +RecvMsg(rcv) == + /\ messages[rcv] > 0 + /\ messages' = [ messages EXCEPT ![rcv] = @ - 1 ] + /\ active' = [ active EXCEPT ![rcv] = TRUE ] + \* eceiving a *message* (not token) blackens the (receiver) node + /\ color' = [color EXCEPT ![rcv] = Black] + \* /\ UNCHANGED color + \* the receipt of a message decrements i's counter + /\ counter' = [ counter EXCEPT ![rcv] = @ - 1] + /\ UNCHANGED token + +Next == + \E n, m \in Nodes: + \/ Idle(n) + \/ SendMsg(n,m) + \/ RecvMsg(n) + \/ PassToken + \/ InitiateToken + +---- + +OnlyThreeMsgs == + \A n \in Nodes: messages[n] < 4 /\ counter[n] \in -3..3 + + +Inv == + TerminationDetected => termination + +NeverTermination == + termination = FALSE + +Good == + termination => <>TerminationDetected + + +Alias == + [ + active |-> active, + color |-> color, + counter |-> counter, + messages |-> messages, + token |-> token, + TD |-> TerminationDetected, + t |-> termination + ] +\***** +===== +ATD => Inv +ATD => Goood + +EWD998 => ATD + +===== \ No newline at end of file