Handle (DOMAIN pc) \subseteq Nat.

tlaplus · Oct 1, 2019 · 702f65a · 702f65a
1 parent 6dbdf73
commit 702f65a
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/modules/ShiViz.tla b/modules/ShiViz.tla
@@ -1,4 +1,4 @@
-------------------------------- MODULE ShiViz -------------------------------
+u------------------------------- MODULE ShiViz -------------------------------
 EXTENDS Integers, Json, Toolbox, TLC
 
 -----------------------------------------------------------------------------
@@ -27,7 +27,8 @@ Host == FnHost[_TEPosition]
 -----------------------------------------------------------------------------
 
 LOCAL clock(n) == 
-   [p \in DOMAIN _TETrace[n].pc |-> IF p = FnHost[n] 
+   IF n = 1 THEN [p \in DOMAIN _TETrace[n].pc |-> 0] \* In the init state, all clocks are 0.
+   ELSE [p \in DOMAIN _TETrace[n].pc |-> IF p = FnHost[n] 
                                     THEN 1
                                     ELSE 0]