Add Alias in _shiviz spec with which a trace can be visualized with ShiViz.

Author: lemmy

specifications/ewd998/EWD998ChanID_shiviz.cfg

@@ -0,0 +1,17 @@
+CONSTANTS
+    Node = {n1,n2,n3,n4,n5,n6,n7}
+    Init <- MCInit \* Fewer initial states to speed-up startup.
+
+SPECIFICATION
+    Spec
+
+INVARIANT 
+    Inv
+
+\* The simulator/generator may generate a prefix of a behavior whose length is
+ \* less than what we wish to see.
+CHECK_DEADLOCK 
+    FALSE
+
+ALIAS
+    Alias

specifications/ewd998/EWD998ChanID_shiviz.tla

@@ -0,0 +1,81 @@
+
+
+$ 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 [0-9]+: <(?<event>\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 ==
+  (* Rule 0 *)
+  /\ counter = [n \in Node |-> 0] \* c properly initialized
+  /\ inbox = [n \in Node |-> IF n = Initiator 
+                              THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> 
+                              ELSE <<>>] \* with empty channels.
+  (* EWD840 *)
+  \* Reduce the number of initial states. 
+  /\ active \in [Node -> {TRUE}]
+  /\ color \in [Node -> {"white"}]
+  (* Each node maintains a (local) vector clock *)
+  (* https://en.wikipedia.org/wiki/Vector_clock *)
+  /\ clock = [n \in Node |-> [m \in Node |-> 0] ]
+
+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 None
+       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
+    ]
+
+=============================================================================