diff --git a/README.md b/README.md index f59ccfa..71063b1 100644 --- a/README.md +++ b/README.md @@ -20,19 +20,23 @@ The Modules | [`FiniteSetsExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt.tla) | Additional operators on finite sets (e.g. `FoldSet`, `Min`, `Max`, `Quantify`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/FiniteSetsExt.java) | [@hwayne](https://github.com/hwayne), [@lemmy](https://github.com/lemmy), [@quicquid](https://github.com/quicquid), [@mryndzionek](https://github.com/mryndzionek), [@will62794](https://github.com/will62794), [@konnov](https://github.com/konnov) | | [`Folds.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Folds.tla) | Basic Fold operator (`MapThenFoldSet`). | | [@quicquid](https://github.com/quicquid), [@muenchnerkindl](https://github.com/muenchnerkindl), [@konnov](https://github.com/konnov) | | [`Functions.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Functions.tla) | Notions about functions (range, anti-function, injection, surjection, bijection) and folds (`FoldFunction`, `FoldFunctionOnSet`). | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Functions.java) | Thomas L. Rodeheffer, [@muenchnerkindl](https://github.com/muenchnerkindl), [@quicquid](https://github.com/quicquid), [@lemmy](https://github.com/lemmy) | -| [`Graphs.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla) | Common operators on directed and undirected graphs | | Leslie Lamport, [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl) | +| [`Graphs.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Graphs.tla) | Common operators on (directed) graphs | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Graphs.java) | Leslie Lamport, [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl) | | [`GraphViz.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/GraphViz.tla) | Generate GraphViz file through TLC | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/GraphViz.java) | [@lemmy](https://github.com/lemmy) | | [`HTML.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/HTML.tla) | Format strings into HTML tags | | [@afonsof](https://github.com/afonsof) | | [`IOUtils.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/IOUtils.tla) | Input/Output of TLA+ values & Spawn system commands from a spec. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/IOUtils.java) | [@lemmy](https://github.com/lemmy), [@lvanengelen](https://github.com/lvanengelen), [@afonsof](https://github.com/afonsof) | | [`Json.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Json.tla) | JSON serialization and deserialization into TLA+ values. | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Json.java) | [@kuujo](https://github.com/kuujo), [@lemmy](https://github.com/lemmy), [@jobvs](https://github.com/jobvs), [@pfeodrippe](https://github.com/pfeodrippe) | +| [`Quorum.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Quorum.tla) | Definition of quorum systems commonly used in fault-tolerant distributed algorithms. | | [@muenchnerkindl](https://github.com/muenchnerkindl) | | [`Relation.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Relation.tla) | Basic operations on relations, represented as binary Boolean functions over some set S. | | [@muenchnerkindl](https://github.com/muenchnerkindl), [@lemmy](https://github.com/lemmy) | | [`SequencesExt.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/SequencesExt.tla) | Additional operators on sequences (e.g. `ToSet`, `Reverse`, `ReplaceAll`, `SelectInSeq`, etc.) | [✔](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), [@konnov](https://github.com/konnov), [@afonsof](https://github.com/afonsof) | | [`ShiViz.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/ShiViz.tla) | Visualize error-traces of multi-process PlusCal algorithms with an [Interactive Communication Graphs](https://bestchai.bitbucket.io/shiviz/). | | [@lemmy](https://github.com/lemmy) | | [`Statistics.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/Statistics.tla) | Statistics operators (`ChiSquare`, etc.) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/Statistics.java) | [@lemmy](https://github.com/lemmy) | | [`SVG.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/SVG.tla) | see [will62794/tlaplus_animation](https://github.com/will62794/tlaplus_animation) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/SVG.java) | [@will62794](https://github.com/will62794), [@lemmy](https://github.com/lemmy) | | [`TLCExt.tla`](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLCExt.tla) | Assertion operators and experimental TLC features (now part of TLC). | [✔](https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java) | [@lemmy](https://github.com/lemmy), [@will62794](https://github.com/will62794) | +| [`UndirectedGraphs.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/UndirectedGraphs.tla) | Common operators on undirected graphs | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/UndirectedGraphs.java) | [@lemmy](https://github.com/lemmy), [@muenchnerkindl](https://github.com/muenchnerkindl) | | [`VectorClocks.tla`](https://github.com/tlaplus/CommunityModules/blob/master/modules/VectorClocks.tla) | Causal order operations on vector clocks (e.g. `CausalOrder`, `IsCausalOrder`) | [✔](https://github.com/tlaplus/CommunityModules/blob/master/modules/tlc2/overrides/VectorClocks.java) | [@lemmy](https://github.com/lemmy) | +Some of these modules are accompanied by collections of theorems about the operators they define. For module `M.tla` the corresponding theorems +appear in module `MTheorems.tla`, and proofs of these theorems can be found in `MTheorems_proofs.tla`. How to use it ------------- diff --git a/modules/FiniteSetsExtTheorems.tla b/modules/FiniteSetsExtTheorems.tla index 7c07b29..6f22eb6 100644 --- a/modules/FiniteSetsExtTheorems.tla +++ b/modules/FiniteSetsExtTheorems.tla @@ -357,5 +357,23 @@ THEOREM MinNat == PROVE /\ Min(S) \in S /\ \A y \in S : Min(S) <= y +--------------------------------------------------------------------------- + +(*************************************************************************) +(* Theorems about majorities. A "majority" of a finite set U is any *) +(* subset whose cardinality is more than half that of U. This *) +(* generalizes the notion of a quorum used in distributed-consensus *) +(* specifications, where U is the set of servers. *) +(*************************************************************************) + +(*************************************************************************) +(* Any superset (within U) of a majority of U is itself a majority. *) +(*************************************************************************) +THEOREM SupersetOfMajorityIsMajority == + ASSUME NEW U, IsFiniteSet(U), + NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2, + 2 * Cardinality(Q1) > Cardinality(U) + PROVE 2 * Cardinality(Q2) > Cardinality(U) + =========================================================================== diff --git a/modules/FiniteSetsExtTheorems_proofs.tla b/modules/FiniteSetsExtTheorems_proofs.tla index 511d9c5..29a3b28 100644 --- a/modules/FiniteSetsExtTheorems_proofs.tla +++ b/modules/FiniteSetsExtTheorems_proofs.tla @@ -621,4 +621,20 @@ THEOREM MinNat == /\ \A y \in S : Min(S) <= y BY MinIntBounded, \A y \in S : 0 <= y +--------------------------------------------------------------------------- + +(*************************************************************************) +(* Any superset (within U) of a majority of U is itself a majority. *) +(*************************************************************************) +THEOREM SupersetOfMajorityIsMajority == + ASSUME NEW U, IsFiniteSet(U), + NEW Q1 \in SUBSET U, NEW Q2 \in SUBSET U, Q1 \subseteq Q2, + 2 * Cardinality(Q1) > Cardinality(U) + PROVE 2 * Cardinality(Q2) > Cardinality(U) +<1>1. IsFiniteSet(Q2) /\ Cardinality(Q2) <= Cardinality(U) BY FS_Subset +<1>2. IsFiniteSet(Q1) /\ Cardinality(Q1) <= Cardinality(Q2) BY <1>1, FS_Subset +<1>3. Cardinality(Q1) \in Nat /\ Cardinality(Q2) \in Nat /\ Cardinality(U) \in Nat + BY FS_CardinalityType, <1>1, <1>2 +<1>. QED BY <1>2, <1>3 + ================================================================================ diff --git a/modules/GraphTheorems.tla b/modules/GraphTheorems.tla new file mode 100644 index 0000000..2aa8840 --- /dev/null +++ b/modules/GraphTheorems.tla @@ -0,0 +1,209 @@ +------------------------------ MODULE GraphTheorems -------------------------- +EXTENDS Graphs, Sequences + +(****************************************************************************) +(* Lemmas about transposed graphs. *) +(****************************************************************************) +THEOREM TransposeIsDirectedGraph == + ASSUME NEW G, IsDirectedGraph(G) + PROVE IsDirectedGraph(Transpose(G)) + +\* Note that the reverse implication does not hold in general. +\* Consider G = [node |-> {1}, edge |-> {<<1,1,1>>}, root |-> {1}] +\* Then Transpose(G) = [node |-> {1}, edge |-> {<<1,1>>}], +\* which is a directed graph whereas G is not. + +THEOREM TransposeTranspose == + ASSUME NEW G, IsDirectedGraph(G) + PROVE Transpose(Transpose(G)) = G + +THEOREM PathTranspose == + ASSUME NEW G, NEW p \in Path(G) + PROVE Reverse(p) \in Path(Transpose(G)) + +THEOREM TransposePath == + ASSUME NEW G, IsDirectedGraph(G), NEW p \in Path(Transpose(G)) + PROVE Reverse(p) \in Path(G) + +THEOREM SimplePathTranspose == + ASSUME NEW G, NEW p \in SimplePath(G) + PROVE Reverse(p) \in SimplePath(Transpose(G)) + +THEOREM TransposeSimplePath == + ASSUME NEW G, IsDirectedGraph(G), NEW p \in SimplePath(Transpose(G)) + PROVE Reverse(p) \in SimplePath(G) + +THEOREM AreConnectedInTranspose == + ASSUME NEW G, NEW m, NEW n, AreConnectedIn(m, n, G) + PROVE AreConnectedIn(n, m, Transpose(G)) + +THEOREM TransposeAreConnectedIn == + ASSUME NEW G, NEW m, NEW n, IsDirectedGraph(G), + AreConnectedIn(m, n, Transpose(G)) + PROVE AreConnectedIn(n, m, G) + +THEOREM IsStronglyConnectedTranspose == + ASSUME NEW G, IsStronglyConnected(G) + PROVE IsStronglyConnected(Transpose(G)) + +THEOREM TransposeIsStronglyConnected == + ASSUME NEW G, IsDirectedGraph(G), IsStronglyConnected(Transpose(G)) + PROVE IsStronglyConnected(G) + +(****************************************************************************) +(* The "concatenation" of two paths that share an endpoint is a path. *) +(****************************************************************************) +THEOREM PathConcatenation == + ASSUME NEW G, NEW p \in Path(G), NEW q \in Path(G), + p[Len(p)] = q[1] + PROVE p \o Tail(q) \in Path(G) + +(****************************************************************************) +(* Any non-empty subsequence of a path is a path. *) +(****************************************************************************) +THEOREM SubPath == + ASSUME NEW G, NEW p \in Path(G), + NEW i \in 1 .. Len(p), NEW j \in i .. Len(p) + PROVE SubSeq(p, i, j) \in Path(G) + +(****************************************************************************) +(* Two nodes are connected by a path if and only if they are connected by *) +(* a simple path. *) +(****************************************************************************) +THEOREM ExistsPathIffExistsSimplePath == + ASSUME NEW G, NEW m \in G.node, NEW n \in G.node + PROVE (\E p \in Path(G) : p[1] = m /\ p[Len(p)] = n) + <=> (\E p \in SimplePath(G) : p[1] = m /\ p[Len(p)] = n) + +(****************************************************************************) +(* Connectedness is a pre-order. *) +(****************************************************************************) +THEOREM ConnectedReflexive == + ASSUME NEW G, NEW a \in G.node + PROVE AreConnectedIn(a, a, G) + +THEOREM ConnectedTransitive == + ASSUME NEW G, NEW a \in G.node, NEW b \in G.node, NEW c \in G.node, + AreConnectedIn(a, b, G), AreConnectedIn(b, c, G) + PROVE AreConnectedIn(a, c, G) + +(****************************************************************************) +(* A tree does not contain a cycle. One way to express this is that no *) +(* non-empty set of nodes is closed under successors. *) +(****************************************************************************) +THEOREM TreeAcyclic == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW S \in SUBSET G.node, S # {} + PROVE \E q \in S : \A e \in G.edge : e[1] = q => e[2] \notin S + +(****************************************************************************) +(* In particular, no node is its own successor in a tree, and all paths in *) +(* a tree are simple paths. *) +(****************************************************************************) +THEOREM TreeIrreflexive == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW n \in G.node + PROVE <> \notin G.edge + +THEOREM TreeSimplePath == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW p \in Path(G) + PROVE p \in SimplePath(G) + +(****************************************************************************) +(* Connectedness is antisymmetric (and thus a partial order) in trees. *) +(****************************************************************************) +THEOREM TreeConnectedAntisymmetric == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW a \in G.node, NEW b \in G.node, + AreConnectedIn(a, b, G), AreConnectedIn(b, a, G) + PROVE a = b + +(****************************************************************************) +(* A graph consisting of only the root and no edges is a tree. *) +(****************************************************************************) +THEOREM SingletonIsTreeWithRoot == + ASSUME NEW r + PROVE IsTreeWithRoot([node |-> {r}, edge |-> {}],r) + +(****************************************************************************) +(* A tree can be extended by attaching a disjoint tree to a node. *) +(****************************************************************************) +THEOREM AttachTree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW n \in G.node, + NEW H, NEW s, IsTreeWithRoot(H,s), G.node \cap H.node = {} + PROVE IsTreeWithRoot([node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}], r) + +(****************************************************************************) +(* In particular, a tree can be extended by a new node that becomes a leaf. *) +(****************************************************************************) +THEOREM AddLeafToTree == + ASSUME NEW G, NEW r, NEW leaf, NEW parent, + IsTreeWithRoot(G,r), leaf \notin G.node, parent \in G.node + PROVE IsTreeWithRoot([node |-> G.node \cup {leaf}, + edge |-> G.edge \cup {<>}], r) + +(****************************************************************************) +(* Removing a subtree from a tree maintains the tree property, provided it *) +(* is not the entire tree (trees must be non-empty.) *) +(****************************************************************************) +THEOREM RemoveSubtree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW nd \in G.node \ {r} + PROVE LET S == { n \in G.node : AreConnectedIn(n, nd, G) } + T == G.node \ S + E == G.edge \cap (T \X T) + IN IsTreeWithRoot([node |-> T, edge |-> E], r) + +(****************************************************************************) +(* In particular, removing a leaf node that is not the root from a tree *) +(* results in a tree. *) +(****************************************************************************) +THEOREM RemoveLeafFromTree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW leaf \in G.node, Predecessors(G, leaf) = {}, + NEW parent \in G.node, <> \in G.edge + PROVE IsTreeWithRoot([node |-> G.node \ {leaf}, + edge |-> G.edge \ {<>}], r) + +(****************************************************************************) +(* The operator IsTreeWithRoot is set up so that edges point towards the *) +(* root of the tree. Sometimes it is more natural to consider trees with *) +(* edges pointing towards the leaves. Such a graph G can be characterized *) +(* by the predicate IsTreeWithRoot(Transpose(G), r). *) +(* We prove lemmas analogous to the above ones about transposed trees. *) +(****************************************************************************) +THEOREM SingletonIsTransposedTreeWithRoot == + ASSUME NEW r + PROVE IsTreeWithRoot(Transpose([node |-> {r}, edge |-> {}]), r) + +THEOREM AttachTransposedTree == + ASSUME NEW G, NEW r, IsDirectedGraph(G), IsTreeWithRoot(Transpose(G), r), + NEW H, NEW s, IsDirectedGraph(H), IsTreeWithRoot(Transpose(H), s), + G.node \cap H.node = {}, NEW n \in G.node + PROVE IsTreeWithRoot(Transpose([node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}]), r) + +THEOREM AddLeafToTransposedTree == + ASSUME NEW G, NEW r, NEW leaf, NEW parent, + IsDirectedGraph(G), IsTreeWithRoot(Transpose(G),r), + leaf \notin G.node, parent \in G.node + PROVE IsTreeWithRoot(Transpose([node |-> G.node \cup {leaf}, + edge |-> G.edge \cup {<>}]), r) + +THEOREM RemoveTransposedSubtree == + ASSUME NEW G, NEW r, IsDirectedGraph(G), IsTreeWithRoot(Transpose(G), r), + NEW nd \in G.node \ {r} + PROVE LET S == {n \in G.node : AreConnectedIn(nd, n, G)} + T == G.node \ S + E == G.edge \cap (T \X T) + IN IsTreeWithRoot(Transpose([node |-> T, edge |-> E]), r) + +THEOREM RemoveLeafFromTransposedTree == + ASSUME NEW G, IsDirectedGraph(G), + NEW r, IsTreeWithRoot(Transpose(G),r), + NEW leaf \in G.node, + Successors(G, leaf) = {}, + NEW parent \in G.node, <> \in G.edge + PROVE IsTreeWithRoot(Transpose([node |-> G.node \ {leaf}, + edge |-> G.edge \ {<>}]), r) + +============================================================================== diff --git a/modules/GraphTheorems_proofs.tla b/modules/GraphTheorems_proofs.tla new file mode 100644 index 0000000..9739c85 --- /dev/null +++ b/modules/GraphTheorems_proofs.tla @@ -0,0 +1,708 @@ +---------------------- MODULE GraphTheorems_proofs -------------------------- +EXTENDS Graphs, Integers, FunctionTheorems, FiniteSetTheorems, + SequencesExtTheorems, + FiniteSetsExt, FiniteSetsExtTheorems, TLAPS + +(****************************************************************************) +(* Lemmas about transposed graphs. *) +(****************************************************************************) +THEOREM TransposeIsDirectedGraph == + ASSUME NEW G, IsDirectedGraph(G) + PROVE IsDirectedGraph(Transpose(G)) +<1>. DEFINE N == G.node + E == G.edge +<1>1. /\ G = [node |-> N, edge |-> E] + /\ E \subseteq N \X N + BY DEF IsDirectedGraph +<1>. HIDE DEF N, E +<1>. QED BY <1>1 DEF IsDirectedGraph, Transpose + +THEOREM TransposeTranspose == + ASSUME NEW G, IsDirectedGraph(G) + PROVE Transpose(Transpose(G)) = G +<1>. DEFINE N == G.node + E == G.edge + TE == { <> : e \in E } + TTE == { <> : e \in TE } +<1>1. /\ G = [node |-> N, edge |-> E] + /\ E \subseteq N \X N + /\ TE \subseteq N \X N + BY DEF IsDirectedGraph +<1>. HIDE DEF N, E +<1>2. Transpose(G) = [node |-> N, edge |-> TE] + BY <1>1 DEF Transpose +<1>3. TTE = E + BY <1>1 +<1>4. Transpose(Transpose(G)) = [node |-> N, edge |-> TTE] + BY <1>2 DEF Transpose +<1>. HIDE DEF TTE +<1>. QED BY <1>1, <1>3, <1>4 + +THEOREM PathTranspose == + ASSUME NEW G, NEW p \in Path(G) + PROVE Reverse(p) \in Path(Transpose(G)) +BY DEF Path, Reverse, Transpose + +THEOREM TransposePath == + ASSUME NEW G, IsDirectedGraph(G), NEW p \in Path(Transpose(G)) + PROVE Reverse(p) \in Path(G) +<1>. DEFINE N == G.node + E == G.edge + TE == { <> : e \in E } +<1>1. /\ G = [node |-> N, edge |-> E] + /\ E \subseteq N \X N + BY DEF IsDirectedGraph +<1>2. Transpose(G) = [node |-> N, edge |-> TE] + BY DEF Transpose +<1>. HIDE DEF N, E +<1>3. /\ p \in Seq(N) \ { <<>> } + /\ \A i \in 1 .. Len(p)-1 : <> \in TE + BY <1>2 DEF Path +<1>. QED BY <1>1, <1>3 DEF Reverse, Path + +THEOREM SimplePathTranspose == + ASSUME NEW G, NEW p \in SimplePath(G) + PROVE Reverse(p) \in SimplePath(Transpose(G)) +<1>1. /\ Reverse(p) \in Path(Transpose(G)) + /\ \A i,j \in 1 .. Len(p) : p[i] = p[j] => i = j + BY PathTranspose DEF SimplePath +<1>2. p \in Seq(G.node) + BY DEF SimplePath, Path +<1>. QED BY <1>1, <1>2 DEF Reverse, SimplePath + +THEOREM TransposeSimplePath == + ASSUME NEW G, IsDirectedGraph(G), NEW p \in SimplePath(Transpose(G)) + PROVE Reverse(p) \in SimplePath(G) +<1>1. /\ Reverse(p) \in Path(G) + /\ \A i,j \in 1 .. Len(p) : p[i] = p[j] => i = j + BY TransposePath DEF SimplePath +<1>2. p \in Seq(G.node) + BY DEF SimplePath, Path, Transpose +<1>. QED BY <1>1, <1>2 DEF Reverse, SimplePath + +THEOREM AreConnectedInTranspose == + ASSUME NEW G, NEW m, NEW n, AreConnectedIn(m, n, G) + PROVE AreConnectedIn(n, m, Transpose(G)) +<1>1. PICK p \in Path(G) : p[1] = m /\ p[Len(p)] = n + BY DEF AreConnectedIn +<1>. p \in Seq(G.node) \ { << >> } + BY DEF Path +<1>2. Reverse(p) \in Path(Transpose(G)) + BY PathTranspose +<1>3. Reverse(p)[1] = n /\ Reverse(p)[Len(Reverse(p))] = m + BY <1>1 DEF Reverse +<1>. QED BY <1>2, <1>3 DEF AreConnectedIn + +THEOREM TransposeAreConnectedIn == + ASSUME NEW G, NEW m, NEW n, IsDirectedGraph(G), AreConnectedIn(m, n, Transpose(G)) + PROVE AreConnectedIn(n, m, G) +<1>1. PICK p \in Path(Transpose(G)) : p[1] = m /\ p[Len(p)] = n + BY DEF AreConnectedIn +<1>. p \in Seq(G.node) \ { << >> } + BY DEF Path, Transpose +<1>2. Reverse(p) \in Path(G) + BY TransposePath +<1>3. Reverse(p)[1] = n /\ Reverse(p)[Len(Reverse(p))] = m + BY <1>1 DEF Reverse +<1>. QED BY <1>2, <1>3 DEF AreConnectedIn + +THEOREM IsStronglyConnectedTranspose == + ASSUME NEW G, IsStronglyConnected(G) + PROVE IsStronglyConnected(Transpose(G)) +<1>. Transpose(G).node = G.node + BY DEF Transpose +<1>. QED BY AreConnectedInTranspose DEF IsStronglyConnected + +THEOREM TransposeIsStronglyConnected == + ASSUME NEW G, IsDirectedGraph(G), IsStronglyConnected(Transpose(G)) + PROVE IsStronglyConnected(G) +<1>. Transpose(G).node = G.node + BY DEF Transpose +<1>. QED BY TransposeAreConnectedIn DEF IsStronglyConnected + +(****************************************************************************) +(* The "concatenation" of two paths that share an endpoint is a path. *) +(****************************************************************************) +THEOREM PathConcatenation == + ASSUME NEW G, NEW p \in Path(G), NEW q \in Path(G), + p[Len(p)] = q[1] + PROVE p \o Tail(q) \in Path(G) +<1>. DEFINE pq == p \o Tail(q) +<1>. p \in Seq(G.node) \ { <<>> } /\ q \in Seq(G.node) \ { <<>> } + BY DEF Path +<1>2. ASSUME NEW i \in 1 .. Len(pq)-1 PROVE <> \in G.edge + <2>1. CASE i \in 1 .. Len(p)-1 + BY <2>1 DEF Path + <2>2. CASE i \in Len(p) .. Len(pq)-1 + BY <2>2, i-Len(p)+1 \in 1 .. Len(q)-1 DEF Path + <2>. QED BY <2>1, <2>2 +<1>. QED BY <1>2 DEF Path + +(****************************************************************************) +(* Any non-empty subsequence of a path is a path. *) +(****************************************************************************) +THEOREM SubPath == + ASSUME NEW G, NEW p \in Path(G), + NEW i \in 1 .. Len(p), NEW j \in i .. Len(p) + PROVE SubSeq(p, i, j) \in Path(G) +<1>. DEFINE s == SubSeq(p, i, j) +<1>. p \in Seq(G.node) + BY DEF Path +<1>1. /\ s \in Seq(G.node) \ { <<>> } + /\ Len(s) = j-i+1 + OBVIOUS +<1>2. ASSUME NEW k \in 1 .. (j-i) PROVE <> \in G.edge + BY i+k-1 \in 1 .. Len(p)-1 DEF Path +<1>. QED BY <1>1, <1>2 DEF Path + +(****************************************************************************) +(* Two nodes are connected by a path if and only if they are connected by *) +(* a simple path. *) +(****************************************************************************) +THEOREM ExistsPathIffExistsSimplePath == + ASSUME NEW G, NEW m \in G.node, NEW n \in G.node + PROVE (\E p \in Path(G) : p[1] = m /\ p[Len(p)] = n) + <=> (\E p \in SimplePath(G) : p[1] = m /\ p[Len(p)] = n) +<1>1. SUFFICES ASSUME NEW p \in Path(G), p[1] = m, p[Len(p)] = n + PROVE \E q \in SimplePath(G) : q[1] = m /\ q[Len(q)] = n + BY DEF SimplePath +<1>. DEFINE Repeats(pp) == {i \in 1 .. Len(pp) : \E j \in 1 .. Len(pp) : j > i /\ pp[i] = pp[j]} + CR(pp) == Cardinality(Repeats(pp)) + P(pp,k) == pp[1] = m /\ pp[Len(pp)] = n /\ CR(pp) = k + => \E q \in SimplePath(G) : q[1] = m /\ q[Len(q)] = n +<1>2. ASSUME NEW pp \in Path(G) + PROVE IsFiniteSet(Repeats(pp)) + BY FS_Subset, FS_Interval DEF Path +<1>3. \E k \in Nat : CR(p) = k + BY <1>2, FS_CardinalityType, Zenon +<1>4. \A k \in Nat : \A pp \in Path(G) : P(pp,k) + <2>. SUFFICES \A k \in Nat : (\A l \in 0 .. k-1 : \A pp \in Path(G) : P(pp,l)) + => \A pp \in Path(G) : P(pp,k) + <3>. HIDE DEF P + <3>. QED BY GeneralNatInduction, IsaM("iprover") + <2>1. SUFFICES ASSUME NEW k \in Nat, + \A l \in 0 .. k-1 : \A pp \in Path(G) : P(pp,l), + NEW pp \in Path(G), pp[1] = m, pp[Len(pp)] = n, CR(pp) = k + PROVE \E q \in SimplePath(G) : q[1] = m /\ q[Len(q)] = n + BY Zenon + <2>. pp \in Seq(G.node) + BY DEF Path + <2>2. CASE k = 0 + <3>. Repeats(pp) = {} + BY <1>2, <2>1, <2>2, FS_EmptySet, Zenon + <3>. QED BY <2>1 DEF SimplePath + <2>3. CASE k # 0 + <3>1. PICK i \in 1 .. Len(pp) : \E j \in 1 .. Len(pp) : j > i /\ pp[i] = pp[j] + BY <1>2, <2>1, <2>3, FS_EmptySet + <3>2. PICK j \in 1 .. Len(pp) : /\ j > i /\ pp[i] = pp[j] + /\ ~(\E jj \in 1 .. Len(pp) : jj > j /\ pp[i] = pp[jj]) + <4>. DEFINE J == {jj \in 1 .. Len(pp) : jj > i /\ pp[i] = pp[jj]} + <4>1. /\ J \in SUBSET Int + /\ J # {} + /\ Len(pp) \in Int + /\ \A jj \in J : Len(pp) >= jj + BY <3>1 + <4>2. /\ Max(J) \in J + /\ \A jj \in J : Max(J) >= jj + BY <4>1, MaxIntBounded + <4>. QED BY <4>2 + <3>. DEFINE pref == SubSeq(pp, 1, i) + suff == SubSeq(pp, j+1, Len(pp)) + qq == pref \o suff + <3>3. qq \in Path(G) + <4>1. qq \in Seq(G.node) + OBVIOUS + <4>2. qq # << >> + BY <3>2 DEF Path + <4>3. ASSUME NEW ii \in 1 .. Len(qq)-1 + PROVE <> \in G.edge + <5>1. CASE ii \in 1 .. i-1 + BY <5>1 DEF Path + <5>2. CASE ii = i + BY <3>2, <5>2 DEF Path + <5>3. CASE ii > i + <6>1. /\ qq[ii] = pp[j-i+ii] + /\ qq[ii+1] = pp[j-i+ii+1] + BY <3>2, <5>3 + <6>. QED BY <3>2, <6>1 DEF Path + <5>. QED BY <5>1, <5>2, <5>3 + <4>. QED BY <4>1, <4>2, <4>3 DEF Path + <3>4. CR(qq) \in 0 .. k-1 + <4>. DEFINE inj == [ii \in Repeats(qq) |-> IF ii <= i THEN ii ELSE j-i+ii] + <4>1. ASSUME NEW ii \in Repeats(qq) + PROVE inj[ii] \in Repeats(pp) + BY <3>2 + <4>2. inj \in [Repeats(qq) -> Repeats(pp)] + BY <4>1, Zenon + <4>3. \A ii,jj \in Repeats(qq) : inj[ii] = inj[jj] => ii = jj + BY <3>2 + <4>4. inj \in Injection(Repeats(qq), Repeats(pp)) + BY <4>2, <4>3, Fun_IsInj, Zenon + <4>5. CR(qq) <= CR(pp) + BY <1>2, <4>4, FS_Injection, Zenon + <4>6. i \in Repeats(pp) + BY <3>1 + <4>7. i \notin Repeats(qq) + BY <3>2 + <4>8. inj \notin Surjection(Repeats(qq), Repeats(pp)) + BY <3>2, <4>6, <4>7, SMTT(10) DEF Surjection + <4>9. /\ CR(qq) <= CR(pp) + /\ CR(qq) # CR(pp) + <5>. HIDE DEF Repeats, inj, qq + <5>. QED BY <1>2, <4>4, <4>8, FS_Injection, Zenon + <4>. QED BY <1>2, <2>1, <3>3, <4>9, FS_CardinalityType, Isa + <3>5. qq[1] = m + BY <2>1 DEF Path + <3>6. qq[Len(qq)] = n + BY <2>1, <3>2 DEF Path + <3>. HIDE DEF CR, qq + <3>. QED BY <2>1, <3>3, <3>4, <3>5, <3>6 + <2>. HIDE DEF P + <2>. QED BY <2>2, <2>3, NatInduction, Isa +<1>. QED BY <1>1, <1>3, <1>4, Zenon + +(****************************************************************************) +(* Connectedness is a pre-order. *) +(****************************************************************************) +THEOREM ConnectedReflexive == + ASSUME NEW G, NEW a \in G.node + PROVE AreConnectedIn(a, a, G) +BY <> \in Seq(G.node) DEF AreConnectedIn, Path + +THEOREM ConnectedTransitive == + ASSUME NEW G, NEW a \in G.node, NEW b \in G.node, NEW c \in G.node, + AreConnectedIn(a, b, G), AreConnectedIn(b, c, G) + PROVE AreConnectedIn(a, c, G) +<1>1. PICK p \in Path(G) : p[1] = a /\ p[Len(p)] = b + BY DEF AreConnectedIn +<1>2. PICK q \in Path(G) : q[1] = b /\ q[Len(q)] = c + BY DEF AreConnectedIn +<1>. DEFINE pq == p \o Tail(q) +<1>3. pq \in Path(G) + BY <1>1, <1>2, PathConcatenation +<1>4. pq[1] = a /\ pq[Len(pq)] = c + BY <1>1, <1>2 DEF Path +<1>. QED BY <1>3, <1>4 DEF AreConnectedIn, Path + +(****************************************************************************) +(* A tree does not contain a cycle. One way to express this is that no *) +(* non-empty set of nodes is closed under successors. *) +(****************************************************************************) +THEOREM TreeAcyclic == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW S \in SUBSET G.node, S # {} + PROVE \E q \in S : \A e \in G.edge : e[1] = q => e[2] \notin S +<1>. DEFINE RootPaths(n) == {p \in Path(G) : p[1] = n /\ p[Len(p)] = r} + height(n) == Min({Len(p) : p \in RootPaths(n)}) +<1>1. \A n \in G.node : RootPaths(n) # {} + BY DEF IsTreeWithRoot, AreConnectedIn +<1>2. \A n \in G.node : /\ height(n) \in Nat + /\ \E p \in RootPaths(n) : Len(p) = height(n) + /\ \A p \in RootPaths(n) : Len(p) >= height(n) + <2>. TAKE n \in G.node + <2>1. {Len(p) : p \in RootPaths(n)} \in (SUBSET Nat) \ {{}} + BY <1>1 DEF Path + <2>2. /\ height(n) \in {Len(p) : p \in RootPaths(n)} + /\ \A l \in {Len(p) : p \in RootPaths(n)} : height(n) <= l + BY <2>1, MinNat + <2>. QED BY <2>1, <2>2 +<1>3. ASSUME NEW e \in G.edge + PROVE height(e[2]) < height(e[1]) + <2>1. e[1] \in G.node /\ e[2] \in G.node + BY DEF IsTreeWithRoot, IsDirectedGraph + <2>2. PICK p \in RootPaths(e[1]) : Len(p) = height(e[1]) + BY <1>2, <2>1 + <2>. p \in Seq(G.node) \ {<< >>} + BY DEF Path + <2>3. p[1] = e[1] /\ p[Len(p)] = r + BY DEF Path + <2>4. e[1] # r + BY DEF IsTreeWithRoot + <2>5. Len(p) >= 2 + BY <2>3, <2>4 + <2>6. <> \in G.edge + BY <2>5, 1 \in 1 .. Len(p)-1 DEF Path + <2>7. p[2] = e[2] + BY <2>3, <2>6 DEF IsTreeWithRoot + <2>. DEFINE q == Tail(p) + <2>8. q \in RootPaths(e[2]) + <3>1. q \in Seq(G.node) \ {<< >>} + BY <2>5 + <3>2. ASSUME NEW i \in 1 .. Len(q)-1 + PROVE <> \in G.edge + BY i+1 \in 1 .. Len(p)-1 DEF Path + <3>3. q[1] = e[2] /\ q[Len(q)] = r + BY <2>5, <2>7 + <3>. QED BY <3>1, <3>2, <3>3 DEF Path + <2>. HIDE DEF height + <2>. QED BY <1>2, <2>1, <2>2, <2>8 +<1>4. PICK q \in S : \A n \in S : height(q) <= height(n) + <2>. HIDE DEF height + <2>. DEFINE HS == {height(n) : n \in S} mh == Min(HS) + <2>1. HS \in (SUBSET Nat) \ {{}} + BY <1>2 + <2>2. /\ mh \in HS + /\ \A h \in HS : mh <= h + BY <2>1, MinNat + <2>. QED BY <2>2 +<1>. HIDE DEF RootPaths +<1>. QED BY <1>2, <1>3, <1>4 + +(****************************************************************************) +(* In particular, no node is its own successor in a tree, and all paths in *) +(* a tree are simple paths. *) +(****************************************************************************) +THEOREM TreeIrreflexive == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW n \in G.node + PROVE <> \notin G.edge +<1>1. PICK q \in {n} : \A e \in G.edge : e[1] = q => e[2] \notin {n} + BY TreeAcyclic, Zenon +<1>. QED BY <1>1 + +THEOREM TreeSimplePath == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW p \in Path(G) + PROVE p \in SimplePath(G) +<1>. SUFFICES ASSUME NEW i \in 1 .. Len(p), NEW j \in 1 .. Len(p), i < j, p[i] = p[j] + PROVE FALSE + BY DEF SimplePath +<1>. p \in Seq(G.node) \ { << >> } + BY DEF Path +<1>. DEFINE S == {p[k] : k \in i .. j} +<1>1. PICK k \in i..j : \A e \in G.edge : e[1] = p[k] => e[2] \notin S + BY TreeAcyclic, S \subseteq G.node, S # {} +<1>2. CASE k < j + <2>1. /\ <> \in G.edge + /\ p[k+1] \in S + BY <1>2 DEF Path + <2>. QED BY <1>1, <2>1 +<1>3. CASE k = j + <2>1. /\ <> \in G.edge + /\ p[i+1] \in S + BY DEF Path + <2>. QED BY <1>1, <1>3, <2>1 +<1>. QED BY <1>2, <1>3 + +(****************************************************************************) +(* Connectedness is antisymmetric (and thus a partial order) in trees. *) +(****************************************************************************) +THEOREM TreeConnectedAntisymmetric == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW a \in G.node, NEW b \in G.node, + AreConnectedIn(a, b, G), AreConnectedIn(b, a, G) + PROVE a = b +<1>1. PICK p \in Path(G) : p[1] = a /\ p[Len(p)] = b + BY DEF AreConnectedIn +<1>2. PICK q \in Path(G) : q[1] = b /\ q[Len(q)] = a + BY DEF AreConnectedIn +<1>. p \in Seq(G.node) \ { <<>> } /\ q \in Seq(G.node) \ { <<>> } + BY DEF Path +<1>. DEFINE pq == p \o Tail(q) +<1>3. pq \in Path(G) + BY <1>1, <1>2, PathConcatenation +<1>4. pq \in SimplePath(G) + BY <1>3, TreeSimplePath +<1>5. pq[1] = a /\ pq[Len(pq)] = a + BY <1>1, <1>2 +<1>6. Len(pq) = 1 + BY <1>4, <1>5 DEF SimplePath +<1>. QED BY <1>1, <1>6 + +(****************************************************************************) +(* A graph consisting of only the root and no edges is a tree. *) +(****************************************************************************) +THEOREM SingletonIsTreeWithRoot == + ASSUME NEW r + PROVE IsTreeWithRoot([node |-> {r}, edge |-> {}],r) +<1>. DEFINE G == [node |-> {r}, edge |-> {}] +<1>1. IsDirectedGraph(G) + BY DEF IsDirectedGraph +<1>2. \A n \in G.node : AreConnectedIn(n, r, G) + <2>. <> \in Path(G) + BY DEF Path + <2>. QED BY DEF AreConnectedIn +<1>. QED BY <1>1, <1>2 DEF IsTreeWithRoot, IsDirectedGraph + +(****************************************************************************) +(* A tree can be extended by attaching a disjoint tree to a node. *) +(****************************************************************************) +THEOREM AttachTree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), NEW n \in G.node, + NEW H, NEW s, IsTreeWithRoot(H,s), G.node \cap H.node = {} + PROVE IsTreeWithRoot([node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}], r) +<1>. DEFINE T == [node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}] +<1>1. IsDirectedGraph(T) + BY DEF IsDirectedGraph, IsTreeWithRoot +<1>2. r \in T.node + BY DEF IsTreeWithRoot +<1>3. ASSUME NEW e \in T.edge PROVE e[1] # r + BY DEF IsTreeWithRoot, IsDirectedGraph +<1>4. ASSUME NEW e \in T.edge, NEW f \in T.edge, e[1] = f[1] + PROVE e = f + BY <1>4 DEF IsTreeWithRoot, IsDirectedGraph +<1>5. ASSUME NEW nd \in T.node + PROVE AreConnectedIn(nd, r, T) + <2>1. CASE nd \in G.node + <3>1. PICK p \in Path(G) : p[1] = nd /\ p[Len(p)] = r + BY <2>1 DEF IsTreeWithRoot, AreConnectedIn + <3>2. p \in Path(T) + BY DEF Path + <3>. QED BY <3>1, <3>2 DEF AreConnectedIn + <2>2. CASE nd \in H.node + <3>1. PICK p \in Path(H) : p[1] = nd /\ p[Len(p)] = s + BY <2>2 DEF IsTreeWithRoot, AreConnectedIn + <3>2. PICK q \in Path(G) : q[1] = n /\ q[Len(q)] = r + BY DEF IsTreeWithRoot, AreConnectedIn + <3>. p \in Seq(H.node) \ { <<>> } /\ q \in Seq(G.node) \ { <<>> } + BY DEF Path + <3>. DEFINE pq == p \o q + <3>3. pq \in Seq(T.node) \ { <<>> } + BY <3>1, <3>2 + <3>4. ASSUME NEW i \in 1 .. Len(pq)-1 + PROVE << pq[i], pq[i+1] >> \in T.edge + <4>1. CASE i \in 1 .. Len(p)-1 + BY <4>1 DEF Path + <4>2. CASE i = Len(p) + BY <3>1, <3>2, <4>2 + <4>3. CASE i \in Len(p)+1 .. Len(pq)-1 + BY <4>3, i - Len(p) \in 1 .. Len(q)-1 DEF Path + <4>. QED BY <4>1, <4>2, <4>3 + <3>5. pq[1] = nd /\ pq[Len(pq)] = r + BY <3>1, <3>2 + <3>. HIDE DEF pq, T + <3>. QED BY <3>3, <3>4, <3>5 DEF AreConnectedIn, Path + <2>. QED BY <2>1, <2>2 +<1>. QED BY <1>1, <1>2, <1>3, <1>4, <1>5 DEF IsTreeWithRoot + +(****************************************************************************) +(* In particular, a tree can be extended by a new node that becomes a leaf. *) +(****************************************************************************) +THEOREM AddLeafToTree == + ASSUME NEW G, NEW r, NEW leaf, NEW parent, + IsTreeWithRoot(G,r), leaf \notin G.node, parent \in G.node + PROVE IsTreeWithRoot([node |-> G.node \cup {leaf}, + edge |-> G.edge \cup {<>}], r) +<1>. DEFINE H == [node |-> {leaf}, edge |-> {}] +<1>1. IsTreeWithRoot(H, leaf) + BY SingletonIsTreeWithRoot +<1>2. G.node \cap H.node = {} + OBVIOUS +<1>3. IsTreeWithRoot([node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}], r) + <2>. HIDE DEF H + <2>. QED BY <1>1, <1>2, AttachTree +<1>. QED BY <1>3, Zenon + +(****************************************************************************) +(* Removing a subtree from a tree maintains the tree property, provided it *) +(* is not the entire tree (trees must be non-empty.) *) +(****************************************************************************) +THEOREM RemoveSubtree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW nd \in G.node \ {r} + PROVE LET S == { n \in G.node : AreConnectedIn(n, nd, G) } + T == G.node \ S + E == G.edge \cap (T \X T) + IN IsTreeWithRoot([node |-> T, edge |-> E], r) +<1>. DEFINE S == { n \in G.node : AreConnectedIn(n, nd, G) } + T == G.node \ S + E == G.edge \cap (T \X T) + SG == [node |-> T, edge |-> E] +<1>1. IsDirectedGraph(SG) + BY DEF IsDirectedGraph +<1>2. r \in SG.node + <2>1. r \in G.node /\ AreConnectedIn(nd, r, G) + BY DEF IsTreeWithRoot + <2>2. ~ AreConnectedIn(r, nd, G) + BY <2>1, TreeConnectedAntisymmetric + <2>. QED BY <2>1, <2>2 +<1>3. ASSUME NEW e \in SG.edge + PROVE /\ e[1] # r + /\ \A f \in SG.edge : e[1] = f[1] => e = f + BY DEF IsTreeWithRoot +<1>4. ASSUME NEW n \in SG.node + PROVE AreConnectedIn(n, r, SG) + <2>1. PICK p \in Path(G) : p[1] = n /\ p[Len(p)] = r + BY DEF IsTreeWithRoot, AreConnectedIn + <2>. p \in Seq(G.node) \ { <<>> } + BY DEF Path + <2>2. p \in Seq(T) + <3>1. SUFFICES ASSUME NEW i \in 1 .. Len(p), AreConnectedIn(p[i], nd, G) + PROVE FALSE + OBVIOUS + <3>2. SubSeq(p, 1, i) \in Path(G) + BY SubPath + <3>3. AreConnectedIn(n, p[i], G) + BY <2>1, <3>2 DEF AreConnectedIn + <3>. QED BY <3>1, <3>3, ConnectedTransitive + <2>. HIDE DEF T + <2>3. \A i \in 1 .. Len(p)-1 : <> \in E + BY <2>2 DEF Path + <2>4. p \in Path(SG) + BY <2>2, <2>3 DEF Path + <2>. QED BY <2>1, <2>4 DEF AreConnectedIn +<1>. QED BY <1>1, <1>2, <1>3, <1>4 DEF IsTreeWithRoot + +(****************************************************************************) +(* In particular, removing a leaf node that is not the root from a tree *) +(* results in a tree. *) +(****************************************************************************) +THEOREM RemoveLeafFromTree == + ASSUME NEW G, NEW r, IsTreeWithRoot(G,r), + NEW leaf \in G.node, Predecessors(G, leaf) = {}, + NEW parent \in G.node, <> \in G.edge + PROVE IsTreeWithRoot([node |-> G.node \ {leaf}, + edge |-> G.edge \ {<>}], r) +<1>1. leaf # r + BY DEF IsTreeWithRoot +<1>. DEFINE S == {n \in G.node : AreConnectedIn(n, leaf, G)} + T == G.node \ S + E == G.edge \cap (T \X T) +<1>2. IsTreeWithRoot([node |-> T, edge |-> E], r) + BY <1>1, RemoveSubtree, IsaM("blast") +<1>3. S = {leaf} + <2>1. leaf \in S + BY ConnectedReflexive + <2>2. ASSUME NEW n \in G.node, AreConnectedIn(n, leaf, G) + PROVE n = leaf + <3>1. PICK p \in Path(G) : p[1] = n /\ p[Len(p)] = leaf + BY <2>2 DEF AreConnectedIn + <3>2. Len(p)-1 \notin 1 .. Len(p)-1 + BY <3>1 DEF Path, Predecessors + <3>. QED BY <3>1, <3>2 DEF Path + <2>. QED BY <2>1, <2>2 +<1>4. E = G.edge \ {<>} + <2>1. E \subseteq G.edge \ {<>} + BY <1>3 + <2>2. ASSUME NEW e \in G.edge, e # <> + PROVE e \in E + <3>1. PICK a \in G.node, b \in G.node : e = <> + BY DEF IsTreeWithRoot, IsDirectedGraph + <3>2. CASE a \in S \* a must be `leaf', but it has a unique successor + BY <1>3, <2>2, <3>1, <3>2 DEF IsTreeWithRoot + <3>3. CASE b \in S \* b must be `leaf', but it has no predecessor + BY <1>3, <3>1, <3>3 DEF Predecessors + <3>. QED BY <3>1, <3>2, <3>3 + <2>. QED BY <2>1, <2>2 +<1>. HIDE DEF E, S +<1>. QED BY <1>2, <1>3, <1>4 + +(****************************************************************************) +(* The operator IsTreeWithRoot is set up so that edges point towards the *) +(* root of the tree. Sometimes it is more natural to consider trees with *) +(* edges pointing towards the leaves. Such a graph G can be characterized *) +(* by the predicate IsTreeWithRoot(Transpose(G), r). *) +(* We prove lemmas analogous to the above ones about transposed trees. *) +(****************************************************************************) +THEOREM SingletonIsTransposedTreeWithRoot == + ASSUME NEW r + PROVE IsTreeWithRoot(Transpose([node |-> {r}, edge |-> {}]), r) +BY SingletonIsTreeWithRoot DEF Transpose + +THEOREM AttachTransposedTree == + ASSUME NEW G, NEW r, IsDirectedGraph(G), IsTreeWithRoot(Transpose(G), r), + NEW H, NEW s, IsDirectedGraph(H), IsTreeWithRoot(Transpose(H), s), + G.node \cap H.node = {}, NEW n \in G.node + PROVE IsTreeWithRoot(Transpose([node |-> G.node \cup H.node, + edge |-> G.edge \cup H.edge \cup {<>}]), r) +<1>. DEFINE GN == G.node GE == G.edge TGE == {<> : e \in GE} + HN == H.node HE == H.edge THE == {<> : e \in HE} +<1>1. /\ G = [node |-> GN, edge |-> GE] + /\ GE \subseteq GN \X GN + /\ H = [node |-> HN, edge |-> HE] + /\ HE \subseteq HN \X HN + BY DEF IsDirectedGraph +<1>. HIDE DEF GN, GE, HN, HE +<1>2. /\ Transpose(G) = [node |-> GN, edge |-> TGE] + /\ Transpose(H) = [node |-> HN, edge |-> THE] + BY <1>1 DEF Transpose +<1>3. IsTreeWithRoot([node |-> GN \cup HN, + edge |-> TGE \cup THE \cup {<>}], r) + BY <1>1, <1>2, AttachTree +<1>4. {<> : e \in GE \cup HE \cup {<>}} = TGE \cup THE \cup {<>} + BY <1>1 +<1>. QED BY <1>1, <1>3, <1>4 DEF Transpose + +THEOREM AddLeafToTransposedTree == + ASSUME NEW G, NEW r, NEW leaf, NEW parent, + IsDirectedGraph(G), IsTreeWithRoot(Transpose(G),r), + leaf \notin G.node, parent \in G.node + PROVE IsTreeWithRoot(Transpose([node |-> G.node \cup {leaf}, + edge |-> G.edge \cup {<>}]), r) +<1>. DEFINE N == G.node + E == G.edge + TE == {<> : e \in G.edge} +<1>1. /\ G = [node |-> N, edge |-> E] + /\ E \subseteq N \X N + BY DEF IsDirectedGraph +<1>. HIDE DEF N, E +<1>2. Transpose(G) = [node |-> N, edge |-> TE] + BY <1>1 DEF Transpose +<1>3. IsTreeWithRoot([node |-> N \cup {leaf}, + edge |-> TE \cup {<>}], r) + BY <1>1, <1>2, AddLeafToTree +<1>4. {<> : e \in E \cup {<>}} = TE \cup {<>} + BY <1>1 +<1>. QED BY <1>1, <1>3, <1>4 DEF Transpose + +THEOREM RemoveTransposedSubtree == + ASSUME NEW G, NEW r, IsDirectedGraph(G), IsTreeWithRoot(Transpose(G), r), + NEW nd \in G.node \ {r} + PROVE LET S == {n \in G.node : AreConnectedIn(nd, n, G)} + T == G.node \ S + E == G.edge \cap (T \X T) + IN IsTreeWithRoot(Transpose([node |-> T, edge |-> E]), r) +<1>. DEFINE GN == G.node GE == G.edge TGE == {<> : e \in GE} + S == {n \in GN : AreConnectedIn(nd, n, G)} + T == GN \ S + E == GE \cap (T \X T) + TG == Transpose(G) + TS == {n \in TG.node : AreConnectedIn(n, nd, TG)} + TT == TG.node \ TS + TE == TG.edge \cap (TT \X TT) +<1>1. /\ G = [node |-> GN, edge |-> GE] + /\ GE \subseteq GN \X GN + BY DEF IsDirectedGraph +<1>. HIDE DEF GN, GE +<1>2. TG = [node |-> GN, edge |-> TGE] + BY <1>1 DEF Transpose +<1>3. /\ IsTreeWithRoot(TG, r) + /\ nd \in TG.node \ {r} + BY <1>1, <1>2 +<1>4. IsTreeWithRoot([node |-> TT, edge |-> TE], r) + BY <1>3, RemoveSubtree, IsaM("blast") +<1>5. T = TT + BY TransposeAreConnectedIn, AreConnectedInTranspose, <1>1, <1>2 +<1>6. {<> : e \in E} = TE + BY <1>1, <1>2, <1>5 +<1>7. IsTreeWithRoot(Transpose([node |-> T, edge |-> E]), r) + <2>. HIDE DEF T, TT, E, TE + <2>. QED BY <1>4, <1>5, <1>6 DEF Transpose +<1>. QED BY <1>7 DEF GN, GE + +THEOREM RemoveLeafFromTransposedTree == + ASSUME NEW G, IsDirectedGraph(G), + NEW r, IsTreeWithRoot(Transpose(G),r), + NEW leaf \in G.node, + Successors(G, leaf) = {}, + NEW parent \in G.node, <> \in G.edge + PROVE IsTreeWithRoot(Transpose([node |-> G.node \ {leaf}, + edge |-> G.edge \ {<>}]), r) +<1>. DEFINE N == G.node + E == G.edge + TE == {<> : e \in G.edge} +<1>1. /\ G = [node |-> N, edge |-> E] + /\ E \subseteq N \X N + BY DEF IsDirectedGraph +<1>. HIDE DEF N, E +<1>2. /\ Transpose(G) = [node |-> N, edge |-> TE] + /\ Predecessors(Transpose(G), leaf) = {} + BY <1>1 DEF Transpose, Predecessors, Successors +<1>3. IsTreeWithRoot([node |-> N \ {leaf}, + edge |-> TE \ {<>}], r) + BY <1>1, <1>2, RemoveLeafFromTree +<1>4. {<> : e \in E \ {<>}} = TE \ {<>} + BY <1>1 +<1>. QED BY <1>1, <1>3, <1>4 DEF Transpose + +============================================================================== diff --git a/modules/Graphs.tla b/modules/Graphs.tla index 72e49b1..c07345b 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -1,10 +1,26 @@ -------------------------------- MODULE Graphs ------------------------------- +------------------------------- MODULE Graphs -------------------------------- +(****************************************************************************) +(* Representation of (directed) graphs in TLA+. *) +(* A graph is represented as a record with two fields: *) +(* - node holds the set of nodes of the graph, *) +(* - edge holds the set of edges, represented as pairs of nodes. *) +(* The definitions of the operators SimplePath, AreConnectedIn, and *) +(* IsStronglyConnected are overridden by TLC with methods defined in *) +(* tlc2/overrides/Graphs.java. *) +(****************************************************************************) + +EXTENDS Naturals, Sequences, FiniteSets, SequencesExt, Relation + +(* TLAPM does not play well with LOCAL INSTANCE. + Reinstate the following when that issue is fixed. LOCAL INSTANCE Naturals LOCAL INSTANCE Sequences -LOCAL INSTANCE SequencesExt LOCAL INSTANCE FiniteSets +LOCAL INSTANCE SequencesExt LOCAL INSTANCE Relation +*) +(***************************************************************************) IsDirectedGraph(G) == /\ G = [node |-> G.node, edge |-> G.edge] /\ G.edge \subseteq (G.node \X G.node) @@ -19,25 +35,36 @@ Transpose(G) == node |-> G.node] ----------------------------------------------------------------------------- +(***************************************************************************) +(* An undirected graph can be represented as a directed graph with a *) +(* symmetric edge relation. However, see alternative definitions of *) +(* undirected graphs in module UndirectedGraphs. *) +(***************************************************************************) IsUndirectedGraph(G) == /\ IsDirectedGraph(G) /\ \A e \in G.edge : <> \in G.edge UndirectedSubgraph(G) == {H \in DirectedSubgraph(G) : IsUndirectedGraph(H)} ----------------------------------------------------------------------------- +(***************************************************************************) +(* A path in a graph is a non-empty sequence of nodes connected by edges. *) +(* A simple path is a path that does not contain duplicate nodes. *) +(* Two nodes m and n are connected if there exists a path from m to n. *) +(* A graph is strongly connected if all of its nodes are connected. *) +(***************************************************************************) Path(G) == {p \in Seq(G.node) : /\ p # << >> /\ \A i \in 1..(Len(p)-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) : <> \in G.edge} + { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } AreConnectedIn(m, n, G) == - \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) + \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) + +IsStronglyConnected(G) == + \* A graph is strongly connected if all pairs of nodes are connected. + \A m, n \in G.node : AreConnectedIn(m, n, G) ConnectionsIn(G) == \* Compute a Boolean matrix that indicates, for each pair of nodes, @@ -45,6 +72,7 @@ ConnectionsIn(G) == \* 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. + \* Note that this is well-defined only for finite graphs. 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 @@ -57,14 +85,24 @@ ConnectionsIn(G) == \/ Cu[m,u] /\ Cu[u,n]] IN C[G.node] -IsStronglyConnected(G) == - \A m, n \in G.node : AreConnectedIn(m, n, G) ----------------------------------------------------------------------------- +(***************************************************************************) +(* A tree is a directed graph (with edges pointing towards the root) *) +(* such that: *) +(* - the root is a node of the graph (in particular, a tree is non-empty), *) +(* - every node has a single parent, and *) +(* - every node is connected to the root. *) +(* *) +(* Note that a tree with edges pointing towards the leaves satisfies *) +(* IsTreeWithRoot(Transpose(G), r). *) +(***************************************************************************) IsTreeWithRoot(G, r) == /\ IsDirectedGraph(G) + /\ r \in G.node /\ \A e \in G.edge : /\ e[1] # r /\ \A f \in G.edge : (e[1] = f[1]) => (e = f) /\ \A n \in G.node : AreConnectedIn(n, r, G) + ----------------------------------------------------------------------------- (*************************************************************) (* Returns the union of two graphs. *) diff --git a/modules/Quorum.tla b/modules/Quorum.tla new file mode 100644 index 0000000..584f369 --- /dev/null +++ b/modules/Quorum.tla @@ -0,0 +1,19 @@ +--------------------------------- MODULE Quorum ----------------------------- + +(***************************************************************************) +(* A quorum system for a set S is a non-empty collection of quorums, i.e. *) +(* subsets of S such that any two quorums intersect. It is typically also *) +(* assumed that a superset of a quorum is itself a quorum. *) +(* *) +(* For example, given a finite and non-empty set S of servers, the sets of *) +(* strict majorities among servers form a quorum system. *) +(***************************************************************************) + +QuorumSystem(S) == + { QS \in SUBSET (SUBSET S) : + /\ QS # {} + /\ \A Q1, Q2 \in QS : Q1 \cap Q2 # {} + /\ \A Q1, Q2 \in SUBSET S : Q1 \in QS /\ Q1 \subseteq Q2 => Q2 \in QS + } + +============================================================================= diff --git a/modules/QuorumTheorems.tla b/modules/QuorumTheorems.tla new file mode 100644 index 0000000..b36acb1 --- /dev/null +++ b/modules/QuorumTheorems.tla @@ -0,0 +1,26 @@ +----------------------------- MODULE QuorumTheorems ------------------------- +EXTENDS Quorum, Integers, FiniteSets + +(***************************************************************************) +(* Direct consequences of the definition of a quorum system. *) +(***************************************************************************) + +THEOREM QuorumsIntersect == + ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS + PROVE \E s \in S : s \in Q1 \cap Q2 + +THEOREM QuorumSuperset == + ASSUME NEW S, NEW QS \in QuorumSystem(S), + NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2 + PROVE Q2 \in QS + +(***************************************************************************) +(* Strict majorities of a non-empty set S form a quorum system. *) +(***************************************************************************) + +THEOREM MajoritiesQuorumSystem == + ASSUME NEW S, IsFiniteSet(S), S # {} + PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } + \in QuorumSystem(S) + +============================================================================= diff --git a/modules/QuorumTheorems_proofs.tla b/modules/QuorumTheorems_proofs.tla new file mode 100644 index 0000000..d2d27e4 --- /dev/null +++ b/modules/QuorumTheorems_proofs.tla @@ -0,0 +1,29 @@ +------------------------- MODULE QuorumTheorems_proofs ---------------------- +EXTENDS Quorum, Integers, FiniteSetTheorems, FiniteSetsExtTheorems + +(***************************************************************************) +(* Direct consequences of the definition of a quorum system. *) +(***************************************************************************) + +THEOREM QuorumsIntersect == + ASSUME NEW S, NEW QS \in QuorumSystem(S), NEW Q1 \in QS, NEW Q2 \in QS + PROVE \E s \in S : s \in Q1 \cap Q2 +BY DEF QuorumSystem + +THEOREM QuorumSuperset == + ASSUME NEW S, NEW QS \in QuorumSystem(S), + NEW Q1 \in QS, NEW Q2 \in SUBSET S, Q1 \subseteq Q2 + PROVE Q2 \in QS +BY DEF QuorumSystem + +(***************************************************************************) +(* Strict majorities of a non-empty set S form a quorum system. *) +(***************************************************************************) + +THEOREM MajoritiesQuorumSystem == + ASSUME NEW S, IsFiniteSet(S), S # {} + PROVE { Q \in SUBSET S : 2 * Cardinality(Q) > Cardinality(S) } + \in QuorumSystem(S) +BY FS_CardinalityType, FS_EmptySet, FS_Subset, FS_Union DEF QuorumSystem + +============================================================================= diff --git a/modules/Relation.tla b/modules/Relation.tla index 0820cbf..c1a853a 100644 --- a/modules/Relation.tla +++ b/modules/Relation.tla @@ -1,6 +1,10 @@ ----------------------------- MODULE Relation ------------------------------ +EXTENDS Naturals, FiniteSets +(* TLAPM does not play well with LOCAL INSTANCE. + Reinstate the following when that issue is fixed. LOCAL INSTANCE Naturals LOCAL INSTANCE FiniteSets +*) (***************************************************************************) (* This module provides some basic operations on relations, represented *) diff --git a/modules/SequencesExt.tla b/modules/SequencesExt.tla index bb4a14d..104d8df 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -1,5 +1,5 @@ ---------------------------- MODULE SequencesExt ---------------------------- -EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags +EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags, TLC \* TLAPM does not play well with LOCAL INSTANCE, reinstate the following \* when that issue is fixed. \* LOCAL INSTANCE Sequences @@ -9,7 +9,7 @@ EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags \* LOCAL INSTANCE Folds \* LOCAL INSTANCE Functions \* LOCAL INSTANCE Bags -LOCAL INSTANCE TLC +\* LOCAL INSTANCE TLC (*************************************************************************) (* Imports the definitions from the modules, but doesn't export them. *) (*************************************************************************) @@ -106,6 +106,31 @@ BoundedSeq(S, n) == Contains(s, e) == \E i \in 1..Len(s) : s[i] = e +(**************************************************************************) +(* TRUE iff the sequence s is sorted with respect to the binary *) +(* relation op, i.e. op(s[i], s[j]) holds for every pair of positions *) +(* i, j in the domain of s with i < j. *) +(* *) +(* No assumptions are made about op; its meaning is fixed by the *) +(* caller. When op is a strict order (irreflexive and transitive), *) +(* s is strictly increasing and therefore duplicate-free; when op is *) +(* a reflexive relation such as <=, equal elements may be adjacent. *) +(* Instantiating op with the converse relation sorts s in the *) +(* opposite direction. The empty sequence and every singleton are *) +(* vacuously sorted under any op. *) +(* *) +(* Examples: *) +(* IsSorted(<<>>, <) = TRUE *) +(* IsSorted(<<5>>, <) = TRUE *) +(* IsSorted(<<1, 2, 3>>, <) = TRUE *) +(* IsSorted(<<1, 2, 2>>, <) = FALSE (not strictly increasing) *) +(* IsSorted(<<1, 2, 2>>, <=) = TRUE *) +(* IsSorted(<<3, 2, 1>>, <) = FALSE *) +(* IsSorted(<<3, 2, 1>>, >) = TRUE *) +(**************************************************************************) +IsSorted(s, op(_, _)) == + \A i, j \in 1..Len(s) : i < j => op(s[i], s[j]) + (**************************************************************************) (* Reverse the given sequence s: Let l be Len(s) (length of s). *) (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>> *) diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla index a04ddbd..95279e0 100644 --- a/modules/SequencesExtTheorems.tla +++ b/modules/SequencesExtTheorems.tla @@ -6,6 +6,13 @@ (**************************************************************************) EXTENDS Sequences, SequencesExt, Functions, Integers, WellFoundedInduction +(***************************************************************************) +(* SeqOf(S,n) is the set of sequences over S whose length is at most n. *) +(***************************************************************************) +THEOREM SeqOfSeq == + ASSUME NEW S, NEW n \in Int + PROVE SeqOf(S,n) = {s \in Seq(S) : Len(s) <= n} + (***************************************************************************) (* Theorems about Cons. *) (* Cons(elt, seq) == <> \o seq *) @@ -47,6 +54,97 @@ THEOREM SequencesInductionCons == \A s \in Seq(S), e \in S : P(s) => P(Cons(e,s)) PROVE \A seq \in Seq(S) : P(seq) +(***************************************************************************) +(* Theorems about Contains. *) +(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *) +(***************************************************************************) + +(* Membership in a sequence coincides with membership in its image set. *) +THEOREM ContainsRange == + ASSUME NEW S, NEW s \in Seq(S), NEW e + PROVE Contains(s, e) <=> e \in Range(s) + +THEOREM ContainsEmpty == + ASSUME NEW e + PROVE ~ Contains(<< >>, e) + +THEOREM ContainsAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x) + +THEOREM ContainsSingleton == + ASSUME NEW S, NEW x + PROVE \A e : Contains(<< x >>, e) <=> e = x + +THEOREM ContainsConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e + PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e)) + +THEOREM ContainsCons == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e)) + +THEOREM ContainsTail == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e + PROVE Contains(Tail(s), e) => Contains(s, e) + +(* An element other than the head of a non-empty sequence that occurs in *) +(* the sequence also occurs in its tail. *) +THEOREM ContainsTailExceptHead == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e, + Contains(s, e), e # Head(s) + PROVE Contains(Tail(s), e) + +(***************************************************************************) +(* Theorems about IsSorted (see SequencesExt). *) +(* *) +(* The relevant order properties of op (transitivity, irreflexivity) *) +(* are stated locally as hypotheses of each theorem, so that the *) +(* theorems apply to an arbitrary binary relation op rather than only *) +(* to relations globally known to be orders. *) +(***************************************************************************) + +THEOREM SortedEmpty == + ASSUME NEW op(_,_) + PROVE IsSorted(<< >>, op) + +THEOREM SortedSingleton == + ASSUME NEW S, NEW x \in S, NEW op(_,_) + PROVE IsSorted(<< x >>, op) + +(* Appending an element that dominates the last one keeps the sequence *) +(* sorted, provided the ordering relation is transitive. *) +THEOREM SortedAppend == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), IsSorted(s, op), + NEW e \in S, s # << >> => op(s[Len(s)], e) + PROVE IsSorted(Append(s, e), op) + +(* Concatenating two sorted sequences whose boundary elements are ordered *) +(* yields a sorted sequence (for a transitive ordering relation). *) +THEOREM SortedConcat == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), NEW t \in Seq(S), + IsSorted(s, op), IsSorted(t, op), + (Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1]) + PROVE IsSorted(s \o t, op) + +(* A sequence sorted by an irreflexive relation has no repeated elements. *) +THEOREM SortedInjective == + ASSUME NEW S, NEW op(_,_), + \A x \in S : ~ op(x, x), + NEW s \in Seq(S), IsSorted(s, op) + PROVE IsInjective(s) + +(* Any contiguous subsequence of a sorted sequence is sorted. *) +THEOREM SortedSubSeq == + ASSUME NEW S, NEW op(_,_), + NEW s \in Seq(S), IsSorted(s, op), + NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s) + PROVE IsSorted(SubSeq(s, m, n), op) + (***************************************************************************) (* Theorems about InsertAt and RemoveAt. *) (* InsertAt(seq,i,elt) == *) diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla index 3c4700c..00bf47f 100644 --- a/modules/SequencesExtTheorems_proofs.tla +++ b/modules/SequencesExtTheorems_proofs.tla @@ -7,6 +7,20 @@ EXTENDS Sequences, SequencesExt, FiniteSetsExt, Functions, Integers, SequenceTheorems, NaturalsInduction, WellFoundedInduction, FiniteSetTheorems, FiniteSetsExtTheorems, FoldsTheorems, TLAPS +(***************************************************************************) +(* SeqOf(S,n) is the set of sequences over S whose length is at most n. *) +(***************************************************************************) +THEOREM SeqOfSeq == + ASSUME NEW S, NEW n \in Int + PROVE SeqOf(S,n) = {s \in Seq(S) : Len(s) <= n} +<1>1. ASSUME NEW s \in SeqOf(S,n) + PROVE s \in Seq(S) /\ Len(s) <= n + BY DEF SeqOf +<1>2. ASSUME NEW s \in Seq(S), Len(s) <= n + PROVE s \in SeqOf(S,n) + BY <1>2 DEF SeqOf +<1>. QED BY <1>1, <1>2 + (***************************************************************************) (* Theorems about Cons. *) (* Cons(elt, seq) == <> \o seq *) @@ -79,6 +93,108 @@ THEOREM SequencesInductionCons == <2>. QED BY <2>1 <1>. QED BY <1>2, <1>3, NatInduction, Isa +(***************************************************************************) +(* Theorems about Contains. *) +(* Contains(s, e) == \E i \in 1 .. Len(s) : s[i] = e *) +(***************************************************************************) + +THEOREM ContainsRange == + ASSUME NEW S, NEW s \in Seq(S), NEW e + PROVE Contains(s, e) <=> e \in Range(s) +BY DEF Contains, Range + +THEOREM ContainsEmpty == + ASSUME NEW e + PROVE ~ Contains(<< >>, e) +BY DEF Contains + +THEOREM ContainsAppend == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Append(s, x), e) <=> (Contains(s, e) \/ e = x) +BY DEF Contains + +THEOREM ContainsSingleton == + ASSUME NEW x + PROVE \A e : Contains(<< x >>, e) <=> e = x +BY Isa DEF Contains + +THEOREM ContainsConcat == + ASSUME NEW S, NEW s \in Seq(S), NEW T, NEW t \in Seq(T), NEW e + PROVE Contains(s \o t, e) <=> (Contains(s, e) \/ Contains(t, e)) +<1>1. ASSUME Contains(s \o t, e), ~ Contains(t, e) PROVE Contains(s, e) + BY <1>1 DEF Contains +<1>2. ASSUME Contains(s, e) PROVE Contains(s \o t, e) + <2>. PICK i \in 1 .. Len(s) : s[i] = e + BY <1>2 DEF Contains + <2>. QED BY i \in 1 .. Len(s \o t) DEF Contains +<1>3. ASSUME Contains(t, e) PROVE Contains(s \o t, e) + <2>. PICK i \in 1 .. Len(t) : t[i] = e + BY <1>3 DEF Contains + <2>. QED BY Len(s)+i \in 1 .. Len(s \o t) DEF Contains +<1>. QED BY <1>1, <1>2, <1>3 + +THEOREM ContainsCons == + ASSUME NEW S, NEW s \in Seq(S), NEW x, NEW e + PROVE Contains(Cons(x, s), e) <=> (e = x \/ Contains(s, e)) +BY ContainsConcat, ContainsSingleton, <> \in Seq({x}) DEF Cons + +THEOREM ContainsTail == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e + PROVE Contains(Tail(s), e) => Contains(s, e) +BY DEF Contains + +THEOREM ContainsTailExceptHead == + ASSUME NEW S, NEW s \in Seq(S), s # << >>, NEW e, + Contains(s, e), e # Head(s) + PROVE Contains(Tail(s), e) +BY DEF Contains + +(***************************************************************************) +(* Theorems about IsSorted. *) +(* IsSorted(s, op) == \A i,j \in 1..Len(s) : i op(s[i],s[j]) *) +(***************************************************************************) + +THEOREM SortedEmpty == + ASSUME NEW op(_,_) + PROVE IsSorted(<< >>, op) +BY DEF IsSorted + +THEOREM SortedSingleton == + ASSUME NEW S, NEW x \in S, NEW op(_,_) + PROVE IsSorted(<< x >>, op) +BY DEF IsSorted + +THEOREM SortedAppend == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), IsSorted(s, op), + NEW e \in S, s # << >> => op(s[Len(s)], e) + PROVE IsSorted(Append(s, e), op) +BY DEF IsSorted + +THEOREM SortedConcat == + ASSUME NEW S, NEW op(_,_), + \A x,y,z \in S : op(x,y) /\ op(y,z) => op(x,z), + NEW s \in Seq(S), NEW t \in Seq(S), + IsSorted(s, op), IsSorted(t, op), + (Len(s) > 0 /\ Len(t) > 0) => op(s[Len(s)], t[1]) + PROVE IsSorted(s \o t, op) +BY SMTT(20) DEF IsSorted + +THEOREM SortedInjective == + ASSUME NEW S, NEW op(_,_), + \A x \in S : ~ op(x, x), + NEW s \in Seq(S), IsSorted(s, op) + PROVE IsInjective(s) +BY DEF IsSorted, IsInjective + +THEOREM SortedSubSeq == + ASSUME NEW S, NEW op(_,_), + NEW s \in Seq(S), IsSorted(s, op), + NEW m \in 1..Len(s)+1, NEW n \in 0..Len(s) + PROVE IsSorted(SubSeq(s, m, n), op) +BY DEF IsSorted + (***************************************************************************) (* Theorems about InsertAt and RemoveAt. *) (* InsertAt(seq,i,elt) == *) diff --git a/modules/UndirectedGraphs.tla b/modules/UndirectedGraphs.tla index 95c3e54..ee0bdb2 100644 --- a/modules/UndirectedGraphs.tla +++ b/modules/UndirectedGraphs.tla @@ -3,12 +3,16 @@ (* Representation of undirected graphs in TLA+. In contrast to module *) (* Graphs, edges are represented as unordered pairs {a,b} of nodes, thus *) (* enforcing symmetry. *) +(* The definitions of the operators SimplePath, AreConnectedIn, and *) +(* ConnectedComponents are overridden by TLC with methods defined in *) +(* tlc2/overrides/UndirectedGraphs.java. *) (****************************************************************************) LOCAL INSTANCE Naturals LOCAL INSTANCE Sequences LOCAL INSTANCE SequencesExt LOCAL INSTANCE FiniteSets LOCAL INSTANCE Folds +LOCAL INSTANCE Functions IsUndirectedGraph(G) == /\ G = [node |-> G.node, edge |-> G.edge] @@ -22,38 +26,60 @@ UndirectedSubgraph(G) == {H \in [node : SUBSET G.node, edge : SUBSET G.edge] : IsUndirectedGraph(H)} ----------------------------------------------------------------------------- +(****************************************************************************) +(* A path in a graph is a non-empty sequence of nodes connected by edges. *) +(* A simple path is a path that does not contain duplicate nodes. *) +(* Two nodes m and n are connected if there exists a path from m to n. *) +(* A graph is strongly connected if all of its nodes are connected. *) +(****************************************************************************) 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} + { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } + +AreConnectedIn(m, n, G) == + \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) +----------------------------------------------------------------------------- (****************************************************************************) -(* 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. *) +(* The (maximal) connected components are the maximal non-empty subsets S *) +(* of nodes such that any two nodes in the set are connected by a path that *) +(* only visits nodes in S. A graph is strongly connected if and only if it *) +(* has precisely one connected component containing all nodes. *) (****************************************************************************) -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) == <> - 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) +ConnectedComponents(G) == + LET IsCC(S) == /\ S # {} + /\ \A m,n \in S : \E p \in Seq(S) : + /\ p # << >> + /\ p[1] = m /\ p[Len(p)] = n + /\ \A i \in 1 .. Len(p)-1 : {p[i], p[i+1]} \in G.edge + IN { S \in SUBSET G.node : + /\ IsCC(S) + /\ \A T \in SUBSET G.node : S \subseteq T /\ S # T => ~ IsCC(T) + } -AreConnectedIn(m, n, G) == - \E comp \in ConnectedComponents(G) : m \in comp /\ n \in comp +\* Observe that the possible alternative definition +\* "Cardinality(ConnectedComponents(G)) = 1" makes sense only if the +\* set of connected components is finite, and this need not be the case +\* in general. +IsStronglyConnected(G) == ConnectedComponents(G) = {G.node} -IsStronglyConnected(G) == - Cardinality(ConnectedComponents(G)) = 1 +----------------------------------------------------------------------------- +(****************************************************************************) +(* The set of all possible undirected graphs whose node set is S. *) +(* *) +(* Example: *) +(* UndirectedGraphs({1, 2}) = { *) +(* [node |-> {1, 2}, edge |-> {}], *) +(* [node |-> {1, 2}, edge |-> {{1}}], *) +(* [node |-> {1, 2}, edge |-> {{2}}], *) +(* [node |-> {1, 2}, edge |-> {{1,2}}], *) +(* [node |-> {1, 2}, edge |-> {{1}, {1,2}}], *) +(* [node |-> {1, 2}, edge |-> {{2}, {1,2}}], *) +(* [node |-> {1, 2}, edge |-> {{1}, {2}, {1,2}}], *) +(* } *) +(****************************************************************************) +UndirectedGraphs(S) == [node: {S}, edge: SUBSET { {s, t} : <> \in S \X S }] ============================================================================= diff --git a/modules/tlc2/overrides/AbstractGraphs.java b/modules/tlc2/overrides/AbstractGraphs.java new file mode 100644 index 0000000..dba8431 --- /dev/null +++ b/modules/tlc2/overrides/AbstractGraphs.java @@ -0,0 +1,261 @@ +/******************************************************************************* + * Copyright (c) 2026 TLA+ Foundation. 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 + * Stephan Merz - undirected graphs + ******************************************************************************/ +package tlc2.overrides; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collections; +import java.util.Deque; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import tlc2.output.EC; +import tlc2.tool.EvalException; +import tlc2.value.Values; +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.StringValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; +import tlc2.value.impl.ValueEnumeration; + +/* + * Shared implementation of the TLC module overrides for the Graphs and + * UndirectedGraphs modules. The two graph kinds differ only in how an element + * of G.edge denotes a pair of endpoints (an ordered 2-tuple for directed graphs + * versus an unordered pair {a,b} for undirected graphs) and in whether the + * resulting adjacency relation is symmetric. Subclasses supply those two aspects + * as an Endpoints delegate and a Mode; everything else (argument validation, + * adjacency construction, path enumeration and reachability) is shared here. + * + * All members are static: subclasses inherit these helpers and call them, + * passing their own edge parser. The class is abstract only to prevent + * instantiation and to give the two override classes a common home. + */ +public abstract class AbstractGraphs { + + protected AbstractGraphs() { + // no-instantiation! + } + + protected static final StringValue NODE = new StringValue("node"); + protected static final StringValue EDGE = new StringValue("edge"); + + /* + * Parses one element of G.edge into its two endpoints {from, to}, or returns + * null if the value cannot denote an edge (and is therefore ignored). A + * self-loop is returned as {n, n}. + */ + @FunctionalInterface + protected interface Endpoints { + Value[] of(Value edge); + } + + /* + * How the arcs of the adjacency relation are derived from an edge's endpoints: + * FORWARD keeps the edge's orientation, TRANSPOSE reverses it, and SYMMETRIC + * adds both orientations. + */ + protected enum Mode { + FORWARD, TRANSPOSE, SYMMETRIC + } + + /* + * Validate that v is a graph record, i.e. a record with a "node" and an "edge" + * field, both of which are sets. Reporting the argument's position (e.g. "third" + * for AreConnectedIn) and rejecting malformed records here yields a proper + * user-facing TLC module argument error instead of a NullPointerException or + * ClassCastException later in nodes/adjacency. The kind noun (e.g. "graph" or + * "undirected graph") tailors the message to the calling module. + */ + protected static RecordValue toGraph(final String op, final String argPos, final String kind, final Value v) { + final Value rcd = v.toRcd(); + if (!(rcd instanceof RecordValue)) { + throw argError(op, argPos, kind, "record with a node and an edge field", v); + } + final RecordValue g = (RecordValue) rcd; + final Value node = g.select(NODE); + if (node == null || node.toSetEnum() == null) { + throw argError(op, argPos, kind, "record whose node field is a set", v); + } + final Value edge = g.select(EDGE); + if (edge == null || edge.toSetEnum() == null) { + throw argError(op, argPos, kind, "record whose edge field is a set", v); + } + return g; + } + + private static EvalException argError(final String op, final String argPos, final String kind, + final String detail, final Value v) { + return new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, kind + " " + detail, Values.ppr(v.toString()) }); + } + + protected static SetEnumValue nodes(final RecordValue g) { + final SetEnumValue nodes = (SetEnumValue) g.select(NODE).toSetEnum(); + nodes.normalize(); + return nodes; + } + + protected static SetEnumValue edges(final RecordValue g) { + final SetEnumValue edges = (SetEnumValue) g.select(EDGE).toSetEnum(); + edges.normalize(); + return edges; + } + + /* + * Adjacency list of the graph, restricted to edges whose endpoints are both + * elements of the node set. This mirrors the TLA+ definitions, in which any + * node on a path is drawn from G.node. Edges that the parser cannot handle + * (e.g. a tuple of the wrong arity, or a set of zero or more than two elements) + * contribute no arc and are skipped. + */ + protected static Map> adjacency(final RecordValue g, final SetEnumValue nodes, + final Endpoints parser, final Mode mode) { + final Map> adj = new HashMap<>(); + final ValueEnumeration ve = edges(g).elements(); + Value v; + while ((v = ve.nextElement()) != null) { + final Value[] e = parser.of(v); + if (e == null) { + continue; + } + Value from = e[0]; + Value to = e[1]; + if (!nodes.member(from) || !nodes.member(to)) { + continue; + } + if (mode == Mode.TRANSPOSE) { + final Value tmp = from; + from = to; + to = tmp; + } + addArc(adj, from, to); + if (mode == Mode.SYMMETRIC && !from.equals(to)) { + addArc(adj, to, from); + } + } + return adj; + } + + private static void addArc(final Map> adj, final Value from, final Value to) { + adj.computeIfAbsent(from, k -> new ArrayList<>()).add(to); + } + + // Breadth-first search returning all nodes reachable from source (inclusive). + protected static Set reachable(final Value source, final Map> adj) { + final Set visited = new HashSet<>(); + final Deque frontier = new ArrayDeque<>(); + visited.add(source); + frontier.add(source); + while (!frontier.isEmpty()) { + final Value current = frontier.remove(); + for (final Value succ : adj.getOrDefault(current, Collections.emptyList())) { + if (visited.add(succ)) { + frontier.add(succ); + } + } + } + return visited; + } + + /* + * SimplePath(G) == { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } + * + * Enumerates the set of all (non-empty) simple paths of G via depth-first + * search. This avoids materializing the (infinite) set Path(G) that the pure + * TLA+ definition ranges over. + */ + protected static Value simplePath(final String kind, final Endpoints parser, final Mode mode, final Value graph) { + final RecordValue g = toGraph("SimplePath", "first", kind, graph); + final SetEnumValue nodes = nodes(g); + final Map> adj = adjacency(g, nodes, parser, mode); + + final List paths = new ArrayList<>(); + final List path = new ArrayList<>(); + final Set visited = new HashSet<>(); + final ValueEnumeration ve = nodes.elements(); + Value start; + while ((start = ve.nextElement()) != null) { + path.add(start); + visited.add(start); + extendSimplePath(start, adj, path, visited, paths); + visited.remove(start); + path.remove(path.size() - 1); + } + + return new SetEnumValue(paths.toArray(new Value[paths.size()]), false); + } + + // Backtracking depth-first search: emit the current path, then recurse into + // each unvisited successor. Every non-empty prefix of a simple path is itself + // a simple path. + private static void extendSimplePath(final Value current, final Map> adj, + final List path, final Set visited, final List paths) { + paths.add(new TupleValue(path.toArray(new Value[path.size()]))); + for (final Value succ : adj.getOrDefault(current, Collections.emptyList())) { + if (visited.add(succ)) { + path.add(succ); + extendSimplePath(succ, adj, path, visited, paths); + path.remove(path.size() - 1); + visited.remove(succ); + } + } + } + + /* + * AreConnectedIn(m, n, G) == \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) + * + * There is a path from m to n. Note that <> is a path, so a node is + * connected to itself iff it is a node of G. + */ + protected static Value areConnectedIn(final String kind, final Endpoints parser, final Mode mode, + final Value m, final Value n, final Value graph) { + final RecordValue g = toGraph("AreConnectedIn", "third", kind, graph); + final SetEnumValue nodes = nodes(g); + + // Every node on a path is drawn from G.node, so m and n must both be nodes. + // Checking membership first also matches the pure definition on an empty node + // set: the existential domain Path(G) is empty, hence the result is FALSE and + // no comparison of m and n happens. Comparing m and n up front (via the + // self-connection fast path below) would instead raise a type error for + // incompatible arguments, e.g. AreConnectedIn(1, "x", G). + if (!nodes.member(m) || !nodes.member(n)) { + return BoolValue.ValFalse; + } + if (m.equals(n)) { + return BoolValue.ValTrue; + } + + final Map> adj = adjacency(g, nodes, parser, mode); + return reachable(m, adj).contains(n) ? BoolValue.ValTrue : BoolValue.ValFalse; + } +} diff --git a/modules/tlc2/overrides/Graphs.java b/modules/tlc2/overrides/Graphs.java new file mode 100644 index 0000000..73d11e6 --- /dev/null +++ b/modules/tlc2/overrides/Graphs.java @@ -0,0 +1,109 @@ +/******************************************************************************* + * Copyright (c) 2026 NVIDIA Corporation. 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.List; +import java.util.Map; + +import tlc2.value.impl.BoolValue; +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.TupleValue; +import tlc2.value.impl.Value; + +/* + * TLC overrides for the (directed) Graphs module. Edges are ordered 2-tuples + * <>. The bulk of the implementation is shared with UndirectedGraphs + * via AbstractGraphs; this class only supplies the directed edge parser and the + * operator entry points. + */ +public final class Graphs extends AbstractGraphs { + + private Graphs() { + // no-instantiation! + } + + private static final String KIND = "graph"; + + /* + * The definitions test <> \in G.edge, i.e. membership of an exact + * 2-tuple. Any element of G.edge that is not a 2-tuple (e.g. <> or + * <>) can therefore never match and contributes no edge, so it is + * skipped rather than mis-parsed (as u -> v) or causing an out-of-bounds error. + */ + private static final Endpoints TUPLE = edge -> { + final Value tuple = edge.toTuple(); + if (!(tuple instanceof TupleValue) || ((TupleValue) tuple).size() != 2) { + return null; + } + final TupleValue e = (TupleValue) tuple; + return new Value[] { e.elems[0], e.elems[1] }; + }; + + @TLAPlusOperator(identifier = "SimplePath", module = "Graphs", warn = false) + public static Value simplePath(final Value graph) { + return simplePath(KIND, TUPLE, Mode.FORWARD, graph); + } + + @TLAPlusOperator(identifier = "AreConnectedIn", module = "Graphs", warn = false) + public static Value areConnectedIn(final Value m, final Value n, final Value graph) { + return areConnectedIn(KIND, TUPLE, Mode.FORWARD, m, n, graph); + } + + /* + * IsStronglyConnected(G) == \A m, n \in G.node : AreConnectedIn(m, n, G) + * + * G is strongly connected iff, from an arbitrary node r, every node is reachable + * (forward) and r is reachable from every node (i.e., every node is reachable in + * the transposed graph). This is the two-pass reachability test underlying + * Kosaraju's algorithm and runs in linear time instead of enumerating all pairs + * of nodes. + */ + @TLAPlusOperator(identifier = "IsStronglyConnected", module = "Graphs", warn = false) + public static Value isStronglyConnected(final Value graph) { + final RecordValue g = toGraph("IsStronglyConnected", "first", KIND, graph); + final SetEnumValue nodes = nodes(g); + + final int order = nodes.size(); + if (order == 0) { + return BoolValue.ValTrue; + } + + final Value root = nodes.elements().nextElement(); + + final Map> adj = adjacency(g, nodes, TUPLE, Mode.FORWARD); + if (reachable(root, adj).size() != order) { + return BoolValue.ValFalse; + } + + final Map> radj = adjacency(g, nodes, TUPLE, Mode.TRANSPOSE); + if (reachable(root, radj).size() != order) { + return BoolValue.ValFalse; + } + + return BoolValue.ValTrue; + } +} diff --git a/modules/tlc2/overrides/TLCOverrides.java b/modules/tlc2/overrides/TLCOverrides.java index 52ac71b..8938f53 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -45,7 +45,8 @@ 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, VectorClocks.class, GraphViz.class }; + DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class, + UndirectedGraphs.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 +54,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, VectorClocks.class, GraphViz.class }; + Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class, UndirectedGraphs.class }; } } diff --git a/modules/tlc2/overrides/UndirectedGraphs.java b/modules/tlc2/overrides/UndirectedGraphs.java new file mode 100644 index 0000000..d56c50e --- /dev/null +++ b/modules/tlc2/overrides/UndirectedGraphs.java @@ -0,0 +1,195 @@ +/******************************************************************************* + * Copyright (c) 2026 TLA+ Foundation. 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: + * Stephan Merz - initial API and implementation (largely based on Graphs.java) + ******************************************************************************/ +package tlc2.overrides; + +import java.util.LinkedHashMap; +import java.util.Map; + +import tlc2.value.impl.RecordValue; +import tlc2.value.impl.SetEnumValue; +import tlc2.value.impl.Value; +import tlc2.value.impl.ValueEnumeration; + +/* + * TLC overrides for the UndirectedGraphs module. Edges are unordered pairs, i.e. + * sets {a, b} of one or two nodes. SimplePath and AreConnectedIn are shared with + * the directed Graphs module via AbstractGraphs; this class supplies the + * undirected edge parser and the ConnectedComponents override. + */ +public final class UndirectedGraphs extends AbstractGraphs { + + private UndirectedGraphs() { + // no-instantiation! + } + + private static final String KIND = "undirected graph"; + + /* + * The definitions test {p[i], p[i+1]} \in G.edge, i.e. membership of an unordered + * pair. Any element of G.edge that is not a set of one or two elements (e.g. {} + * or {u, v, x}) can therefore never match and contributes no edge, so it is + * skipped. A singleton {u} denotes the self-loop {u, u}. + */ + private static final Endpoints PAIR = edge -> { + final Value set = edge.toSetEnum(); + if (!(set instanceof SetEnumValue)) { + return null; + } + final SetEnumValue e = (SetEnumValue) set; + if ((e.size() == 0) || (e.size() > 2)) { + return null; + } + final ValueEnumeration ne = e.elements(); + final Value from = ne.nextElement(); + final Value to = ne.nextElement(); + return new Value[] { from, to == null ? from : to }; + }; + + @TLAPlusOperator(identifier = "SimplePath", module = "UndirectedGraphs", warn = false) + public static Value simplePath(final Value graph) { + return simplePath(KIND, PAIR, Mode.SYMMETRIC, graph); + } + + @TLAPlusOperator(identifier = "AreConnectedIn", module = "UndirectedGraphs", warn = false) + public static Value areConnectedIn(final Value m, final Value n, final Value graph) { + return areConnectedIn(KIND, PAIR, Mode.SYMMETRIC, m, n, graph); + } + + /* + * 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 an edge. Self-loops (singleton edges) and edges with an endpoint + * outside the node set do not merge anything. + */ + @TLAPlusOperator(identifier = "ConnectedComponents", module = "UndirectedGraphs", warn = false) + public static Value connectedComponents(final Value graph) { + final RecordValue g = toGraph("ConnectedComponents", "first", KIND, graph); + final SetEnumValue nds = nodes(g); + final UnionFind comps = new UnionFind(nds.elements()); + + final ValueEnumeration ee = edges(g).elements(); + Value edge; + while ((edge = ee.nextElement()) != null) { + final Value[] e = PAIR.of(edge); + if (e == null) { + continue; + } + if (nds.member(e[0]) && nds.member(e[1])) { + comps.union(e[0], e[1]); + } + } + + // finally convert the UnionFind structure to a set of sets + final Map compSet = new LinkedHashMap<>(); + final ValueEnumeration ve = nds.elements(); + Value nd; + while ((nd = ve.nextElement()) != null) { + final Value rep = comps.find(nd); + if (compSet.containsKey(rep)) { + // add the current node to the component represented by rep + final SetEnumValue comp = compSet.get(rep); + compSet.put(rep, (SetEnumValue) comp.cup(new SetEnumValue(nd)).toSetEnum()); + } else { + // start a new component {nd} + compSet.put(rep, new SetEnumValue(nd)); + } + } + SetEnumValue result = new SetEnumValue(); + for (final SetEnumValue c : compSet.values()) { + result = (SetEnumValue) result.cup(new SetEnumValue(c)).toSetEnum(); + } + return result; + } + + /* + * Helper class: union-find algorithm, used for computing connected components. + */ + static final class UnionFind { + private final Map parent; // map every value to its parent + private int count; // number of components + + /* + * Initialize a new union-find structure containing all values in elts as + * singleton components. + */ + public UnionFind(final ValueEnumeration elts) { + parent = new LinkedHashMap<>(); + count = 0; + Value elt; + while ((elt = elts.nextElement()) != null) { + parent.put(elt, elt); // initially every element is its own parent + count++; + } + } + + /* + * Return the representative element of the component to which the element + * belongs. As a side effect, flatten the representation of the component. + */ + public Value find(final Value elt) { + if (!(parent.containsKey(elt))) { + throw new IllegalArgumentException("element not contained in UnionFind data structure: " + elt); + } + Value curr = elt; + while (true) { + final Value par = parent.get(curr); + if (par.equals(curr)) { + break; + } + curr = par; + } + final Value root = curr; + + curr = elt; + while (!curr.equals(root)) { + final Value par = parent.get(curr); + parent.put(curr, root); + curr = par; + } + + return root; + } + + /* + * Merge the components containing two elements. + */ + public void union(final Value elt1, final Value elt2) { + if (!(parent.containsKey(elt1)) || !(parent.containsKey(elt2))) { + throw new IllegalArgumentException( + "UnionFind data structure does not contain both " + elt1 + " and " + elt2); + } + + final Value par1 = find(elt1); + final Value par2 = find(elt2); + + if (!(par1.equals(par2))) { + // nothing to do if the elements already belong to the same component + parent.put(par2, par1); + count--; + } + } + } +} diff --git a/tests/AllTests.tla b/tests/AllTests.tla index 38b7ce2..8005e59 100644 --- a/tests/AllTests.tla +++ b/tests/AllTests.tla @@ -19,6 +19,7 @@ EXTENDS RelationTests, BagsExtTests, DyadicRationalsTests, StatisticsTests, + UndirectedGraphsTests, VectorClocksTests, GraphVizTests diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index 46c3aa6..f45ab9f 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -1,22 +1,205 @@ ------------------------- MODULE GraphsTests ------------------------- -EXTENDS Graphs, TLCExt +EXTENDS Graphs, SequencesExt, TLCExt ASSUME LET T == INSTANCE TLC IN T!PrintT("GraphsTests") +(******************************************************************************) +(* Pure TLA+ reference definitions, kept verbatim in sync with the operators *) +(* in modules/Graphs.tla. They serve as the oracle against which the Java *) +(* module overrides (SimplePath, AreConnectedIn, IsStronglyConnected) are *) +(* checked exhaustively below. ConnectionsIn (Warshall's algorithm) provides *) +(* a second, independent oracle for reachability. *) +(******************************************************************************) +LOCAL SimplePathPure(G) == + {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) : <> \in G.edge} + +LOCAL AreConnectedInPure(m, n, G) == + \E p \in SimplePathPure(G) : (p[1] = m) /\ (p[Len(p)] = n) + +LOCAL IsStronglyConnectedPure(G) == + \A m, n \in G.node : AreConnectedInPure(m, n, G) + +\* One representative graph set of each node-set cardinality 0 through 3 +\* (including the empty graph and self-loops). The operators treat nodes as +\* opaque values and are invariant under renaming, so a graph on nodes {1, 3} +\* or {2, 3} is just a relabeling of one on {1, 2} and adds no coverage. It +\* therefore suffices to use the prefixes {}, {1}, {1, 2}, {1, 2, 3} rather +\* than all same-cardinality node sets (e.g. Graphs({1, 3}), Graphs({2, 3})). +LOCAL SmallGraphs == + Graphs({}) \cup Graphs({1}) \cup Graphs({1, 2}) \cup Graphs({1, 2, 3}) + +(******************************************************************************) +(* A graph whose edge set is built via a set image that yields the same edge *) +(* multiple times, i.e. a potentially non-normalized SetEnumValue. The *) +(* overrides enumerate sets via SetEnumValue#elements(), which normalizes *) +(* (deduplicates), so the result is unaffected by the input representation. *) +(******************************************************************************) +LOCAL DupEdgeGraph == + [node |-> {1, 2, 3}, + edge |-> {<<2, 3>>} \cup { <<1, 2>> : i \in {"a", "b", "c"} }] + +ASSUME AssertEq(Cardinality(SimplePath(DupEdgeGraph)), 6) +ASSUME AssertEq(SimplePath(DupEdgeGraph), + {<<1>>, <<2>>, <<3>>, <<1, 2>>, <<2, 3>>, <<1, 2, 3>>}) + +(******************************************************************************) +(* The TLA+ definitions test membership of an exact 2-tuple <> *) +(* in G.edge, so an edge element that is not a 2-tuple (e.g. <> or *) +(* <>) matches nothing and contributes no edge. The overrides must *) +(* neither crash on 1-tuples nor read <> as the edge u -> v. *) +(******************************************************************************) +LOCAL OneTupleEdgeGraph == [node |-> {1, 2}, edge |-> {<<1>>, <<2>>}] +LOCAL ThreeTupleEdgeGraph == [node |-> {1, 2, 3}, edge |-> {<<1, 2, 3>>}] +LOCAL MixedArityEdgeGraph == + [node |-> {1, 2, 3}, edge |-> {<<1>>, <<1, 2>>, <<2, 3, 4>>}] + +\* 1-tuple edges are ignored: only the trivial single-node paths remain. +ASSUME AssertEq(SimplePath(OneTupleEdgeGraph), {<<1>>, <<2>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, OneTupleEdgeGraph), FALSE) +ASSUME AssertEq(IsStronglyConnected(OneTupleEdgeGraph), FALSE) + +\* A 3-tuple <<1, 2, 3>> is not the edge 1 -> 2 and is ignored. +ASSUME AssertEq(SimplePath(ThreeTupleEdgeGraph), {<<1>>, <<2>>, <<3>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, ThreeTupleEdgeGraph), FALSE) + +\* Only the genuine 2-tuple <<1, 2>> is treated as an edge. +ASSUME AssertEq(SimplePath(MixedArityEdgeGraph), {<<1>>, <<2>>, <<3>>, <<1, 2>>}) +ASSUME AssertEq(AreConnectedIn(1, 2, MixedArityEdgeGraph), TRUE) +ASSUME AssertEq(AreConnectedIn(2, 3, MixedArityEdgeGraph), FALSE) + +\* The overrides agree with the pure TLA+ definitions on these graphs. +ASSUME \A G \in {OneTupleEdgeGraph, ThreeTupleEdgeGraph, MixedArityEdgeGraph} : + /\ SimplePath(G) = SimplePathPure(G) + /\ \A m, n \in G.node : AreConnectedIn(m, n, G) = AreConnectedInPure(m, n, G) + /\ IsStronglyConnected(G) = IsStronglyConnectedPure(G) + +(******************************************************************************) +(* SimplePath Tests *) +(******************************************************************************) ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {}]), {}) ASSUME AssertEq(SimplePath([edge|-> {}, node |-> {1,2,3}]), {<<1>>, <<2>>, <<3>>}) ASSUME AssertEq(SimplePath([edge|-> {<<1,2>>, <<2,3>>}, node |-> {1,2,3}]), { <<1>>, <<2>>, <<3>>, <<1,2>>, <<2,3>>, <<1,2,3>> } ) +\* A self-loop never yields a path with a repeated node, so it does not add any +\* simple path beyond the single-node one. +ASSUME AssertEq(SimplePath([node |-> {1}, edge |-> {<<1, 1>>}]), {<<1>>}) +ASSUME AssertEq(SimplePath([node |-> {1, 2}, edge |-> {<<1, 1>>, <<1, 2>>}]), + {<<1>>, <<2>>, <<1, 2>>}) + +\* A 2-cycle contributes both directed edges as simple paths. +ASSUME AssertEq(SimplePath([node |-> {1, 2}, edge |-> {<<1, 2>>, <<2, 1>>}]), + {<<1>>, <<2>>, <<1, 2>>, <<2, 1>>}) + +\* A 3-cycle contributes every rotation as a simple path. +ASSUME AssertEq(SimplePath([node |-> {1, 2, 3}, edge |-> {<<1, 2>>, <<2, 3>>, <<3, 1>>}]), + {<<1>>, <<2>>, <<3>>, <<1, 2>>, <<2, 3>>, <<3, 1>>, + <<1, 2, 3>>, <<2, 3, 1>>, <<3, 1, 2>>}) + +\* Exhaustively: the Java override agrees with the original TLA+ definition for +\* every directed graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : AssertEq(SimplePath(g), SimplePathPure(g)) + +(******************************************************************************) +(* AreConnectedIn Tests *) +(******************************************************************************) ASSUME \A g \in Graphs({"A", "B", "C"}): \A u,v \in g.node : AreConnectedIn(u, v, g) \in BOOLEAN +\* A node is connected to itself iff it is a node of the graph (via <>). +ASSUME AssertEq(AreConnectedIn(1, 1, [node |-> {1}, edge |-> {}]), TRUE) +ASSUME AssertEq(AreConnectedIn(1, 1, EmptyGraph), FALSE) + +\* Connectivity is directed and requires both endpoints to be nodes of the graph. +ASSUME AssertEq(AreConnectedIn(1, 2, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), TRUE) +ASSUME AssertEq(AreConnectedIn(2, 1, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), FALSE) +ASSUME AssertEq(AreConnectedIn(1, 9, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), FALSE) + +\* Type-incompatible arguments must not be compared when no node matches: on the +\* empty graph the existential domain SimplePath(G) is empty, so the result is +\* FALSE (matching AreConnectedInPure) rather than a type error from m = n. +ASSUME AssertEq(AreConnectedIn(1, "x", EmptyGraph), FALSE) +ASSUME AssertEq(AreConnectedIn(1, "x", EmptyGraph), AreConnectedInPure(1, "x", EmptyGraph)) +ASSUME AssertEq(AreConnectedIn("x", "x", EmptyGraph), FALSE) + 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] +\* Exhaustively: the override agrees with the original TLA+ definition and with +\* the independent ConnectionsIn oracle for every graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : + \A m, n \in g.node : + /\ AreConnectedIn(m, n, g) = AreConnectedInPure(m, n, g) + /\ AreConnectedIn(m, n, g) <=> ConnectionsIn(g)[m, n] + +(******************************************************************************) +(* IsStronglyConnected Tests *) +(******************************************************************************) +ASSUME \A g \in Graphs({1, 2, 3}): IsStronglyConnected(g) \in BOOLEAN + +\* The empty graph is (vacuously) strongly connected. +ASSUME AssertEq(IsStronglyConnected(EmptyGraph), TRUE) + +\* A single node is strongly connected (a node is connected to itself via the +\* trivial path <>), with or without a self-loop. +ASSUME AssertEq(IsStronglyConnected([node |-> {1}, edge |-> {}]), TRUE) +ASSUME AssertEq(IsStronglyConnected([node |-> {1}, edge |-> {<<1, 1>>}]), TRUE) + +\* A simple directed cycle is strongly connected. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3}, + edge |-> {<<1, 2>>, <<2, 3>>, <<3, 1>>}]), TRUE) + +\* Two mutually connected nodes are strongly connected, ... +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2}, + edge |-> {<<1, 2>>, <<2, 1>>}]), TRUE) + +\* ... whereas a single directed edge between them is not. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2}, + edge |-> {<<1, 2>>}]), FALSE) + +\* A directed line (path graph) is not strongly connected. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3}, + edge |-> {<<1, 2>>, <<2, 3>>}]), FALSE) + +\* A graph with two separate strongly connected components is not strongly +\* connected as a whole. +ASSUME AssertEq(IsStronglyConnected([node |-> {1, 2, 3, 4}, + edge |-> {<<1, 2>>, <<2, 1>>, + <<3, 4>>, <<4, 3>>}]), FALSE) + +\* Exhaustively: the override agrees with the original TLA+ definition and with +\* the independent ConnectionsIn oracle for every graph in SmallGraphs. +ASSUME \A g \in SmallGraphs : + /\ IsStronglyConnected(g) = IsStronglyConnectedPure(g) + /\ IsStronglyConnected(g) <=> (\A m, n \in g.node : ConnectionsIn(g)[m, n]) + +(******************************************************************************) +(* Value identity Tests *) +(* *) +(* These tests use composite node values (sets) that are written with *) +(* different internal orderings but denote the same TLA+ value, so that nodes *) +(* and edge endpoints are matched by value equality rather than by their *) +(* concrete representation. *) +(******************************************************************************) +ASSUME LET G == [node |-> {{1, 2}, {3}}, edge |-> {<<{1, 2}, {3}>>}] + IN /\ AssertEq(SimplePath(G), {<<{1, 2}>>, <<{3}>>, <<{1, 2}, {3}>>}) + /\ AssertEq(AreConnectedIn({1, 2}, {3}, G), TRUE) + /\ AssertEq(AreConnectedIn({3}, {1, 2}, G), FALSE) + /\ AssertEq(IsStronglyConnected(G), FALSE) + +\* The edge endpoint {2, 1} and the node/argument {1, 2} denote the same set, so +\* the override must treat them as identical despite the differing literal order. +ASSUME LET G == [node |-> {{1, 2}, {3}}, edge |-> {<<{2, 1}, {3}>>, <<{3}, {1, 2}>>}] + IN /\ AssertEq(AreConnectedIn({1, 2}, {3}, G), TRUE) + /\ AssertEq(AreConnectedIn({3}, {2, 1}, G), TRUE) + /\ AssertEq(IsStronglyConnected(G), TRUE) + (******************************************************************************) (* GraphUnion Tests *) (******************************************************************************) @@ -137,7 +320,3 @@ ASSUME AssertEq(Leaves([node |-> {1, 2, 3}, edge |-> {<<1, 2>>, <<1, 3>>}]), {2, ASSUME AssertEq(Leaves([node |-> {1, 2}, edge |-> {<<1, 2>>, <<2, 1>>}]), {}) ===================================================================== -\* 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 \ No newline at end of file diff --git a/tests/UndirectedGraphsTests.tla b/tests/UndirectedGraphsTests.tla index 86dda82..3177895 100644 --- a/tests/UndirectedGraphsTests.tla +++ b/tests/UndirectedGraphsTests.tla @@ -1,24 +1,109 @@ -------------------------- MODULE UndirectedGraphsTests ------------------- -EXTENDS UndirectedGraphs, TLCExt +------------------------- MODULE UndirectedGraphsTests ----------------------- +EXTENDS UndirectedGraphs, SequencesExt, TLCExt ASSUME LET T == INSTANCE TLC IN T!PrintT("UndirectedGraphsTests") +(******************************************************************************) +(* Pure TLA+ reference definitions that can be evaluated by TLC and that *) +(* as oracles against which the module overrides (SimplePath, AreConnectedIn, *) +(* ConnectedComponents) are checked below. Note that these definitions are *) +(* correct only for graphs with a finite set of nodes. *) +(******************************************************************************) + +LOCAL SimplePathPure(G) == + {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} + +LOCAL ConnectedComponentsPure(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) == <> + 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) + +LOCAL AreConnectedInPure(m, n, G) == + \E comp \in ConnectedComponentsPure(G) : m \in comp /\ n \in comp + +\* Undirected graphs with one, two or three nodes. +LOCAL SmallGraphs == + UndirectedGraphs({}) \cup + UndirectedGraphs({1}) \cup + UndirectedGraphs({1,2}) \cup + UndirectedGraphs({1,2,3}) + +\* An undirected graph whose edge set is built via a set image that yields +\* the same edge multiple times: make sure the Java overrides work as expected. +LOCAL DupEdgeGraph == + [node |-> {1,2,3}, + edge |-> {{2,3}} \cup { {1,2} : i \in {"a", "b", "c"}}] + +\* An undirected graph containing "edges" that are sets containing +\* not exactly one or two elements or elements that are not nodes. +\* Such "edges" will be ignored by the Java overrides. +LOCAL MalformedGraph == + [node |-> {1,2,3}, + edge |-> { {}, {1}, {1,2}, {3,2,1}, {5,6}}] + +------------------------------------------------------------------------------ +(******************************************************************************) +(* SimplePath tests. *) +(******************************************************************************) + 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(SimplePath(DupEdgeGraph), + {<<1>>, <<2>>, <<3>>, <<1,2>>, <<2,1>>, <<2,3>>, <<3,2>>, <<1,2,3>>, <<3,2,1>>}) +ASSUME AssertEq(SimplePath(MalformedGraph), + {<<1>>, <<2>>, <<3>>, <<1,2>>, <<2,1>>}) +ASSUME \A g \in SmallGraphs : AssertEq(SimplePath(g), SimplePathPure(g)) -ASSUME AssertEq(ConnectedComponents([edge|-> {}, node |-> {}]), {}) +(******************************************************************************) +(* AreConnectedIn tests. *) +(******************************************************************************) ASSUME LET G == [edge|-> {{1,2}}, node |-> {1,2,3}] - IN /\ AssertEq(ConnectedComponents(G), {{1,2}, {3}}) - /\ AreConnectedIn(1, 2, G) + IN /\ AreConnectedIn(1, 2, G) /\ ~ AreConnectedIn(1, 3, G) -ASSUME AssertEq(ConnectedComponents([edge|-> {{1,2}}, node |-> {1,2,3}]), - {{1,2}, {3}}) +ASSUME \A m,n \in DupEdgeGraph.node : AreConnectedIn(m, n, DupEdgeGraph) + +ASSUME /\ AreConnectedIn(1, 2, MalformedGraph) + /\ ~ AreConnectedIn(3, 2, MalformedGraph) + +ASSUME \A g \in SmallGraphs : \A m,n \in g.node : + /\ AssertEq(AreConnectedIn(m, n, g), AreConnectedInPure(m, n, g)) + /\ AssertEq(AreConnectedIn(m, n, g), AreConnectedIn(n, m, g)) + +(******************************************************************************) +(* ConnectedComponents tests. *) +(******************************************************************************) +ASSUME AssertEq(ConnectedComponents([edge|-> {}, node |-> {}]), {}) + +ASSUME LET G == [edge|-> {{1,2}}, node |-> {1,2,3}] + IN AssertEq(ConnectedComponents(G), {{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) +ASSUME /\ AssertEq(ConnectedComponents(DupEdgeGraph), { {1,2,3} }) + /\ IsStronglyConnected(DupEdgeGraph) + +ASSUME /\ AssertEq(ConnectedComponents(MalformedGraph), { {1,2}, {3} }) + /\ ~ IsStronglyConnected(MalformedGraph) + +ASSUME \A g \in SmallGraphs : + AssertEq(ConnectedComponents(g), ConnectedComponentsPure(g)) + =====================================================================