EOD1

AsyncTerminationDetection.cfg

@@ -0,0 +1,5 @@
+INIT Init
+NEXT Next
+CONSTANT N = 2
+CONSTRAINT OnlyThreeMsgs
+INVARIANT Inv

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

EWD998.cfg

@@ -0,0 +1,9 @@
+INIT Init
+NEXT Next
+INVARIANT Inv
+INVARIANT
+    TypeOK
+    \* NeverTermination
+CONSTANT N = 2
+CONSTRAINT OnlyThreeMsgs
+ALIAS Alias

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 <<active, counter, messages>>
+
+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 <<active, counter, messages>>
+
+Idle(node) ==
+    \* /\ active' = [ n \in Nodes |-> IF n = node THEN FALSE ELSE active[n]]
+    /\ active' = [ active EXCEPT ![node] = FALSE ]
+    /\ UNCHANGED <<token, color, counter, messages>>
+
+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 <<active, color, token>>
+
+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
+
+=====