EWD998ChanID_shiviz.tla

$ java -Dtlc2.value.Values.width=99999 -jar tla2tools.jar \
  -noTE -deadlock -generate -depth 99999 \
  EWD998ChanID_shiviz > ewd998-$(date +%s).txt


* -D...=99999 sets the line width to 99999 chars to prevent line breaks in TLA+
 values when printed by TLC. Otherwise, add more sophisticated regex matching
* "noTE" prevents TLC from generating a trace evaluation spec
* "generate" to not exhaustively check the spec but quickly generate some trace
* "depth" has to be greater than the limit in  Inv  below.  By default, the 
  generator creates traces of length 100


The regex below (without backticks) has to appear on the first line of the input
file for ShiViz. In other words, prepend it to the file  ewd-$(date +%s).txt
generated by TLC.

```
^State (?<event>[0-9]+: <([\w\(\),]+)) .*>\n\/\\ Host = (?<host>.*)\n\/\\ Clock = "(?<clock>.*)"\n\/\\ active = (?<active>.*)\n\/\\ color = (?<color>.*)\n\/\\ counter = (?<counter>.*)
```

------------------------ MODULE EWD998ChanID_shiviz -------------------------
EXTENDS EWD998ChanID, TLC, TLCExt, Json

\* Init  except that  active  and  color  are restricted to TRUE and "white" to
 \* not waste time generating initial states nobody needs.
MCInit ==
  (* Each node maintains a (local) vector clock *)
  (* https://en.wikipedia.org/wiki/Vector_clock *)
  /\ clock = [ n \in Node |-> IF n = Initiator 
                THEN [ m \in Node |-> IF m = Initiator THEN 1 ELSE 0 ]
                ELSE [ m \in Node |-> 0 ] ]
  (* Rule 0 *)
  /\ counter = [n \in Node |-> 0] \* c properly initialized
  /\ inbox = [n \in Node |-> IF n = Initiator 
                              THEN << [type |-> "tok", q |-> 0, color |-> "black", vc |-> clock[n] ] >> 
                              ELSE <<>>] \* with empty channels.
  (* EWD840 *)
  \* Reduce the number of initial states. 
  /\ active \in [Node -> {TRUE}]
  /\ color \in [Node -> {"white"}]

Inv ==
    \* TODO Choose some upper length or a invariant that produces a more
     \* TODO interesting behavior.  If you increase the length, don't forget
     \* TODO to also update TLC's depth parameter.
    TLCGet("level") < 666
    \* A trace ending with  terminationDetected = TRUE  that is longer than 22
     \* steps.
    \*EWD998Chan!EWD998!terminationDetected => TLCGet("level") < 23
    
\* Temporal logics got rid of explicit state indices.  However, when we transform
 \* counter-examples, the annoyances of handling indices re-surface.  Especially,
 \* we are dealing with *finite* prefixes of behaviors.

\* The  n \in Node  whose "variables" changed in the current step compared to
 \* the *predecessor* state.  The parameter  s  represents the current state,
 \* the parameter  t  the predecessor state.
 \* Determining whether or not a node has changed is usually easiest by
 \* introducing a prophecy variable into the spec (see  thread  variable in
 \* https://git.io/JZ0Wb).
host ==
    LET None == "--" \* This should be a model value:  CHOOSE n : n \notin Node
        lvl == TLCGet("level")
        trc == Trace
    IN IF lvl = 1 THEN Initiator
       ELSE CHOOSE n \in Node:
            trc[lvl].clock[n] # trc[lvl-1].clock[n]

Alias == 
    [
        Host |-> host
        ,Clock |-> ToJsonObject(clock[host])
        
        ,active |-> active
        ,color |-> color
        ,counter |-> counter
        ,inbox |-> inbox
    ]

=============================================================================