Trace validation has begun to reject traces due to the presence of termination ("trm") messages in the implementation, which are not included in the EWD998 model. This represents the first discrepancy that has been discovered between the specifications and the actual code, but it is something that could have easily been spotted through a manual comparison between the two.

To resolve this issue, the TraceNextConstraint has been defined to allow for "trm" messages and is based on finite stuttering, similar to the way the IsRecvToken is handled.

Author: lemmy

specifications/ewd998/EWD998ChanTrace.tla

@@ -165,6 +165,20 @@ IsDeactivate(l) ==
         /\ active' = [active EXCEPT ![node] = FALSE]
         /\ UNCHANGED <<color, inbox, counter>>
 
+IsTrm(l) ==
+    \* "trm" messages are not part of EWD998, and, thus, not modeled in EWD998Chan.  We map
+     \* "trm" messages to (finite) stuttering, essentially, skipping the "trm" messages in
+     \* the log.  One could have also preprocessed/filtered the trace log, but the extra
+     \* step is not necessary.
+    /\ l.event \in {"<", ">"}
+    /\ l.pkt.msg.type = "trm"
+    \* The (mere) existance of a "trm" message implies that *all* nodes have terminated.
+    /\ \A n \in Node: ~active[n]
+    \* Careful! Without UNCHANGED vars, isTrm is true of all states of the high-level spec
+     \* if the current line is a trm message.  In general, it is good practice to constrain
+     \* all spec variables!
+    /\ UNCHANGED vars
+
 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.
@@ -186,6 +200,7 @@ TraceNextConstraint ==
                 \/ IsSendMsg(logline)
                 \/ IsRecvMsg(logline)
                 \/ IsDeactivate(logline)
+                \/ IsTrm(logline)
 
 -----------------------------------------------------------------------------