Log exceptions to the trace and make them fail a trace validation.

Author: lemmy

specifications/ewd998/EWD998ChanTrace.tla

@@ -191,13 +191,23 @@ TraceNextConstraint ==
               \* BP:: line below is the first step towards diagnosing a divergence. Once
               \* hit, advance evaluation with step over (F10) and step into (F11).
               BP::
-                \/ IsInitiateToken(logline)
-                \/ IsPassToken(logline)
-                \/ IsRecvToken(logline)
-                \/ IsSendMsg(logline)
-                \/ IsRecvMsg(logline)
-                \/ IsDeactivate(logline)
-                \/ IsTrm(logline)
+              /\ \/ IsInitiateToken(logline)
+                 \/ IsPassToken(logline)
+                 \/ IsRecvToken(logline)
+                 \/ IsSendMsg(logline)
+                 \/ IsRecvMsg(logline)
+                 \/ IsDeactivate(logline)
+                 \/ IsTrm(logline)
+              \* Fail trace validation if the log contains a failure message. As an alternative,
+               \* we could have used  TraceInv below, which would cause TLC to print the current
+               \* trace upon its violation.  For the sake of consistency, we use the 
+               \*  TraceAccepted  approach for all trace validation.
+              /\ "failure" \notin DOMAIN logline
+
+TraceInv ==
+    LET l == TraceLog[TLCGet("level")] IN
+    /\ "failure" \notin DOMAIN l
+    /\ (l.event \in {"<", ">"} /\ l.pkt.msg.type = "trm") => \A n \in Node: ~active[n]
 
 -----------------------------------------------------------------------------
 

specifications/ewd998/impl/src/EWD998.java

@@ -188,6 +188,8 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
 				assert inbox.isEmpty();
 				return;
 			} else {
+				logline.add("failure", new JsonPrimitive(String.format("Unknown message type: %s", msg.get(TYPE).getAsString())));
+				System.out.println(logline);
 				throw new IllegalArgumentException("Unknown message type");
 			}
 
@@ -354,10 +356,13 @@ private void sendMsg(final int sender, final int receiver, final JsonObject msg)
 				return;
 			} catch (SocketTimeoutException | ConnectException thisIsFineWillRetry) {
 				if (retry > 3) {
-					// Stay silent if it failed less than three times. If it fails more than three
+					// Stay silent if it a transient failure. If it fails more than three
 					// times, the user will likely want to inspect.  Note that EWD998 assumes
 					// reliable message infrastructure and doesn't consider network failure.
 					thisIsFineWillRetry.printStackTrace();
+					logline.add("failure", new JsonPrimitive(thisIsFineWillRetry.toString()));
+					System.out.println(logline);
+					return;
 				}
 				Thread.sleep(500L * retry);
 			}