The implementation took two hours and did not involve running the code.

Disclaimer: The code first used a home-grown wire format that we replaced
with Json to remove error-prone ad-hoc parsing.

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

[Bug]

Notice that logging happes at two points in time when the system is in a
consistent state; a) when a message is received^1 and b) when a message
is sent.

1 A message is conceptually received, not when the receiver thread accepts
  the message from the ServerSocket, but when the message is taken out
  of the inbox.  While it might be tempting to log in the receiver thread,
  it would break the happen-before relationship of some log statements.
  For example, it could appear as if a node first received a payload
  message that activated the node, and it then passes the token (which
  a node is only allowed to do when it is inactive).

The approach by Ron Pressler [1] does not work well for validating a trace that is extremely partial, i.e., it only contains messages that cross the network.  EWD998's trace neither has the values of all variables nor logs every state of the system.  Using non-determinism to define the missing values and states is not practical, as we end up in a TLA+ fragment that TLC cannot handle, such as the following sub-formula of the next-state relation, where the first conjunct defines an infinite set of functions from which the second conjunction filters an infinite subset of functions.

```tla
SomeAct ==
    /\ ...
    /\ inbox' \in [Node -> Seq(Msg)]
    /\ \E idx \in DOMAIN inbox[Initiator]':
            inbox[Initiator][idx]' = Trace[TLCGet("level")].msg
    /\ ...
```

A workaround is to define TLC state and action constraints that match each line in the trace to the current state of a prefix of some behavior defined by the original spec.  The trace can only be mapped to a behavior iff TLC can match every line in the trace to a state in the prefix.  If not, a TLC postcondition will be violated the unmatched logline.

[1] https://www.youtube.com/watch?v=TP3SY0EUV2A

…al clock, which is why the trace/log file is unordered. For example, the receiver of a message might log the receipt of a message before the sender logs the send event. The canonical solution in distributed systems is a vector clock.

Note that EWD998ChanID models a vector clock to interface with https://bestchai.bitbucket.io/shiviz/

… ShiViz (https://bestchai.bitbucket.io/shiviz).

Regex:

^{"event":"(<|>|d)","node":(?<host>[0-9]?),"pkt":{("snd":(?<src>[0-9]?),"rcv":(?<rcv>[0-9]?),"msg":(?<event>({"type":"tok","q":-?[0-9]*,"color":"(white|black)"}|{"type":"(pl|trm|w|d)"})),|)"vc":(?<clock>.*)}}

…98Chan models token passing as a single, atomic step, but in a real system, passing the token is not atomic. The token is transmitted via the network.

To handle this problem, this technique introduces (explicit) stuttering steps, where the variables remain unchanged, but the length of the behavior increases.

…nodes deactivating are not logged in the implementation. This leads to a rejected trace when a seemingly active node passes the token.

TLC's limitation in supporting the composition of actions (compare section 7.3 (page 76ff) of Lamport's Specifying Systems) prevents the  TraceSpec  from defining its next-state relation by conjoining  Deactivate \cdot PassToken.  However, this limitation can be overcome by defining a suitable action that deactivates the node when it passes the token.

… 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.

…rmination ("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.

The SendMsg action in the high-level specification does not allow a message to be sent from a node to itself.  While self-messaging is safe and does not violate the properties of the specification, the implementation will be changed instead.

…nerating approximately 10k states.

The initiator initiates another token round even when the previous token round is conclusive. The system is in this state after a token round with all nodes white and inactive except for an active but white initiator.

This is a first attempt at a bugfix.

```
<< "Failed matching the trace to (a prefix of) a behavior:",
   [ pkt |->
         [ vc |->
               [ 1 |-> 342,
                 3 |-> 300,
                 0 |-> 216,
                 2 |-> 341,
                 5 |-> 313,
                 4 |-> 313,
                 6 |-> 320,
                 7 |-> 413 ],
           msg |-> [type |-> "pl"],
           snd |-> 0,
           rcv |-> 7 ],
     event |-> "<" ],
   "TLA+ debugger breakpoint hit count 2576" >>  FALSE
Error: Assumption line 212, col 5 to line 215, col 84 of module EWD998ChanTrace is false.
...
```

after generating approximately 10k states." and finally implement the
EWD998 specification.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

… EWD998Chan where possible.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

…allowed ('config' was unexpected)

[Build]