Add Graphs!ConnectedIn(G)

#70

[Feature]

Author: muenchnerkindl

README.md

@@ -13,7 +13,7 @@ The Modules
 | :--: | ---- | ---- | ---- |
 | <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/Functions.tla">Functions.tla</a> | Notions about functions including injection, surjection, and bijection. |[&#10004;](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Functions.java) | [@muenchnerkindl](https://github.com/muenchnerkindl), [@quicquid](https://github.com/quicquid),[@lemmy](https://github.com/lemmy) | 
 | <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/Folds.tla">Folds.tla</a> | Basic Fold operator. | | [@quicquid](https://github.com/quicquid), [@muenchnerkindl](https://github.com/muenchnerkindl) | 
-| <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla">Graphs.tla</a> | Common operators on directed and undirected graphs. | | Leslie Lamport | 
+| <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla">Graphs.tla</a> | Common operators on directed and undirected graphs. | | Leslie Lamport, [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl) | 
 | <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla">SequencesExt.tla</a> | Various operators to manipulate sequences. | [&#10004;](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SequencesExt.java)| [@muenchnerkindl](https://github.com/muenchnerkindl),[@lemmy](https://github.com/lemmy), [@hwayne](https://github.com/hwayne), [@quicquid](https://github.com/quicquid) | 
 | <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla">Relation.tla</a> | Basic operations on relations, represented as binary Boolean functions over some set S.| | [@muenchnerkindl](https://github.com/muenchnerkindl) | 
 | <a href="https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt.tla">FiniteSetsExt.tla</a> | An Operator to do folds without having to use RECURSIVE. | &#10004;| [@hwayne](https://github.com/hwayne),[@lemmy](https://github.com/lemmy), [@quicquid](https://github.com/quicquid) | 

modules/Graphs.tla

@@ -38,6 +38,24 @@ SimplePath(G) ==
 AreConnectedIn(m, n, G) == 
   \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n)
 
+ConnectionsIn(G) ==
+  \* Compute a Boolean matrix that indicates, for each pair of nodes,
+  \* if there exists a path that links the two nodes. The computation,
+  \* based on Warshall's algorithm, is much more efficient than the
+  \* definition used in AreConnectedIn, and the result can be cached
+  \* by TLC, avoiding recomputation.
+  LET C[N \in SUBSET G.node] ==
+      \* Matrix representing the existence of paths whose inner nodes
+      \* (i.e., except for the source and the target) are all in the
+      \* set of nodes N.
+      IF N = {}
+      THEN [m,n \in G.node |-> m = n \/ <<m,n>> \in G.edge]
+      ELSE LET u == CHOOSE u \in N : TRUE
+               Cu == C[N \ {u}]
+           IN  [m,n \in G.node |-> \/ Cu[m,n]
+                                   \/ Cu[m,u] /\ Cu[u,n]]
+  IN  C[G.node]
+
 IsStronglyConnected(G) == 
   \A m, n \in G.node : AreConnectedIn(m, n, G) 
 -----------------------------------------------------------------------------
@@ -48,5 +66,6 @@ IsTreeWithRoot(G, r) ==
   /\ \A n \in G.node : AreConnectedIn(n, r, G)
 =============================================================================
 \* Modification History
+\* Last modified Sun Mar 06 18:10:34 CET 2022 by Stephan Merz
 \* Last modified Tue Dec 21 15:55:45 PST 2021 by Markus Kuppe
 \* Created Tue Jun 18 11:44:08 PST 2002 by Leslie Lamport

tests/GraphsTests.tla

@@ -14,7 +14,14 @@ Graphs(nodes) ==
 ASSUME \A g \in Graphs({"A", "B", "C"}):
     \A u,v \in g.node :
         AreConnectedIn(u, v, g) \in BOOLEAN 
+
+ASSUME LET G ==  [node |-> {1,2,3,4,5,6}, 
+                  edge |-> {<<1,2>>, <<2,3>>, <<2,4>>, <<3,2>>, <<3,4>>, <<3,5>>, 
+                            <<4,2>>, <<5,6>>, <<6,5>>}]
+       IN  \A m,n \in G.node : AreConnectedIn(m,n,G) <=> ConnectionsIn(G)[m,n]
+
 =====================================================================
 \* Modification History
+\* Last modified Sun Mar 06 18:15:49 CET 2022 by Stephan Merz
 \* Last modified Tue Dec 21 15:55:45 PST 2021 by Markus Kuppe
 \* Created Mon Dec 20 20:55:45 PST 2021 by Markus Kuppe