diff --git a/modules/VectorClocks.tla b/modules/VectorClocks.tla new file mode 100644 index 0000000..f1bd15b --- /dev/null +++ b/modules/VectorClocks.tla @@ -0,0 +1,33 @@ +---------------------------- MODULE VectorClocks ------------------------------- +EXTENDS Naturals, Sequences, Functions + +LOCAL concurrent(v1, v2) == + \* One or more of the clock values of v1 are less than v2's value. + \E i,j \in DOMAIN v1: i # j /\ v1[i] < v2[i] /\ v1[j] > v2[j] + +LOCAL happenedBefore(v1, v2) == + \* A vector clock v1 is said to happen before v2 if for all nodes, + \* x[n] <= y[n] , and there exists at least one node such that + \* x[h] < y[h]. + /\ \A i \in DOMAIN v1: v1[i] <= v2[i] + /\ \E i \in DOMAIN v1: v1[i] < v2[i] + +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])) + +SortCausally(log, clock(_), node(_)) == + (* + 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. + *) + CHOOSE newlog \in + { f \in + [ 1..Len(log) -> Range(log)] : + Range(f) = Range(log) } : + IsCausallyOrdered(newlog, clock) + +=============================================================================== \ No newline at end of file diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index 7967afb..24d7040 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -45,7 +45,7 @@ public Class[] get() { Json.resolves(); return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, - DyadicRationals.class, Statistics.class }; + DyadicRationals.class, Statistics.class, VectorClocks.class }; } catch (NoClassDefFoundError e) { // Remove this catch when this Class is moved to `TLC`. System.out.println("gson dependencies of Json overrides not found, Json module won't work unless " @@ -53,6 +53,6 @@ public Class[] get() { } return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, - Statistics.class }; + Statistics.class, VectorClocks.class }; } } diff --git a/modules/tlc2/overrides/VectorClocks.java b/modules/tlc2/overrides/VectorClocks.java new file mode 100644 index 0000000..369ae8b --- /dev/null +++ b/modules/tlc2/overrides/VectorClocks.java @@ -0,0 +1,168 @@ +/******************************************************************************* + * Copyright (c) 2023 Microsoft Research. All rights reserved. + * + * The MIT License (MIT) + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is furnished to do + * so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN + * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION + * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + * + * Contributors: + * Markus Alexander Kuppe - initial API and implementation + ******************************************************************************/ +package tlc2.overrides; + +import java.util.ArrayList; +import java.util.Comparator; +import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import tlc2.tool.EvalControl; +import tlc2.value.impl.Applicable; +import tlc2.value.impl.IntValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; + +public class VectorClocks { + + private static class GraphNode { + + private final Set parents = new HashSet<>(); + private final Set children = new HashSet<>(); + + private final Value value; + private final Value clock; + private final Value time; + + public GraphNode(final Value clock, final Value time, final Value value) { + this.clock = clock; + this.time = time; + this.value = value; + } + + public Value getClock() { + return clock; + } + + public Value getTime() { + return time; + } + + public boolean hasParents() { + return !parents.isEmpty(); + } + + public void addParent(GraphNode p) { + this.parents.add(p); + p.children.add(this); + } + + public Value delete() { + // Remove this node from its children, i.e., reduce the in-degree of this node's + // children by one. + this.children.forEach(g -> g.parents.remove(this)); + return value; + } + } + + /* + * The implementation is inspired by (MIT licensed) ShiViz. Specifically: + * https://github.com/DistributedClocks/shiviz/blob/ + * 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) { + + // A1) Sort each node's individual log which can be totally ordered. + final Map> n2l = new HashMap<>(); + for (int j = 0; j < v.elems.length; j++) { + final Value val = v.elems[j]; + + 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 LinkedList list = n2l.computeIfAbsent(nodeId, k -> new LinkedList()); + list.add(new GraphNode(vc, nodeTime, val)); + } + + // A2) Totally order each node's vector clocks in the log! They are likely + // already be ordered, because a single process is unlike to have its log + // reordered. + n2l.values().forEach(list -> list.sort(new Comparator() { + @Override + public int compare(GraphNode o1, GraphNode o2) { + // It suffices the compare the node's vector clock value because a node's vector + // clock value is incremented on every receive: "Each time a process receives a + // message, it increments its own logical clock in the vector by one and ...' + return o1.getTime().compareTo(o2.getTime()); + } + })); + + // ----------------------------------------------------------------------- // + + // B) Merge the totally ordered logs into a directed acyclic graph (DAG). + for (Value host : n2l.keySet()) { + final LinkedList list = n2l.get(host); + + // Initialize the global vector clock. + final Map globalClock = new HashMap<>(); + n2l.keySet().forEach(h -> globalClock.put(h, IntValue.ValZero)); + + for (int i = 0; i < list.size(); i++) { + final GraphNode gn = list.get(i); + + globalClock.put(host, gn.getTime()); + + final Value c = gn.getClock(); + for (Value otherHost : n2l.keySet()) { + final Value time = c.select(new Value[] { otherHost }); + + if (globalClock.get(otherHost).compareTo(time) < 0) { + globalClock.put(otherHost, time); + int idx = ((IntValue) time).val - 1; + gn.addParent(n2l.get(otherHost).get(idx)); + } + } + } + } + + // ----------------------------------------------------------------------- // + + // C) Pop one of the DAG's roots (zero in-degree) and append it to the list. We + // know that at least one head of lists will be a root. + final List sorted = new ArrayList<>(v.elems.length); + int i = 0; + while (i++ < v.elems.length) { + for (Value host : n2l.keySet()) { + final LinkedList list = n2l.get(host); + if (list.isEmpty()) { + continue; + } + if (!list.peek().hasParents()) { + final GraphNode g = list.remove(); + sorted.add(g.delete()); + } + } + } + assert sorted.size() == v.elems.length; + return new TupleValue(sorted.toArray(new Value[sorted.size()])); + } +} diff --git a/tests/AllTests.tla b/tests/AllTests.tla index 5d5901a..addf89e 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -17,6 +17,7 @@ EXTENDS SequencesExtTests, GraphsTests, BagsExtTests, DyadicRationalsTests, - StatisticsTests + StatisticsTests, + VectorClocksTests =========================================== diff --git a/tests/VectorClocksTests.ndjson b/tests/VectorClocksTests.ndjson new file mode 100644 index 0000000..8c2320a --- /dev/null +++ b/tests/VectorClocksTests.ndjson @@ -0,0 +1,271 @@ +{"event":"<","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":1,"1":0,"2":0,"3":0}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":2,"1":0,"2":0,"3":0}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":3,"1":0,"2":0,"3":0}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":3,"1":0,"2":0,"3":1}}} +{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":2,"1":0,"2":1,"3":0}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":2,"1":0,"2":2,"3":0}}} +{"event":"d","node":2,"pkt":{"vc":{"0":2,"1":0,"2":3,"3":0}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":2,"1":1,"2":2,"3":0}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":2,"1":2,"2":2,"3":0}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":3,"1":0,"2":0,"3":2}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":3,"1":2,"2":2,"3":3}}} +{"event":"<","node":0,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":4,"1":0,"2":0,"3":2}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":3,"1":2,"2":2,"3":4}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":5,"1":0,"2":0,"3":2}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":5,"1":2,"2":2,"3":5}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":5,"1":2,"2":2,"3":6}}} +{"event":"d","node":3,"pkt":{"vc":{"0":5,"1":2,"2":2,"3":7}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":2,"2":2,"3":8}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":2,"2":4,"3":8}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":2,"2":5,"3":8}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":3,"2":5,"3":8}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":5,"1":4,"2":5,"3":8}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":5,"2":5,"3":8}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":5,"1":4,"2":6,"3":8}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":5,"1":6,"2":5,"3":8}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":5,"1":4,"2":7,"3":8}}} +{"event":"d","node":1,"pkt":{"vc":{"0":5,"1":7,"2":5,"3":8}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":5,"1":8,"2":5,"3":8}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":5,"1":9,"2":7,"3":8}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":6,"1":8,"2":5,"3":8}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":7,"1":8,"2":5,"3":8}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":7,"1":8,"2":5,"3":9}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":7,"1":8,"2":5,"3":10}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":7,"1":8,"2":8,"3":10}}} +{"event":"d","node":2,"pkt":{"vc":{"0":7,"1":8,"2":9,"3":10}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":7,"1":8,"2":10,"3":10}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":7,"1":10,"2":10,"3":10}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":7,"1":11,"2":10,"3":10}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":7,"1":12,"2":10,"3":10}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":8,"1":11,"2":10,"3":10}}} +{"event":"d","node":1,"pkt":{"vc":{"0":7,"1":13,"2":10,"3":10}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":7,"1":14,"2":10,"3":10}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":0,"color":"black"},"vc":{"0":9,"1":14,"2":10,"3":10}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":10,"1":14,"2":10,"3":10}}} +{"event":"d","node":0,"pkt":{"vc":{"0":11,"1":14,"2":10,"3":10}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":10,"1":15,"2":10,"3":10}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":12,"1":14,"2":10,"3":10}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":12,"1":14,"2":10,"3":11}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":14,"2":10,"3":12}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":14,"2":11,"3":12}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":14,"2":12,"3":12}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":10,"1":16,"2":10,"3":10}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":17,"2":12,"3":12}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":12,"1":16,"2":13,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":18,"2":12,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":19,"2":12,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":20,"2":12,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":21,"2":12,"3":12}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":12,"1":22,"2":12,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":23,"2":12,"3":12}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":12,"1":22,"2":14,"3":12}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":12,"1":22,"2":15,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":12,"1":24,"2":15,"3":12}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"white"},"vc":{"0":12,"1":25,"2":15,"3":12}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":12,"1":26,"2":15,"3":12}}} +{"event":"d","node":1,"pkt":{"vc":{"0":12,"1":27,"2":15,"3":12}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":13,"1":26,"2":15,"3":12}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":12,"1":28,"2":15,"3":12}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":14,"1":26,"2":15,"3":12}}} +{"event":"d","node":0,"pkt":{"vc":{"0":15,"1":26,"2":15,"3":12}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":16,"1":28,"2":15,"3":12}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":14,"1":26,"2":15,"3":13}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":17,"1":28,"2":15,"3":12}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":14,"1":26,"2":15,"3":14}}} +{"event":"d","node":3,"pkt":{"vc":{"0":14,"1":26,"2":15,"3":15}}} +{"event":"<","node":0,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":18,"1":28,"2":15,"3":14}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":17,"1":28,"2":15,"3":16}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":17,"1":28,"2":15,"3":17}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":17,"1":28,"2":16,"3":17}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":19,"1":28,"2":15,"3":14}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":19,"1":29,"2":15,"3":14}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":19,"1":30,"2":15,"3":14}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":20,"1":30,"2":15,"3":14}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":17,"1":28,"2":17,"3":17}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":17,"1":28,"2":18,"3":17}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":21,"1":30,"2":15,"3":14}}} +{"event":"d","node":0,"pkt":{"vc":{"0":22,"1":30,"2":15,"3":14}}} +{"event":"<","node":0,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":23,"1":30,"2":17,"3":17}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":30,"2":17,"3":17}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":30,"2":17,"3":18}}} +{"event":"d","node":3,"pkt":{"vc":{"0":24,"1":30,"2":17,"3":19}}} +{"event":"d","node":2,"pkt":{"vc":{"0":17,"1":28,"2":19,"3":17}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":17,"1":28,"2":20,"3":17}}} +{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"pl"},"vc":{"0":21,"1":30,"2":21,"3":17}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":19,"1":31,"2":20,"3":17}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":19,"1":32,"2":20,"3":17}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":19,"1":33,"2":20,"3":17}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":21,"1":32,"2":22,"3":17}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":19,"1":34,"2":20,"3":17}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":34,"2":20,"3":20}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":19,"1":35,"2":20,"3":17}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":1,"msg":{"type":"pl"},"vc":{"0":24,"1":34,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":3,"rcv":1,"msg":{"type":"pl"},"vc":{"0":24,"1":36,"2":20,"3":21}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":21,"1":32,"2":23,"3":17}}} +{"event":"<","node":3,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":34,"2":23,"3":22}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":37,"2":20,"3":21}}} +{"event":"d","node":3,"pkt":{"vc":{"0":24,"1":34,"2":23,"3":23}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":24,"1":38,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":39,"2":20,"3":21}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":25,"1":38,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":40,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":41,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":42,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":43,"2":20,"3":21}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":24,"1":44,"2":20,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":45,"2":20,"3":21}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":24,"1":44,"2":24,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":46,"2":20,"3":21}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":24,"1":44,"2":25,"3":21}}} +{"event":"d","node":2,"pkt":{"vc":{"0":24,"1":44,"2":26,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":24,"1":47,"2":25,"3":21}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":48,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":49,"2":25,"3":21}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":24,"1":48,"2":25,"3":24}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":50,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":51,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":52,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":53,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":54,"2":25,"3":21}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":24,"1":55,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-1,"color":"black"},"vc":{"0":24,"1":56,"2":25,"3":21}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":26,"1":55,"2":25,"3":21}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":24,"1":57,"2":25,"3":21}}} +{"event":"d","node":1,"pkt":{"vc":{"0":24,"1":58,"2":25,"3":21}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":6,"color":"black"},"vc":{"0":24,"1":59,"2":25,"3":21}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":27,"1":55,"2":25,"3":21}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":28,"1":57,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":27,"1":60,"2":25,"3":21}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":29,"1":57,"2":25,"3":21}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":6,"color":"black"},"vc":{"0":30,"1":59,"2":25,"3":21}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":29,"1":61,"2":25,"3":21}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":31,"1":59,"2":25,"3":21}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":31,"1":59,"2":25,"3":25}}} +{"event":"d","node":3,"pkt":{"vc":{"0":31,"1":59,"2":25,"3":26}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-4,"color":"black"},"vc":{"0":31,"1":59,"2":25,"3":27}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-4,"color":"black"},"vc":{"0":31,"1":59,"2":27,"3":27}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":31,"1":59,"2":28,"3":27}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":31,"1":62,"2":28,"3":27}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":63,"2":28,"3":27}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":31,"1":64,"2":28,"3":27}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":63,"2":28,"3":28}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":65,"2":28,"3":27}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":31,"1":66,"2":28,"3":27}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":65,"2":28,"3":29}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":67,"2":28,"3":27}}} +{"event":"d","node":1,"pkt":{"vc":{"0":31,"1":68,"2":28,"3":27}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":3,"color":"black"},"vc":{"0":31,"1":69,"2":28,"3":27}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":3,"color":"black"},"vc":{"0":32,"1":69,"2":28,"3":27}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":31,"1":67,"2":28,"3":30}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":33,"1":69,"2":28,"3":27}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":34,"1":69,"2":28,"3":27}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":1,"msg":{"type":"pl"},"vc":{"0":31,"1":67,"2":28,"3":31}}} +{"event":"d","node":3,"pkt":{"vc":{"0":31,"1":67,"2":28,"3":32}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"pl"},"vc":{"0":33,"1":69,"2":28,"3":33}}} +{"event":"<","node":1,"pkt":{"snd":3,"rcv":1,"msg":{"type":"pl"},"vc":{"0":31,"1":70,"2":28,"3":31}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":34,"1":69,"2":28,"3":34}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":34,"1":69,"2":28,"3":35}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":34,"1":69,"2":28,"3":36}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":34,"1":69,"2":28,"3":37}}} +{"event":"d","node":3,"pkt":{"vc":{"0":34,"1":69,"2":28,"3":38}}} +{"event":"<","node":0,"pkt":{"snd":3,"rcv":0,"msg":{"type":"pl"},"vc":{"0":35,"1":69,"2":28,"3":37}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":34,"1":69,"2":28,"3":39}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":34,"1":69,"2":29,"3":39}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":69,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":71,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":72,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":73,"2":30,"3":39}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":34,"1":74,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":75,"2":30,"3":39}}} +{"event":"<","node":3,"pkt":{"snd":1,"rcv":3,"msg":{"type":"pl"},"vc":{"0":34,"1":74,"2":30,"3":40}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":34,"1":76,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":77,"2":30,"3":39}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":34,"1":76,"2":31,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":34,"1":78,"2":30,"3":39}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":34,"1":76,"2":32,"3":39}}} +{"event":"d","node":2,"pkt":{"vc":{"0":34,"1":76,"2":33,"3":39}}} +{"event":"d","node":1,"pkt":{"vc":{"0":34,"1":79,"2":30,"3":39}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":2,"color":"black"},"vc":{"0":34,"1":80,"2":30,"3":39}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":34,"1":81,"2":32,"3":39}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":2,"color":"black"},"vc":{"0":36,"1":80,"2":30,"3":39}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":37,"1":80,"2":30,"3":39}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":37,"1":80,"2":30,"3":41}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":30,"3":42}}} +{"event":"d","node":3,"pkt":{"vc":{"0":37,"1":80,"2":30,"3":43}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":34,"3":42}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":37,"1":80,"2":30,"3":44}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":35,"3":42}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":34,"1":82,"2":32,"3":39}}} +{"event":"d","node":1,"pkt":{"vc":{"0":34,"1":83,"2":32,"3":39}}} +{"event":"<","node":0,"pkt":{"snd":2,"rcv":0,"msg":{"type":"pl"},"vc":{"0":38,"1":80,"2":35,"3":42}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":37,"1":80,"2":36,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":37,"1":80,"2":37,"3":44}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":38,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":37,"1":80,"2":39,"3":44}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":37,"1":84,"2":38,"3":44}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":40,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":37,"1":80,"2":41,"3":44}}} +{"event":"<","node":3,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":37,"1":80,"2":40,"3":45}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"pl"},"vc":{"0":39,"1":82,"2":35,"3":42}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":40,"1":82,"2":35,"3":42}}} +{"event":"d","node":0,"pkt":{"vc":{"0":41,"1":82,"2":35,"3":42}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"pl"},"vc":{"0":40,"1":85,"2":38,"3":44}}} +{"event":"d","node":2,"pkt":{"vc":{"0":37,"1":80,"2":42,"3":44}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":37,"1":80,"2":43,"3":44}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":40,"1":86,"2":38,"3":44}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":40,"1":87,"2":43,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":40,"1":86,"2":44,"3":44}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":40,"1":88,"2":43,"3":44}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":40,"1":89,"2":43,"3":44}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-5,"color":"black"},"vc":{"0":40,"1":90,"2":43,"3":44}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":40,"1":91,"2":43,"3":44}}} +{"event":"d","node":1,"pkt":{"vc":{"0":40,"1":92,"2":43,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":40,"1":91,"2":45,"3":44}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":4,"color":"black"},"vc":{"0":40,"1":93,"2":43,"3":44}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":4,"color":"black"},"vc":{"0":42,"1":93,"2":43,"3":44}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":43,"1":93,"2":43,"3":44}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":43,"1":93,"2":43,"3":46}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"pl"},"vc":{"0":43,"1":93,"2":43,"3":47}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":43,"1":93,"2":43,"3":48}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":40,"1":91,"2":46,"3":44}}} +{"event":"d","node":3,"pkt":{"vc":{"0":43,"1":93,"2":43,"3":49}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"pl"},"vc":{"0":43,"1":93,"2":47,"3":47}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"pl"},"vc":{"0":40,"1":94,"2":46,"3":44}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":43,"1":93,"2":43,"3":50}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":40,"1":95,"2":46,"3":44}}} +{"event":"d","node":1,"pkt":{"vc":{"0":40,"1":96,"2":46,"3":44}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":43,"1":93,"2":48,"3":50}}} +{"event":"<","node":2,"pkt":{"snd":1,"rcv":2,"msg":{"type":"pl"},"vc":{"0":43,"1":95,"2":49,"3":50}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-6,"color":"black"},"vc":{"0":43,"1":95,"2":50,"3":50}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":43,"1":95,"2":51,"3":50}}} +{"event":"d","node":2,"pkt":{"vc":{"0":43,"1":95,"2":52,"3":50}}} +{"event":"<","node":3,"pkt":{"snd":2,"rcv":3,"msg":{"type":"pl"},"vc":{"0":43,"1":95,"2":51,"3":51}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":43,"1":95,"2":53,"3":50}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":43,"1":97,"2":53,"3":50}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":2,"color":"black"},"vc":{"0":43,"1":98,"2":53,"3":50}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":2,"color":"black"},"vc":{"0":44,"1":98,"2":53,"3":50}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":45,"1":98,"2":53,"3":50}}} +{"event":"d","node":3,"pkt":{"vc":{"0":43,"1":95,"2":51,"3":52}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":45,"1":98,"2":53,"3":53}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":45,"1":98,"2":53,"3":54}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-7,"color":"black"},"vc":{"0":45,"1":98,"2":54,"3":54}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-8,"color":"black"},"vc":{"0":45,"1":98,"2":55,"3":54}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-8,"color":"black"},"vc":{"0":45,"1":99,"2":55,"3":54}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":45,"1":100,"2":55,"3":54}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"black"},"vc":{"0":46,"1":100,"2":55,"3":54}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":47,"1":100,"2":55,"3":54}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"tok","q":0,"color":"white"},"vc":{"0":47,"1":100,"2":55,"3":55}}} +{"event":">","node":3,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-7,"color":"white"},"vc":{"0":47,"1":100,"2":55,"3":56}}} +{"event":"<","node":2,"pkt":{"snd":3,"rcv":2,"msg":{"type":"tok","q":-7,"color":"white"},"vc":{"0":47,"1":100,"2":56,"3":56}}} +{"event":">","node":2,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-8,"color":"white"},"vc":{"0":47,"1":100,"2":57,"3":56}}} +{"event":"<","node":1,"pkt":{"snd":2,"rcv":1,"msg":{"type":"tok","q":-8,"color":"white"},"vc":{"0":47,"1":101,"2":57,"3":56}}} +{"event":">","node":1,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":47,"1":102,"2":57,"3":56}}} +{"event":"<","node":0,"pkt":{"snd":1,"rcv":0,"msg":{"type":"tok","q":1,"color":"white"},"vc":{"0":48,"1":102,"2":57,"3":56}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"trm"},"vc":{"0":49,"1":102,"2":57,"3":56}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":1,"msg":{"type":"trm"},"vc":{"0":50,"1":102,"2":57,"3":56}}} +{"event":"<","node":1,"pkt":{"snd":0,"rcv":1,"msg":{"type":"trm"},"vc":{"0":50,"1":103,"2":57,"3":56}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":2,"msg":{"type":"trm"},"vc":{"0":51,"1":102,"2":57,"3":56}}} +{"event":"<","node":2,"pkt":{"snd":0,"rcv":2,"msg":{"type":"trm"},"vc":{"0":51,"1":102,"2":58,"3":56}}} +{"event":">","node":0,"pkt":{"snd":0,"rcv":3,"msg":{"type":"trm"},"vc":{"0":52,"1":102,"2":57,"3":56}}} +{"event":"<","node":0,"pkt":{"snd":0,"rcv":0,"msg":{"type":"trm"},"vc":{"0":53,"1":102,"2":57,"3":56}}} +{"event":"<","node":3,"pkt":{"snd":0,"rcv":3,"msg":{"type":"trm"},"vc":{"0":52,"1":102,"2":57,"3":57}}} diff --git a/tests/VectorClocksTests.tla b/tests/VectorClocksTests.tla new file mode 100644 index 0000000..7375a97 --- /dev/null +++ b/tests/VectorClocksTests.tla @@ -0,0 +1,19 @@ +------------------------- MODULE VectorClocksTests ------------------------- +EXTENDS VectorClocks, Sequences, Naturals, TLC, TLCExt, Json + +ASSUME LET T == INSTANCE TLC IN T!PrintT("VectorClocksTests") + +Log == + ndJsonDeserialize("tests/VectorClocksTests.ndjson") + +VectorClock(l) == + l.pkt.vc + +Node(l) == + ToString(l.node) + +ASSUME IsCausallyOrdered(Log, VectorClock) + +ASSUME IsCausallyOrdered(SortCausally(Log, VectorClock, Node), VectorClock) + +=============================================================================