This node possesses the token, and therefore must retain it unchanged.

The resolution of this translation error took approximately 15 minutes and required the execution of the code using a debugger.

[Bug]

Author: lemmy

specifications/ewd998/impl/src/EWD998.java

@@ -224,6 +224,20 @@ public EWD998(final Map<Integer, Pair> nodes, final int myId, final boolean isIn
 					color = Color.white;
 
 					tokenColor = null;
+				} else {
+					// This node owns the token and is active; keep the unchanged token.
+					/*
+						Deactivate(i) ==
+							    /\ ...
+							    /\ UNCHANGED <<..., token>>
+						SendMsg(i) ==
+						    /\ ...
+						    /\ UNCHANGED <<..., token>>
+						RecvMsg(i) ==
+						    /\ ...
+						    /\ UNCHANGED <<token>>
+				     */
+					inbox.add(msg);
 				}
 			}
 		}