From a845f264d437969d5558dd5d3e826b464efa4b40 Mon Sep 17 00:00:00 2001
From: Stephan Merz <stephan.merz@loria.fr>
Date: Mon, 26 Feb 2024 15:29:39 +0100
Subject: [PATCH] adding UndirectedGraphs module and tests

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
---
 modules/UndirectedGraphs.tla    | 59 +++++++++++++++++++++++++++++++++
 tests/UndirectedGraphsTests.tla | 24 ++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 modules/UndirectedGraphs.tla
 create mode 100644 tests/UndirectedGraphsTests.tla

diff --git a/modules/UndirectedGraphs.tla b/modules/UndirectedGraphs.tla
new file mode 100644
index 0000000..95c3e54
--- /dev/null
+++ b/modules/UndirectedGraphs.tla
@@ -0,0 +1,59 @@
+------------------------- MODULE UndirectedGraphs ----------------------------
+(****************************************************************************)
+(* Representation of undirected graphs in TLA+. In contrast to module       *)
+(* Graphs, edges are represented as unordered pairs {a,b} of nodes, thus    *)
+(* enforcing symmetry.                                                      *)
+(****************************************************************************)
+LOCAL INSTANCE Naturals
+LOCAL INSTANCE Sequences
+LOCAL INSTANCE SequencesExt
+LOCAL INSTANCE FiniteSets
+LOCAL INSTANCE Folds
+
+IsUndirectedGraph(G) ==
+   /\ G = [node |-> G.node, edge |-> G.edge]
+   /\ \A e \in G.edge : \E a,b \in G.node : e = {a,b}
+
+IsLoopFreeUndirectedGraph(G) ==
+   /\ G = [node |-> G.node, edge |-> G.edge]
+   /\ \A e \in G.edge : \E a,b \in G.node : a # b /\ e = {a,b}
+
+UndirectedSubgraph(G) ==
+   {H \in [node : SUBSET G.node, edge : SUBSET G.edge] : IsUndirectedGraph(H)}
+
+-----------------------------------------------------------------------------
+Path(G) == {p \in Seq(G.node) :
+             /\ p # << >>
+             /\ \A i \in 1..(Len(p)-1) : {p[i], p[i+1]} \in G.edge}
+
+SimplePath(G) ==
+    \* A simple path is a path with no repeated nodes.
+    {p \in SeqOf(G.node, Cardinality(G.node)) :
+             /\ p # << >>
+             /\ Cardinality({ p[i] : i \in DOMAIN p }) = Len(p)
+             /\ \A i \in 1..(Len(p)-1) : {p[i], p[i+1]} \in G.edge}
+
+(****************************************************************************)
+(* Compute the connected components of an undirected graph: initially each  *)
+(* node is in a component by itself, then iterate over the edges to merge   *)
+(* the components related by the edge.                                      *)
+(****************************************************************************)
+ConnectedComponents(G) ==
+   LET base == {{n} : n \in G.node}
+       choice(E) == CHOOSE e \in E : TRUE
+       firstNode(e) == CHOOSE a \in G.node : \E b \in G.node : e = {a,b}
+       secondNode(e) == CHOOSE b \in G.node : e = {firstNode(e), b}
+       nodesOfEdge(e) == <<firstNode(e), secondNode(e)>>
+       merge(e, comps) ==
+          LET compA == CHOOSE c \in comps : e[1] \in c
+              compB == CHOOSE c \in comps : e[2] \in c
+          IN  IF compA = compB THEN comps
+              ELSE (comps \ {compA, compB}) \union {compA \union compB}
+   IN MapThenFoldSet(merge, base, nodesOfEdge, choice, G.edge)
+
+AreConnectedIn(m, n, G) ==
+   \E comp \in ConnectedComponents(G) : m \in comp /\ n \in comp
+
+IsStronglyConnected(G) == 
+  Cardinality(ConnectedComponents(G)) = 1
+=============================================================================
diff --git a/tests/UndirectedGraphsTests.tla b/tests/UndirectedGraphsTests.tla
new file mode 100644
index 0000000..9773875
--- /dev/null
+++ b/tests/UndirectedGraphsTests.tla
@@ -0,0 +1,24 @@
+------------------------- MODULE GraphsTests -------------------------
+EXTENDS UndirectedGraphs, TLCExt
+
+ASSUME LET T == INSTANCE TLC IN T!PrintT("UndirectedGraphsTests")
+
+ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {}]), {})
+ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {1,2,3}]), {<<1>>, <<2>>, <<3>>})
+ASSUME AssertEq(SimplePath([edge|-> {{1,2}}, node |-> {1,2,3}]), 
+            { <<1>>, <<2>>, <<3>>, <<1,2>>, <<2,1>>} )
+
+ASSUME AssertEq(ConnectedComponents([edge|-> {}, node |-> {}]), {})
+ASSUME LET G == [edge|-> {{1,2}}, node |-> {1,2,3}]
+       IN  /\ AssertEq(ConnectedComponents(G), {{1,2}, {3}})
+           /\ AreConnectedIn(1, 2, G)
+           /\ ~ AreConnectedIn(1, 3, G)
+
+AssertEq(ConnectedComponents([edge|-> {{1,2}}, node |-> {1,2,3}]), 
+                {{1,2}, {3}})
+ASSUME LET G == [node |-> {1,2,3,4,5},
+                 edge |-> {{1,3}, {1,4}, {2,3}, {2,4}, {3,5}, {4,5}}]
+       IN  /\ AssertEq(ConnectedComponents(G), {{1,2,3,4,5}})
+           /\ IsStronglyConnected(G)
+
+=====================================================================