From c60e5a7e945e04576b6b4a625d97b9aab63e8aa4 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <github.com@lemmster.de>
Date: Tue, 21 Feb 2023 21:25:44 -0800
Subject: [PATCH] Streamline operator names.

---
 modules/VectorClocks.tla                 |  8 ++++----
 modules/tlc2/overrides/VectorClocks.java |  4 ++--
 tests/VectorClocksTests.tla              | 22 +++++++++++-----------
 3 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/modules/VectorClocks.tla b/modules/VectorClocks.tla
index 2ee9ced..76c299b 100644
--- a/modules/VectorClocks.tla
+++ b/modules/VectorClocks.tla
@@ -11,7 +11,7 @@ LOCAL happenedBefore(v1, v2) ==
     /\ \A i \in DOMAIN v1: v1[i] <= v2[i]
     /\ \E i \in DOMAIN v1: v1[i]  < v2[i]
 
-IsCausallyOrdered(log, clock(_)) ==
+IsCausalOrder(log, clock(_)) ==
     \A i \in 1..Len(log) :
         \A j \in 1..(i - 1) :
             \* Align the vector clocks to the same domain (mapping
@@ -24,7 +24,7 @@ IsCausallyOrdered(log, clock(_)) ==
                 vcj == Fill(clock(log[j]), D)
             IN happenedBefore(vcj, vci) \/ concurrent(vcj, vci)
 
-SortCausally(log, clock(_), node(_), domain(_)) ==
+CausalOrder(log, clock(_), node(_), domain(_)) ==
     (*
         Sort the provided log by the vector clock values indicated on each line
         of the log. This operator cannot accommodate "hidden" events, meaning
@@ -49,7 +49,7 @@ SortCausally(log, clock(_), node(_), domain(_)) ==
 			 ...
 		    ]
 		 
-		 SortCausally(log, 
+		 CausalOrder(log, 
 					 	LAMBDA line: line.pkt.vc,
 					 	LAMBDA line: line.node,
 						LAMBDA vc : DOMAIN vc)
@@ -58,6 +58,6 @@ SortCausally(log, clock(_), node(_), domain(_)) ==
         { f \in 
             [ 1..Len(log) -> Range(log)] : 
                 Range(f) = Range(log) } : 
-                    IsCausallyOrdered(newlog, clock)
+                    IsCausalOrder(newlog, clock)
 
 ===============================================================================
\ No newline at end of file
diff --git a/modules/tlc2/overrides/VectorClocks.java b/modules/tlc2/overrides/VectorClocks.java
index 6f67a61..97d573d 100644
--- a/modules/tlc2/overrides/VectorClocks.java
+++ b/modules/tlc2/overrides/VectorClocks.java
@@ -95,8 +95,8 @@ public Value delete() {
 	 * 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,
+	@TLAPlusOperator(identifier = "CausalOrder", module = "VectorClocks", warn = false)
+	public static Value causalOrder(final TupleValue v, final Applicable opClock, final Applicable opNode,
 			final Applicable opDomain) {
 
 		// A1) Sort each node's individual log which can be totally ordered.
diff --git a/tests/VectorClocksTests.tla b/tests/VectorClocksTests.tla
index 923cb7c..e9fc842 100644
--- a/tests/VectorClocksTests.tla
+++ b/tests/VectorClocksTests.tla
@@ -3,17 +3,17 @@ EXTENDS VectorClocks, Sequences, Naturals, TLC, Json
 
 ASSUME LET T == INSTANCE TLC IN T!PrintT("VectorClocksTests")
 
-ASSUME IsCausallyOrdered(<< >>, LAMBDA l: l)
-ASSUME IsCausallyOrdered(<< <<0,0>> >>, LAMBDA l: l)
-ASSUME IsCausallyOrdered(<< <<0,0>>, <<0,1>> >>, LAMBDA l: l) \* happened before
-ASSUME IsCausallyOrdered(<< <<1,0>>, <<0,1>> >>, LAMBDA l: l) \* concurrent
+ASSUME IsCausalOrder(<< >>, LAMBDA l: l)
+ASSUME IsCausalOrder(<< <<0,0>> >>, LAMBDA l: l)
+ASSUME IsCausalOrder(<< <<0,0>>, <<0,1>> >>, LAMBDA l: l) \* happened before
+ASSUME IsCausalOrder(<< <<1,0>>, <<0,1>> >>, LAMBDA l: l) \* concurrent
 
-ASSUME IsCausallyOrdered(<< <<0>>, <<0,1>> >>, LAMBDA l: l) \* happened before
-ASSUME IsCausallyOrdered(<< <<1>>, <<0,1>> >>, LAMBDA l: l) \* concurrent
+ASSUME IsCausalOrder(<< <<0>>, <<0,1>> >>, LAMBDA l: l) \* happened before
+ASSUME IsCausalOrder(<< <<1>>, <<0,1>> >>, LAMBDA l: l) \* concurrent
 
-ASSUME ~IsCausallyOrdered(<< <<0,1>>, <<0,0>> >>, LAMBDA l: l)
+ASSUME ~IsCausalOrder(<< <<0,1>>, <<0,0>> >>, LAMBDA l: l)
 
-ASSUME ~IsCausallyOrdered(<< <<1>>, <<0,0>> >>, LAMBDA l: l) \* concurrent
+ASSUME ~IsCausalOrder(<< <<1>>, <<0,0>> >>, LAMBDA l: l) \* concurrent
 
 Log ==
     ndJsonDeserialize("tests/VectorClocksTests.ndjson")
@@ -28,10 +28,10 @@ Node(l) ==
      \* into a function with domain {0, 1}.
     ToString(l.node)
 
-ASSUME ~IsCausallyOrdered(Log, VectorClock)
+ASSUME ~IsCausalOrder(Log, VectorClock)
 
-ASSUME IsCausallyOrdered(
-			SortCausally(Log, 
+ASSUME IsCausalOrder(
+			CausalOrder(Log, 
 						 VectorClock, 
 						 Node,
 						 LAMBDA vc: DOMAIN vc),