Support dynamic vector clocks.

modules/VectorClocks.tla

@@ -14,14 +14,45 @@ LOCAL happenedBefore(v1, v2) ==
 IsCausallyOrdered(log, clock(_)) ==
     \A i \in 1..Len(log) :
         \A j \in 1..(i - 1) :
-            \/ happenedBefore(clock(log[j]), clock(log[i]))
-            \/ concurrent(clock(log[j]), clock(log[i]))
+            \* Align the vector clocks to the same domain (mapping
+             \* missing values to 0).  A node gradually learns about
+             \* other nodes, so its clock domain expands over time.
+            LET Fill(c, D) == 
+                    [ d \in D |-> IF d \in DOMAIN c THEN c[d] ELSE 0 ]
+                D   == DOMAIN clock(log[i]) \cup DOMAIN clock(log[j])
+                vci == Fill(clock(log[i]), D)
+                vcj == Fill(clock(log[j]), D)
+            IN happenedBefore(vcj, vci) \/ concurrent(vcj, vci)
 
-SortCausally(log, clock(_), node(_)) ==
+SortCausally(log, clock(_), node(_), domain(_)) ==
     (*
-        Sort the given log based on the vector clock values. The predicates
-        clock and node are used to extract the vector clock and node values
-        from the log entries.
+        Sort the provided log by the vector clock values indicated on each line
+        of the log. This operator cannot accommodate "hidden" events, meaning
+        events that are excluded from the log. The vector clocks must be
+        continuous without any gaps.
+        
+        The predicates clock, node, and domain equals the vector clock from
+        a log entry, the node's clock value, and the clock's domain, i.e., the
+        nodes for which the clock has values.
+        
+        Imagine a log containing lines such as:
+        
+        	[pkt |-> 
+        		[vc |-> 
+        			[1 |-> 20, 
+        			 0 |-> 10,
+        			 3 |-> 16, 
+        			 7 |-> 21, 
+        			 4 |-> 10, 
+        			 6 |-> 21]],
+        	 node |-> 5,
+			 ...
+		    ]
+		 
+		 SortCausally(log, 
+					 	LAMBDA line: line.pkt.vc,
+					 	LAMBDA line: line.node,
+						LAMBDA vc : DOMAIN vc)
     *)
     CHOOSE newlog \in 
         { f \in 

modules/tlc2/overrides/VectorClocks.java

@@ -36,9 +36,11 @@
 
 import tlc2.tool.EvalControl;
 import tlc2.value.impl.Applicable;
+import tlc2.value.impl.Enumerable;
 import tlc2.value.impl.IntValue;
 import tlc2.value.impl.TupleValue;
 import tlc2.value.impl.Value;
+import tlc2.value.impl.ValueEnumeration;
 
 public class VectorClocks {
 
@@ -49,11 +51,13 @@ private static class GraphNode {
 
 		private final Value value;
 		private final Value clock;
+		private final Enumerable domain;
 		private final Value time;
 
-		public GraphNode(final Value clock, final Value time, final Value value) {
+		public GraphNode(final Value clock, final Value time, final Enumerable domain, Value value) {
 			this.clock = clock;
 			this.time = time;
+			this.domain = domain;
 			this.value = value;
 		}
 
@@ -65,6 +69,10 @@ public Value getTime() {
 			return time;
 		}
 
+		public Enumerable getHosts() {
+			return domain;
+		}
+
 		public boolean hasParents() {
 			return !parents.isEmpty();
 		}
@@ -88,7 +96,8 @@ public Value delete() {
 	 * ff02d48ed2bcda065f326aa25409cb317be9feb9/js/model/modelGraph.js
 	 */
 	@TLAPlusOperator(identifier = "SortCausally", module = "VectorClocks", warn = false)
-	public static Value SortCausally(final TupleValue v, final Applicable opClock, final Applicable opNode) {
+	public static Value SortCausally(final TupleValue v, final Applicable opClock, final Applicable opNode,
+			final Applicable opDomain) {
 
 		// A1) Sort each node's individual log which can be totally ordered.
 		final Map<Value, LinkedList<GraphNode>> n2l = new HashMap<>();
@@ -98,9 +107,10 @@ public static Value SortCausally(final TupleValue v, final Applicable opClock, f
 			final Value nodeId = opNode.apply(new Value[] { val }, EvalControl.Clear);
 			final Value vc = opClock.apply(new Value[] { val }, EvalControl.Clear);
 			final Value nodeTime = vc.select(new Value[] { nodeId });
+			final Enumerable dom = (Enumerable) opDomain.apply(new Value[] { vc }, EvalControl.Clear).toSetEnum();
 
 			final LinkedList<GraphNode> list = n2l.computeIfAbsent(nodeId, k -> new LinkedList<GraphNode>());
-			list.add(new GraphNode(vc, nodeTime, val));
+			list.add(new GraphNode(vc, nodeTime, dom, val));
 		}
 
 		// A2) Totally order each node's vector clocks in the log! They are likely
@@ -132,7 +142,9 @@ public int compare(GraphNode o1, GraphNode o2) {
 				globalClock.put(host, gn.getTime());
 
 				final Value c = gn.getClock();
-				for (Value otherHost : n2l.keySet()) {
+				final ValueEnumeration hosts = gn.getHosts().elements();
+				Value otherHost = null;
+		        while ((otherHost = hosts.nextElement()) != null) {
 					final Value time = c.select(new Value[] { otherHost });
 
 					if (globalClock.get(otherHost).compareTo(time) < 0) {