Erik's mods to EWD998 from class on 2022-07-12

[xkrogen]

Primarily closely read the paper's description of the algorithm and made changes to match the spec to the text description. One of the biggest changes was that nodes get marked as tainted when they RECEIVE a message, not when they SEND a message. Whoops! There were also minor changes necessary to match the token's initial state (I think we previously marked it tainted at the start if the initiator is tainted, but that's not right, the token always starts untained and the initiator's taint status gets checked when the token makes its way back around).

I also had to make small adjustments to the ATD spec, most notably to change the WF criteria to only check for Terminate, instead of Next. Not sure if that's "cheating", but I think it makes sense based on my understanding: as with EWD998, we don't want to force nodes to send/rcv messages indefinitely, we just want to ensure that we detect termination.

I validated this up to 3 nodes, and am trying on 4, though it has been running for multiple hours and generated 10M+ states without finishing...