The previous commit showed how (manually) composed actions can handle…

… missing state changes in the trace/log file, and we see no reason why this approach won't generalize beyond this particular example. With the EWD998 implementation, however, we can (consistently) log when a node deactivates, thereby increasing the coverage of trace validation by including more system state.
tlaplus · Apr 10, 2023 · 55e9a64 · 55e9a64
1 parent ad8988f
commit 55e9a64
Show file tree

Hide file tree

Showing 2 changed files with 26 additions and 12 deletions.
diff --git a/specifications/ewd998/EWD998ChanTrace.tla b/specifications/ewd998/EWD998ChanTrace.tla
@@ -34,21 +34,14 @@ TraceLog ==
 
 -----------------------------------------------------------------------------
 
-DeactivateAndPassToken ==
-    \E i \in Node:
-        /\ PassToken(i)!2
-        /\ PassToken(i)!3
-        /\ active' = [active EXCEPT ![i] = FALSE]
-        /\ UNCHANGED counter
-
 TraceSpec ==
     \* Because of  [A]_v <=> A \/ v=v'  , the following formula is logically
      \* equivalent to the (canonical) Spec formual  Init /\ [][Next]_vars  .  
      \* However, TLC's breadth-first algorithm does not explore successor
      \* states of a *seen* state.  Since one or more states may appear one or 
      \* more times in the the trace, the  UNCHANGED vars  combined with the
      \*  TraceView  that includes  TLCGet("level")  is our workaround. 
-    Init /\ [][Next \/ UNCHANGED vars \/ DeactivateAndPassToken]_vars
+    Init /\ [][Next \/ UNCHANGED vars]_vars
 
 -----------------------------------------------------------------------------
 
@@ -106,8 +99,9 @@ IsPassToken(l) ==
         \* The sender's inbox contains no tok message in the next state.
         /\ \A idx \in DOMAIN inbox'[snd]:
                 inbox'[snd][idx].type # "tok"
-        \* Sender has to be inactive to pass the token, i.e
-        /\ UNCHANGED <<counter>>                            
+        \* Sender has to be inactive to pass the token, i.e.,
+        /\ ~active[snd]
+        /\ UNCHANGED <<active, counter>>                            
 
 IsRecvToken(l) ==
     \* Log statement was printed by the receiver.
@@ -162,6 +156,15 @@ IsRecvMsg(l) ==
          \* inbox.  Thus, thee receiver's inbox contains one less pl message in the next state.
         /\ Len(SelectSeq(inbox[rcv], PayloadPred)) > Len(SelectSeq(inbox'[rcv], PayloadPred))
 
+IsDeactivate(l) ==
+    \* Log statement was printed by the receiver.
+    /\ l.event = "d"
+    /\ LET node == l.node IN
+        \* The receiver and only the receiver transitions to inactive.
+        /\ active[node]
+        /\ active' = [active EXCEPT ![node] = FALSE]
+        /\ UNCHANGED <<color, inbox, counter>>
+
 TraceNextConstraint ==
     \* We could have used an auxiliary spec variable for i  , but TLCGet("level") has the
      \* advantage that TLC continues to show the high-level action names instead of just  Next.
@@ -182,6 +185,7 @@ TraceNextConstraint ==
                 \/ IsRecvToken(logline)
                 \/ IsSendMsg(logline)
                 \/ IsRecvMsg(logline)
+                \/ IsDeactivate(logline)
 
 -----------------------------------------------------------------------------
 
@@ -227,7 +231,6 @@ TraceAlias ==
         enabled |-> 
             [
                 InitToken  |-> ENABLED InitiateProbe,
-                DeAndPass  |-> ENABLED DeactivateAndPassToken,
                 PassToken  |-> ENABLED \E i \in Node \ {0} : PassToken(i),
                 SendMsg    |-> ENABLED \E i \in Node : SendMsg(i),
                 RecvMsg    |-> ENABLED \E i \in Node : RecvMsg(i),

diff --git a/specifications/ewd998/impl/src/EWD998.java b/specifications/ewd998/impl/src/EWD998.java
@@ -34,6 +34,7 @@ public class EWD998 {
 	private static final String NODE = "node";
 	private static final JsonPrimitive IN = new JsonPrimitive("<");
 	private static final JsonPrimitive OUT = new JsonPrimitive(">");
+	private static final JsonPrimitive DEACTIVATE = new JsonPrimitive("d");
 
 	private static final String VC = "vc";
 
@@ -131,7 +132,7 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
 
 			// A log line is a json object with an "event" and a "pkt" field. The
 			// event shows is this is an incoming ("<") or outgoing (">") packet.
-			final JsonObject logline = new JsonObject();
+			JsonObject logline = new JsonObject();
 			logline.add(EVENT, IN);
 			logline.add(NODE, new JsonPrimitive(myId));
 			pkt.add(VC, vc.tickAndMerge(pkt.get(VC).getAsJsonObject()));
@@ -221,6 +222,16 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
 			 */
 			if (active) {
 				active = randomWork.nextDouble() < 0.75d;
+
+				if (!active) {
+					logline = new JsonObject();
+					logline.add(EVENT, DEACTIVATE);
+					logline.add("node", new JsonPrimitive(myId));
+					JsonObject j = new JsonObject();
+					j.add(VC, vc.tick());
+					logline.add(PKT, j);
+					System.out.println(logline);
+				}
 			}
 
 			// --------------------------------------------------------------------------------- //