From 45e83ab89cdc1840f15a7cf4a1f6fc69fa57c793 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Wed, 1 Jul 2026 19:00:04 +0200 Subject: [PATCH 01/15] several theorems about graphs Signed-off-by: Stephan Merz --- modules/GraphTheorems.tla | 209 +++++++ modules/GraphTheorems_proof.tla | 708 ++++++++++++++++++++++++ modules/Graphs.tla | 37 +- modules/Relation.tla | 4 + modules/SequencesExt.tla | 4 +- modules/SequencesExtTheorems.tla | 7 + modules/SequencesExtTheorems_proofs.tla | 14 + 7 files changed, 979 insertions(+), 4 deletions(-) create mode 100644 modules/GraphTheorems.tla create mode 100644 modules/GraphTheorems_proof.tla diff --git a/modules/GraphTheorems.tla b/modules/GraphTheorems.tla new file mode 100644 index 0000000..504db31 --- /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_proof.tla b/modules/GraphTheorems_proof.tla new file mode 100644 index 0000000..c3f14dc --- /dev/null +++ b/modules/GraphTheorems_proof.tla @@ -0,0 +1,708 @@ +---------------------- MODULE GraphTheorems_proof --------------------------- +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 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, Zenon +<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..d1a9a6a 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -1,9 +1,14 @@ ------------------------------- MODULE Graphs ------------------------------- +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] @@ -31,13 +36,26 @@ Path(G) == {p \in Seq(G.node) : SimplePath(G) == \* A simple path is a path with no repeated nodes. + { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } + +MCSimplePath(G) == + \* This alternative definition for finite graphs can be evaluated by TLC: add + \* SimplePath <- MCSimplePath + \* to the CONSTANTS section of the config file {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} AreConnectedIn(m, n, G) == - \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) + \* Two nodes are connected if there is a path from the first to the second one + \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) + +MCAreConnectedIn(m, n, G) == + \* This alternative definition is better suited for evaluation with TLC: add + \* AreConnectedIn <- MCAreConnectedIn + \* to the CONSTANTS section of the config file + \E p \in MCSimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) ConnectionsIn(G) == \* Compute a Boolean matrix that indicates, for each pair of nodes, @@ -58,13 +76,28 @@ ConnectionsIn(G) == IN C[G.node] IsStronglyConnected(G) == + \* A graph is strongly connected if all pairs of nodes are connected. \A m, n \in G.node : AreConnectedIn(m, n, G) + +MCIsStronglyConnected(G) == + \* Alternative definition better suited for evaluation with TLC: add + \* IsStronglyConnected <- MCIsStronglyConnected + \* to the CONSTANTS section of the configuration file + LET Cs == ConnectionsIn(G) + IN \A m,n \in G.node : Cs[m,n] + ----------------------------------------------------------------------------- IsTreeWithRoot(G, r) == + \* A tree is a directed graph (with edges pointing towards the root) such that: + \* (i) the graph contains the root, + \* (ii) every node has a single parent, + \* (iii) every node is connected to the root. /\ 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/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..13b89ab 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. *) (*************************************************************************) diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla index a04ddbd..a5955e7 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 *) diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla index 3c4700c..f25ad68 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 *) From 7e67a802479e6f353b9b461bf94a52f2d3105a27 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Wed, 1 Jul 2026 19:17:07 +0200 Subject: [PATCH 02/15] rename operators in tests for graphs Signed-off-by: Stephan Merz --- tests/GraphsTests.tla | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index 46c3aa6..5d22482 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -3,19 +3,19 @@ EXTENDS Graphs, TLCExt ASSUME LET T == INSTANCE TLC IN T!PrintT("GraphsTests") -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}]), +ASSUME AssertEq(MCSimplePath([edge|-> {}, node |-> {}]), {}) +ASSUME AssertEq(MCSimplePath([edge|-> {}, node |-> {1,2,3}]), {<<1>>, <<2>>, <<3>>}) +ASSUME AssertEq(MCSimplePath([edge|-> {<<1,2>>, <<2,3>>}, node |-> {1,2,3}]), { <<1>>, <<2>>, <<3>>, <<1,2>>, <<2,3>>, <<1,2,3>> } ) ASSUME \A g \in Graphs({"A", "B", "C"}): \A u,v \in g.node : - AreConnectedIn(u, v, g) \in BOOLEAN + MCAreConnectedIn(u, v, g) \in BOOLEAN ASSUME LET G == [node |-> {1,2,3,4,5,6}, edge |-> {<<1,2>>, <<2,3>>, <<2,4>>, <<3,2>>, <<3,4>>, <<3,5>>, <<4,2>>, <<5,6>>, <<6,5>>}] - IN \A m,n \in G.node : AreConnectedIn(m,n,G) <=> ConnectionsIn(G)[m,n] + IN \A m,n \in G.node : MCAreConnectedIn(m,n,G) <=> ConnectionsIn(G)[m,n] (******************************************************************************) (* GraphUnion Tests *) From a7d55df940f95125d0d9da20624ba404be11790a Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 2 Jul 2026 08:57:24 +0200 Subject: [PATCH 03/15] rename proofs module so that it will be picked up by CI Signed-off-by: Stephan Merz --- modules/{GraphTheorems_proof.tla => GraphTheorems_proofs.tla} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename modules/{GraphTheorems_proof.tla => GraphTheorems_proofs.tla} (100%) diff --git a/modules/GraphTheorems_proof.tla b/modules/GraphTheorems_proofs.tla similarity index 100% rename from modules/GraphTheorems_proof.tla rename to modules/GraphTheorems_proofs.tla From b76466a334aaa315a0e2e8d8a8d502121812e42d Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 2 Jul 2026 09:36:04 +0200 Subject: [PATCH 04/15] fix two proof steps that appear to be shaky in the CI check Signed-off-by: Stephan Merz --- modules/GraphTheorems_proofs.tla | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/modules/GraphTheorems_proofs.tla b/modules/GraphTheorems_proofs.tla index c3f14dc..9739c85 100644 --- a/modules/GraphTheorems_proofs.tla +++ b/modules/GraphTheorems_proofs.tla @@ -1,4 +1,4 @@ ----------------------- MODULE GraphTheorems_proof --------------------------- +---------------------- MODULE GraphTheorems_proofs -------------------------- EXTENDS Graphs, Integers, FunctionTheorems, FiniteSetTheorems, SequencesExtTheorems, FiniteSetsExt, FiniteSetsExtTheorems, TLAPS @@ -245,7 +245,7 @@ THEOREM ExistsPathIffExistsSimplePath == <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 DEF Surjection + 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 @@ -559,7 +559,7 @@ THEOREM RemoveLeafFromTree == T == G.node \ S E == G.edge \cap (T \X T) <1>2. IsTreeWithRoot([node |-> T, edge |-> E], r) - BY <1>1, RemoveSubtree, Zenon + BY <1>1, RemoveSubtree, IsaM("blast") <1>3. S = {leaf} <2>1. leaf \in S BY ConnectedReflexive From ca8e433997f18e3576ed238bbecad5232ca27099 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 8 Jul 2026 11:06:10 -0700 Subject: [PATCH 05/15] Add tests for Graphs SimplePath, AreConnectedIn and IsStronglyConnected Check the operators exhaustively against their pure TLA+ definitions and the ConnectionsIn oracle over all graphs on up to three nodes, plus edge cases (self-loops, arguments outside the node set, composite/non-normalized node values). [Tests] Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- tests/GraphsTests.tla | 147 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 146 insertions(+), 1 deletion(-) diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index 46c3aa6..29e198b 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -1,22 +1,167 @@ ------------------------- 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>>}) + +(******************************************************************************) +(* 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) + 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 *) (******************************************************************************) From dac980822793a0597b66209338311ec65d9532b3 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 8 Jul 2026 11:52:25 -0700 Subject: [PATCH 06/15] Add Graphs module overrides for SimplePath, AreConnectedIn and IsStronglyConnected Register three Java overrides in TLCOverrides. SimplePath enumerates simple paths via DFS instead of materializing SeqOf(node, Cardinality(node)); AreConnectedIn and IsStronglyConnected use BFS (the latter forward and on the transpose) rather than the quadratic all-pairs pure-TLA+ definitions. The overrides cut GraphsTests (exhaustive checks over all graphs on up to four nodes `\cup Graphs({1, 2, 3})`) from ~15 to ~5 minutes. TLC's code is not reused: its only Value-based graph algorithm, TransitiveClosure.Warshall, is non-reflexive, drops isolated nodes and is O(V^3), so it fits none of these operators. [TLC] Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- modules/tlc2/overrides/Graphs.java | 256 +++++++++++++++++++++++ modules/tlc2/overrides/TLCOverrides.java | 4 +- tests/GraphsTests.tla | 38 ++++ 3 files changed, 296 insertions(+), 2 deletions(-) create mode 100644 modules/tlc2/overrides/Graphs.java diff --git a/modules/tlc2/overrides/Graphs.java b/modules/tlc2/overrides/Graphs.java new file mode 100644 index 0000000..015d6ee --- /dev/null +++ b/modules/tlc2/overrides/Graphs.java @@ -0,0 +1,256 @@ +/******************************************************************************* + * 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.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; + +public final class Graphs { + + private Graphs() { + // no-instantiation! + } + + private static final StringValue NODE = new StringValue("node"); + private static final StringValue EDGE = new StringValue("edge"); + + /* + * 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. + */ + private static RecordValue toGraph(final String op, final String argPos, final Value v) { + final Value rcd = v.toRcd(); + if (!(rcd instanceof RecordValue)) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record with a node and an edge field", Values.ppr(v.toString()) }); + } + final RecordValue g = (RecordValue) rcd; + final Value node = g.select(NODE); + if (node == null || node.toSetEnum() == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record whose node field is a set", Values.ppr(v.toString()) }); + } + final Value edge = g.select(EDGE); + if (edge == null || edge.toSetEnum() == null) { + throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, + new String[] { argPos, op, "graph record whose edge field is a set", Values.ppr(v.toString()) }); + } + return g; + } + + private static SetEnumValue nodes(final RecordValue g) { + final SetEnumValue nodes = (SetEnumValue) g.select(NODE).toSetEnum(); + nodes.normalize(); + return nodes; + } + + /* + * 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. + * + * 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 Map> adjacency(final RecordValue g, final SetEnumValue nodes, + final boolean transpose) { + final SetEnumValue edges = (SetEnumValue) g.select(EDGE).toSetEnum(); + final Map> adj = new HashMap<>(); + final ValueEnumeration ve = edges.elements(); + Value v; + while ((v = ve.nextElement()) != null) { + final Value tuple = v.toTuple(); + if (!(tuple instanceof TupleValue) || ((TupleValue) tuple).size() != 2) { + continue; + } + final TupleValue e = (TupleValue) tuple; + Value from = e.elems[0]; + Value to = e.elems[1]; + if (transpose) { + final Value tmp = from; + from = to; + to = tmp; + } + if (nodes.member(from) && nodes.member(to)) { + adj.computeIfAbsent(from, k -> new ArrayList<>()).add(to); + } + } + return adj; + } + + /* + * SimplePath(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} + * + * Enumerates the set of all (non-empty) simple paths of G via depth-first + * search. This avoids materializing the (exponentially large) set + * SeqOf(G.node, Cardinality(G.node)) that the pure TLA+ definition ranges over. + */ + @TLAPlusOperator(identifier = "SimplePath", module = "Graphs", warn = false) + public static Value simplePath(final Value graph) { + final RecordValue g = toGraph("SimplePath", "first", graph); + final SetEnumValue nodes = nodes(g); + final Map> adj = adjacency(g, nodes, false); + + 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. + private static void extendSimplePath(final Value current, final Map> adj, + final List path, final Set visited, final List paths) { + // Every non-empty prefix of a simple path is itself a simple path. + 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 SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) + * + * There is a simple (hence any) directed path from m to n. Note that <> is a + * simple path, so a node is connected to itself iff it is a node of G. + */ + @TLAPlusOperator(identifier = "AreConnectedIn", module = "Graphs", warn = false) + public static Value areConnectedIn(final Value m, final Value n, final Value graph) { + final RecordValue g = toGraph("AreConnectedIn", "third", graph); + final SetEnumValue nodes = nodes(g); + + // Every node on a simple 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 SimplePath(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, false); + return reachable(m, adj).contains(n) ? BoolValue.ValTrue : BoolValue.ValFalse; + } + + // Breadth-first search returning all nodes reachable from source (inclusive). + private 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; + } + + /* + * 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", 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, false); + if (reachable(root, adj).size() != order) { + return BoolValue.ValFalse; + } + + final Map> radj = adjacency(g, nodes, true); + 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..aff1ca5 100644 --- a/modules/tlc2/overrides/TLCOverrides.java +++ b/modules/tlc2/overrides/TLCOverrides.java @@ -45,7 +45,7 @@ public Class[] get() { Json.resolves(); return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Json.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, - DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class }; + DyadicRationals.class, Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class }; } catch (NoClassDefFoundError e) { // Remove this catch when this Class is moved to `TLC`. System.out.println("gson dependencies of Json overrides not found, Json module won't work unless " @@ -53,6 +53,6 @@ public Class[] get() { } return new Class[] { IOUtils.class, SVG.class, SequencesExt.class, Bitwise.class, FiniteSetsExt.class, Functions.class, CSV.class, Combinatorics.class, BagsExt.class, DyadicRationals.class, - Statistics.class, VectorClocks.class, GraphViz.class }; + Statistics.class, VectorClocks.class, GraphViz.class, Graphs.class }; } } diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index 29e198b..f7b225f 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -45,6 +45,37 @@ 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 *) (******************************************************************************) @@ -88,6 +119,13 @@ ASSUME AssertEq(AreConnectedIn(1, 2, [node |-> {1, 2}, edge |-> {<<1, 2>>}]), TR 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>>}] From 7b0e76cd33b76032148367d9fe9a0da54a417406 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Tue, 14 Jul 2026 00:01:59 -0700 Subject: [PATCH 07/15] Towards a TLAPS stdlib (#127) * Theorems about Contains and majority supersets Add and prove membership theorems for SequencesExt!Contains (empty/Append/Cons/Concat/Tail/singleton plus heterogeneous-type Append/Concat variants) and SupersetOfMajorityIsMajority for FiniteSetsExt. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe * IsSorted operator and sortedness theorems Add SequencesExt!IsSorted(s, op(_,_)), which holds iff s is sorted with respect to an arbitrary binary relation op, with a formal doc comment and examples. Add and prove the accompanying theorems SortedEmpty, SortedSingleton, SortedAppend, SortedConcat, SortedInjective and SortedSubSeq, whose order hypotheses on op (transitivity, irreflexivity) are stated locally so they apply to any relation. All obligations checked with TLAPS. Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe * theorems about sequences, finite sets, and quorum systems Signed-off-by: Stephan Merz * fixing two apparently brittle proofs Signed-off-by: Stephan Merz * align theorem statements in SequencesExtTheorems with those in the _proofs module Signed-off-by: Stephan Merz --------- Signed-off-by: Markus Alexander Kuppe Signed-off-by: Stephan Merz Co-authored-by: Claude Opus 4.8 Co-authored-by: Stephan Merz --- modules/FiniteSetsExtTheorems.tla | 18 ++++ modules/FiniteSetsExtTheorems_proofs.tla | 16 ++++ modules/Quorum.tla | 19 +++++ modules/QuorumTheorems.tla | 26 ++++++ modules/QuorumTheorems_proofs.tla | 29 +++++++ modules/SequencesExt.tla | 25 ++++++ modules/SequencesExtTheorems.tla | 91 ++++++++++++++++++++ modules/SequencesExtTheorems_proofs.tla | 102 +++++++++++++++++++++++ 8 files changed, 326 insertions(+) create mode 100644 modules/Quorum.tla create mode 100644 modules/QuorumTheorems.tla create mode 100644 modules/QuorumTheorems_proofs.tla 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/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/SequencesExt.tla b/modules/SequencesExt.tla index bb4a14d..28679e7 100644 --- a/modules/SequencesExt.tla +++ b/modules/SequencesExt.tla @@ -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..9462873 100644 --- a/modules/SequencesExtTheorems.tla +++ b/modules/SequencesExtTheorems.tla @@ -47,6 +47,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..5db8707 100644 --- a/modules/SequencesExtTheorems_proofs.tla +++ b/modules/SequencesExtTheorems_proofs.tla @@ -79,6 +79,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) == *) From e381d19932e2cc6d2fe0cad2be3e97d684c20f8c Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Wed, 1 Jul 2026 19:00:04 +0200 Subject: [PATCH 08/15] several theorems about graphs Signed-off-by: Stephan Merz --- modules/GraphTheorems.tla | 209 +++++++ modules/GraphTheorems_proof.tla | 708 ++++++++++++++++++++++++ modules/Graphs.tla | 37 +- modules/Relation.tla | 4 + modules/SequencesExt.tla | 4 +- modules/SequencesExtTheorems.tla | 7 + modules/SequencesExtTheorems_proofs.tla | 14 + 7 files changed, 979 insertions(+), 4 deletions(-) create mode 100644 modules/GraphTheorems.tla create mode 100644 modules/GraphTheorems_proof.tla diff --git a/modules/GraphTheorems.tla b/modules/GraphTheorems.tla new file mode 100644 index 0000000..504db31 --- /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_proof.tla b/modules/GraphTheorems_proof.tla new file mode 100644 index 0000000..c3f14dc --- /dev/null +++ b/modules/GraphTheorems_proof.tla @@ -0,0 +1,708 @@ +---------------------- MODULE GraphTheorems_proof --------------------------- +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 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, Zenon +<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..d1a9a6a 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -1,9 +1,14 @@ ------------------------------- MODULE Graphs ------------------------------- +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] @@ -31,13 +36,26 @@ Path(G) == {p \in Seq(G.node) : SimplePath(G) == \* A simple path is a path with no repeated nodes. + { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } + +MCSimplePath(G) == + \* This alternative definition for finite graphs can be evaluated by TLC: add + \* SimplePath <- MCSimplePath + \* to the CONSTANTS section of the config file {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} AreConnectedIn(m, n, G) == - \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) + \* Two nodes are connected if there is a path from the first to the second one + \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) + +MCAreConnectedIn(m, n, G) == + \* This alternative definition is better suited for evaluation with TLC: add + \* AreConnectedIn <- MCAreConnectedIn + \* to the CONSTANTS section of the config file + \E p \in MCSimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) ConnectionsIn(G) == \* Compute a Boolean matrix that indicates, for each pair of nodes, @@ -58,13 +76,28 @@ ConnectionsIn(G) == IN C[G.node] IsStronglyConnected(G) == + \* A graph is strongly connected if all pairs of nodes are connected. \A m, n \in G.node : AreConnectedIn(m, n, G) + +MCIsStronglyConnected(G) == + \* Alternative definition better suited for evaluation with TLC: add + \* IsStronglyConnected <- MCIsStronglyConnected + \* to the CONSTANTS section of the configuration file + LET Cs == ConnectionsIn(G) + IN \A m,n \in G.node : Cs[m,n] + ----------------------------------------------------------------------------- IsTreeWithRoot(G, r) == + \* A tree is a directed graph (with edges pointing towards the root) such that: + \* (i) the graph contains the root, + \* (ii) every node has a single parent, + \* (iii) every node is connected to the root. /\ 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/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 28679e7..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. *) (*************************************************************************) diff --git a/modules/SequencesExtTheorems.tla b/modules/SequencesExtTheorems.tla index 9462873..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 *) diff --git a/modules/SequencesExtTheorems_proofs.tla b/modules/SequencesExtTheorems_proofs.tla index 5db8707..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 *) From 3019bc3a07ac7984fd1c7f13e91a5f7340847424 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Wed, 1 Jul 2026 19:17:07 +0200 Subject: [PATCH 09/15] rename operators in tests for graphs Signed-off-by: Stephan Merz --- tests/GraphsTests.tla | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/tests/GraphsTests.tla b/tests/GraphsTests.tla index f7b225f..9534205 100644 --- a/tests/GraphsTests.tla +++ b/tests/GraphsTests.tla @@ -108,7 +108,7 @@ ASSUME \A g \in SmallGraphs : AssertEq(SimplePath(g), SimplePathPure(g)) (******************************************************************************) ASSUME \A g \in Graphs({"A", "B", "C"}): \A u,v \in g.node : - AreConnectedIn(u, v, g) \in BOOLEAN + MCAreConnectedIn(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) @@ -129,7 +129,7 @@ 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] + IN \A m,n \in G.node : MCAreConnectedIn(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. @@ -320,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 From ee0bb01f569c09b987b20608d08e5a105f8b6361 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 2 Jul 2026 08:57:24 +0200 Subject: [PATCH 10/15] rename proofs module so that it will be picked up by CI Signed-off-by: Stephan Merz --- modules/{GraphTheorems_proof.tla => GraphTheorems_proofs.tla} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename modules/{GraphTheorems_proof.tla => GraphTheorems_proofs.tla} (100%) diff --git a/modules/GraphTheorems_proof.tla b/modules/GraphTheorems_proofs.tla similarity index 100% rename from modules/GraphTheorems_proof.tla rename to modules/GraphTheorems_proofs.tla From 9501bcd88e10bcdc55ba77e09c8b51124bc567af Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Thu, 2 Jul 2026 09:36:04 +0200 Subject: [PATCH 11/15] fix two proof steps that appear to be shaky in the CI check Signed-off-by: Stephan Merz --- modules/GraphTheorems_proofs.tla | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/modules/GraphTheorems_proofs.tla b/modules/GraphTheorems_proofs.tla index c3f14dc..9739c85 100644 --- a/modules/GraphTheorems_proofs.tla +++ b/modules/GraphTheorems_proofs.tla @@ -1,4 +1,4 @@ ----------------------- MODULE GraphTheorems_proof --------------------------- +---------------------- MODULE GraphTheorems_proofs -------------------------- EXTENDS Graphs, Integers, FunctionTheorems, FiniteSetTheorems, SequencesExtTheorems, FiniteSetsExt, FiniteSetsExtTheorems, TLAPS @@ -245,7 +245,7 @@ THEOREM ExistsPathIffExistsSimplePath == <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 DEF Surjection + 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 @@ -559,7 +559,7 @@ THEOREM RemoveLeafFromTree == T == G.node \ S E == G.edge \cap (T \X T) <1>2. IsTreeWithRoot([node |-> T, edge |-> E], r) - BY <1>1, RemoveSubtree, Zenon + BY <1>1, RemoveSubtree, IsaM("blast") <1>3. S = {leaf} <2>1. leaf \in S BY ConnectedReflexive From 94c8ae414724a5561bdce39ebddb5d8a346a29c0 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Fri, 17 Jul 2026 16:24:14 +0200 Subject: [PATCH 12/15] minor changes Signed-off-by: Stephan Merz --- modules/UndirectedGraphs.tla | 32 ++++++++++++++++---------------- tests/UndirectedGraphsTests.tla | 3 ++- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/modules/UndirectedGraphs.tla b/modules/UndirectedGraphs.tla index 3af7556..803adfd 100644 --- a/modules/UndirectedGraphs.tla +++ b/modules/UndirectedGraphs.tla @@ -44,24 +44,21 @@ AreConnectedIn(m, n, G) == ----------------------------------------------------------------------------- (****************************************************************************) -(* A non-empty set S of nodes is a connected component if any two nodes in *) -(* S are connected by a path that only visits nodes in S. *) -(* NB: This definition does not enforce that the component is maximal. *) -(* The (maximal) connected components are the maximal subsets of nodes that *) -(* are connected. *) +(* 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. *) (****************************************************************************) -IsConnectedComponent(S, G) == - /\ S # {} - /\ \A m,n \in S : \E p \in Path(G) : - /\ p[1] = m /\ p[Len(p)] = n - /\ Range(p) \subseteq S - ConnectedComponents(G) == \* NB: TLC uses a Java override for this operator. - { S \in SUBSET G.node : - /\ IsConnectedComponent(S, G) - /\ \A T \in (SUBSET S) \ {S} : ~ IsConnectedComponent(T, 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 S) \ {S} : ~ IsCC(T) + } IsStronglyConnected(G) == Cardinality(ConnectedComponents(G)) = 1 @@ -75,7 +72,10 @@ IsStronglyConnected(G) == (* [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,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/tests/UndirectedGraphsTests.tla b/tests/UndirectedGraphsTests.tla index 971730a..3177895 100644 --- a/tests/UndirectedGraphsTests.tla +++ b/tests/UndirectedGraphsTests.tla @@ -6,7 +6,8 @@ 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. *) +(* ConnectedComponents) are checked below. Note that these definitions are *) +(* correct only for graphs with a finite set of nodes. *) (******************************************************************************) LOCAL SimplePathPure(G) == From 837b16fbfa722fb200c902a2378ddcfb40324578 Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Fri, 17 Jul 2026 20:17:26 +0200 Subject: [PATCH 13/15] make SCCs maximal Signed-off-by: Stephan Merz --- modules/UndirectedGraphs.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/modules/UndirectedGraphs.tla b/modules/UndirectedGraphs.tla index 803adfd..f576bbf 100644 --- a/modules/UndirectedGraphs.tla +++ b/modules/UndirectedGraphs.tla @@ -57,7 +57,7 @@ ConnectedComponents(G) == /\ \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 S) \ {S} : ~ IsCC(T) + /\ \A T \in SUBSET G.node : S \subseteq T /\ S # T => ~ IsCC(T) } IsStronglyConnected(G) == From 5b5f16a126cb59316d2d3b5ed027db6c5d342fe4 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 17 Jul 2026 17:12:31 -0700 Subject: [PATCH 14/15] Add AbstractGraphs class to share implementation between directed and undirected graph modules Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- modules/tlc2/overrides/AbstractGraphs.java | 261 +++++++++++++++++ modules/tlc2/overrides/Graphs.java | 193 ++----------- modules/tlc2/overrides/UndirectedGraphs.java | 284 ++++--------------- 3 files changed, 342 insertions(+), 396 deletions(-) create mode 100644 modules/tlc2/overrides/AbstractGraphs.java 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 index 015d6ee..73d11e6 100644 --- a/modules/tlc2/overrides/Graphs.java +++ b/modules/tlc2/overrides/Graphs.java @@ -25,213 +25,66 @@ ******************************************************************************/ 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; -public final class Graphs { +/* + * 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 StringValue NODE = new StringValue("node"); - private static final StringValue EDGE = new StringValue("edge"); + private static final String KIND = "graph"; /* - * 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. - */ - private static RecordValue toGraph(final String op, final String argPos, final Value v) { - final Value rcd = v.toRcd(); - if (!(rcd instanceof RecordValue)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "graph record with a node and an edge field", Values.ppr(v.toString()) }); - } - final RecordValue g = (RecordValue) rcd; - final Value node = g.select(NODE); - if (node == null || node.toSetEnum() == null) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "graph record whose node field is a set", Values.ppr(v.toString()) }); - } - final Value edge = g.select(EDGE); - if (edge == null || edge.toSetEnum() == null) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "graph record whose edge field is a set", Values.ppr(v.toString()) }); - } - return g; - } - - private static SetEnumValue nodes(final RecordValue g) { - final SetEnumValue nodes = (SetEnumValue) g.select(NODE).toSetEnum(); - nodes.normalize(); - return nodes; - } - - /* - * 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. - * * 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 + * 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 Map> adjacency(final RecordValue g, final SetEnumValue nodes, - final boolean transpose) { - final SetEnumValue edges = (SetEnumValue) g.select(EDGE).toSetEnum(); - final Map> adj = new HashMap<>(); - final ValueEnumeration ve = edges.elements(); - Value v; - while ((v = ve.nextElement()) != null) { - final Value tuple = v.toTuple(); - if (!(tuple instanceof TupleValue) || ((TupleValue) tuple).size() != 2) { - continue; - } - final TupleValue e = (TupleValue) tuple; - Value from = e.elems[0]; - Value to = e.elems[1]; - if (transpose) { - final Value tmp = from; - from = to; - to = tmp; - } - if (nodes.member(from) && nodes.member(to)) { - adj.computeIfAbsent(from, k -> new ArrayList<>()).add(to); - } + private static final Endpoints TUPLE = edge -> { + final Value tuple = edge.toTuple(); + if (!(tuple instanceof TupleValue) || ((TupleValue) tuple).size() != 2) { + return null; } - return adj; - } + final TupleValue e = (TupleValue) tuple; + return new Value[] { e.elems[0], e.elems[1] }; + }; - /* - * SimplePath(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} - * - * Enumerates the set of all (non-empty) simple paths of G via depth-first - * search. This avoids materializing the (exponentially large) set - * SeqOf(G.node, Cardinality(G.node)) that the pure TLA+ definition ranges over. - */ @TLAPlusOperator(identifier = "SimplePath", module = "Graphs", warn = false) public static Value simplePath(final Value graph) { - final RecordValue g = toGraph("SimplePath", "first", graph); - final SetEnumValue nodes = nodes(g); - final Map> adj = adjacency(g, nodes, false); - - 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); + return simplePath(KIND, TUPLE, Mode.FORWARD, graph); } - // Backtracking depth-first search: emit the current path, then recurse into - // each unvisited successor. - private static void extendSimplePath(final Value current, final Map> adj, - final List path, final Set visited, final List paths) { - // Every non-empty prefix of a simple path is itself a simple path. - 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 SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) - * - * There is a simple (hence any) directed path from m to n. Note that <> is a - * simple path, so a node is connected to itself iff it is a node of G. - */ @TLAPlusOperator(identifier = "AreConnectedIn", module = "Graphs", warn = false) public static Value areConnectedIn(final Value m, final Value n, final Value graph) { - final RecordValue g = toGraph("AreConnectedIn", "third", graph); - final SetEnumValue nodes = nodes(g); - - // Every node on a simple 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 SimplePath(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, false); - return reachable(m, adj).contains(n) ? BoolValue.ValTrue : BoolValue.ValFalse; - } - - // Breadth-first search returning all nodes reachable from source (inclusive). - private 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; + return areConnectedIn(KIND, TUPLE, Mode.FORWARD, m, n, graph); } /* - * IsStronglyConnected(G) == - * \A m, n \in G.node : AreConnectedIn(m, n, G) + * 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 + * 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", graph); + final RecordValue g = toGraph("IsStronglyConnected", "first", KIND, graph); final SetEnumValue nodes = nodes(g); final int order = nodes.size(); @@ -241,12 +94,12 @@ public static Value isStronglyConnected(final Value graph) { final Value root = nodes.elements().nextElement(); - final Map> adj = adjacency(g, nodes, false); + final Map> adj = adjacency(g, nodes, TUPLE, Mode.FORWARD); if (reachable(root, adj).size() != order) { return BoolValue.ValFalse; } - final Map> radj = adjacency(g, nodes, true); + final Map> radj = adjacency(g, nodes, TUPLE, Mode.TRANSPOSE); if (reachable(root, radj).size() != order) { return BoolValue.ValFalse; } diff --git a/modules/tlc2/overrides/UndirectedGraphs.java b/modules/tlc2/overrides/UndirectedGraphs.java index bab1ba3..d56c50e 100644 --- a/modules/tlc2/overrides/UndirectedGraphs.java +++ b/modules/tlc2/overrides/UndirectedGraphs.java @@ -25,297 +25,129 @@ ******************************************************************************/ 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.LinkedHashMap; -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; -public final class UndirectedGraphs { +/* + * 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 StringValue NODE = new StringValue("node"); - private static final StringValue EDGE = new StringValue("edge"); + private static final String KIND = "undirected graph"; /* - * 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 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 RecordValue toGraph(final String op, final String argPos, final Value v) { - final Value rcd = v.toRcd(); - if (!(rcd instanceof RecordValue)) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "undirected graph record with a node and an edge field", Values.ppr(v.toString()) }); + private static final Endpoints PAIR = edge -> { + final Value set = edge.toSetEnum(); + if (!(set instanceof SetEnumValue)) { + return null; } - final RecordValue g = (RecordValue) rcd; - final Value node = g.select(NODE); - if (node == null || node.toSetEnum() == null) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "undirected graph record whose node field is a set", Values.ppr(v.toString()) }); + final SetEnumValue e = (SetEnumValue) set; + if ((e.size() == 0) || (e.size() > 2)) { + return null; } - final Value edge = g.select(EDGE); - if (edge == null || edge.toSetEnum() == null) { - throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, - new String[] { argPos, op, "undirected graph record whose edge field is a set", Values.ppr(v.toString()) }); - } - return g; - } - - private static SetEnumValue nodes(final RecordValue g) { - final SetEnumValue nodes = (SetEnumValue) g.select(NODE).toSetEnum(); - nodes.normalize(); - return nodes; - } - - private static SetEnumValue edges(final RecordValue g) { - final SetEnumValue edges = (SetEnumValue) g.select(EDGE).toSetEnum(); - edges.normalize(); - return edges; - } + final ValueEnumeration ne = e.elements(); + final Value from = ne.nextElement(); + final Value to = ne.nextElement(); + return new Value[] { from, to == null ? from : to }; + }; - /* - * 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. - * - * The definitions test {p[i], p[i+1]} \in G.edge. - * 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 rather than mis-parsed or causing an out-of-bounds error. - */ - private static Map> adjacency(final RecordValue g, final SetEnumValue nodes) { - final Map> adj = new HashMap<>(); - final ValueEnumeration ve = edges(g).elements(); - Value v; - while ((v = ve.nextElement()) != null) { - final Value set = v.toSetEnum(); - if ((set == null) || !(set instanceof SetEnumValue)) { - continue; - } - final SetEnumValue e = (SetEnumValue) set; - if ((e.size() == 0) || (e.size() > 2)) { - continue; - } - ValueEnumeration ne = e.elements(); - Value from = ne.nextElement(); - Value to = ne.nextElement(); - if (to == null) { - to = from; - } - if (nodes.member(from) && nodes.member(to)) { - // add the edges in both directions to enforce symmetry - adj.computeIfAbsent(from, k -> new ArrayList<>()).add(to); - if (from != to) { - adj.computeIfAbsent(to, k -> new ArrayList<>()).add(from); - } - } - } - return adj; - } - - /* - * SimplePath(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} - * - * Enumerates the set of all (non-empty) simple paths of G via depth-first - * search. This avoids materializing the (exponentially large) set - * SeqOf(G.node, Cardinality(G.node)) that the pure TLA+ definition ranges over. - */ @TLAPlusOperator(identifier = "SimplePath", module = "UndirectedGraphs", warn = false) public static Value simplePath(final Value graph) { - final RecordValue g = toGraph("SimplePath", "first", graph); - final SetEnumValue nodes = nodes(g); - final Map> adj = adjacency(g, nodes); - - 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. - private static void extendSimplePath(final Value current, final Map> adj, - final List path, final Set visited, final List paths) { - // Every non-empty prefix of a simple path is itself a simple path. - 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); - } - } + return simplePath(KIND, PAIR, Mode.SYMMETRIC, graph); } - /* - * AreConnectedIn(m, n, G) == - * \E p \in SimplePath(G) : (p[1] = m) /\ (p[Len(p)] = n) - * - * There is a simple (hence any) directed path from m to n. Note that <> is a - * simple path, so a node is connected to itself iff it is a node of G. - */ @TLAPlusOperator(identifier = "AreConnectedIn", module = "UndirectedGraphs", warn = false) public static Value areConnectedIn(final Value m, final Value n, final Value graph) { - final RecordValue g = toGraph("AreConnectedIn", "third", graph); - final SetEnumValue nodes = nodes(g); - - // Every node on a simple 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 SimplePath(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); - return reachable(m, adj).contains(n) ? BoolValue.ValTrue : BoolValue.ValFalse; - } - - // Breadth-first search returning all nodes reachable from source (inclusive). - private 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; + return areConnectedIn(KIND, PAIR, Mode.SYMMETRIC, m, n, graph); } /* - * Compute the strongly 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. + * 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", 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 set = edge.toSetEnum(); - // ignore any "edges" that are not sets - if ((set == null) || !(set instanceof SetEnumValue)) { + final Value[] e = PAIR.of(edge); + if (e == null) { continue; } - final SetEnumValue e = (SetEnumValue) set; - if (e.size() == 2) { - // ignore singletons because doesn't merge any components - final ValueEnumeration ve = e.elements(); - final Value from = ve.nextElement(); - final Value to = ve.nextElement(); - if (nds.member(from) && nds.member(to)) { - // ignore any "edges" that do not relate two nodes - comps.union(from, to); - } + 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 - Map compSet = new LinkedHashMap<>(); + 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 - SetEnumValue comp = compSet.get(rep); - Value newcomp = comp.cup(new SetEnumValue(nd)).toSetEnum(); - if (newcomp instanceof SetEnumValue) { - // why wouldn't this be the case? what to do then? - compSet.put(rep, (SetEnumValue)newcomp); - } + final SetEnumValue comp = compSet.get(rep); + compSet.put(rep, (SetEnumValue) comp.cup(new SetEnumValue(nd)).toSetEnum()); } else { - // put the singleton {rep} in the component map + // start a new component {nd} compSet.put(rep, new SetEnumValue(nd)); } } SetEnumValue result = new SetEnumValue(); - for (SetEnumValue c : compSet.values()) { - Value nr = result.cup(new SetEnumValue(c)).toSetEnum(); - if (nr instanceof SetEnumValue) { - // how could this not be true? - result = (SetEnumValue)nr; - } + for (final SetEnumValue c : compSet.values()) { + result = (SetEnumValue) result.cup(new SetEnumValue(c)).toSetEnum(); } return result; } /* - * Helper class: union-find algorithm, used for computing SCCs. + * Helper class: union-find algorithm, used for computing connected components. */ - final static class UnionFind { - private final Map parent; // map every value to its parent - private int count; // number of 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. + * Initialize a new union-find structure containing all values in elts as + * singleton components. */ - public UnionFind(ValueEnumeration elts) { + 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 + 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. + * 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))) { @@ -323,7 +155,7 @@ public Value find(final Value elt) { } Value curr = elt; while (true) { - Value par = parent.get(curr); + final Value par = parent.get(curr); if (par.equals(curr)) { break; } @@ -333,7 +165,7 @@ public Value find(final Value elt) { curr = elt; while (!curr.equals(root)) { - Value par = parent.get(curr); + final Value par = parent.get(curr); parent.put(curr, root); curr = par; } @@ -344,13 +176,14 @@ public Value find(final Value elt) { /* * Merge the components containing two elements. */ - public void union(Value elt1, Value elt2) { + 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); + throw new IllegalArgumentException( + "UnionFind data structure does not contain both " + elt1 + " and " + elt2); } - Value par1 = find(elt1); - Value par2 = find(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 @@ -359,5 +192,4 @@ public void union(Value elt1, Value elt2) { } } } - } From 2a51bbb85075ca0ff6e4f74e030415acf758a6ff Mon Sep 17 00:00:00 2001 From: Stephan Merz Date: Sat, 18 Jul 2026 16:16:30 +0200 Subject: [PATCH 15/15] final cleanup Signed-off-by: Stephan Merz --- modules/GraphTheorems.tla | 2 +- modules/Graphs.tla | 20 +++++++++++--------- modules/UndirectedGraphs.tla | 19 +++++++++++-------- 3 files changed, 23 insertions(+), 18 deletions(-) diff --git a/modules/GraphTheorems.tla b/modules/GraphTheorems.tla index 504db31..2aa8840 100644 --- a/modules/GraphTheorems.tla +++ b/modules/GraphTheorems.tla @@ -9,7 +9,7 @@ THEOREM TransposeIsDirectedGraph == PROVE IsDirectedGraph(Transpose(G)) \* Note that the reverse implication does not hold in general. -\* Consider G = [node |-> {1}, edge |-> {<<1,1,1}>>, root |-> {1}] +\* 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. diff --git a/modules/Graphs.tla b/modules/Graphs.tla index 18be1da..c07345b 100644 --- a/modules/Graphs.tla +++ b/modules/Graphs.tla @@ -1,4 +1,14 @@ -------------------------------- 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. @@ -10,10 +20,6 @@ LOCAL INSTANCE SequencesExt LOCAL INSTANCE Relation *) -(***************************************************************************) -(* 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. *) (***************************************************************************) IsDirectedGraph(G) == /\ G = [node |-> G.node, edge |-> G.edge] @@ -51,17 +57,13 @@ Path(G) == {p \in Seq(G.node) : /\ \A i \in 1..(Len(p)-1) : <> \in G.edge} SimplePath(G) == - \* NB: TLC uses a Java override instead of this definition, - \* which it cannot evaluate. { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } AreConnectedIn(m, n, G) == - \* NB: TLC uses a Java override instead of this definition. \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. - \* NB: TLC uses a Java override instead of this definition. \A m, n \in G.node : AreConnectedIn(m, n, G) ConnectionsIn(G) == diff --git a/modules/UndirectedGraphs.tla b/modules/UndirectedGraphs.tla index f576bbf..ee0bdb2 100644 --- a/modules/UndirectedGraphs.tla +++ b/modules/UndirectedGraphs.tla @@ -3,6 +3,9 @@ (* 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 @@ -34,22 +37,19 @@ Path(G) == {p \in Seq(G.node) : /\ \A i \in 1..(Len(p)-1) : {p[i], p[i+1]} \in G.edge} SimplePath(G) == - \* NB: TLC uses a Java override for this operator because - \* it cannot enumerate the set Path(G). { p \in Path(G) : \A i,j \in 1..Len(p) : p[i] = p[j] => i = j } AreConnectedIn(m, n, G) == - \* NB: TLC uses a Java override for this operator. \E p \in Path(G) : (p[1] = m) /\ (p[Len(p)] = n) ----------------------------------------------------------------------------- (****************************************************************************) (* 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. *) +(* 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) == - \* NB: TLC uses a Java override for this operator. LET IsCC(S) == /\ S # {} /\ \A m,n \in S : \E p \in Seq(S) : /\ p # << >> @@ -60,12 +60,15 @@ ConnectedComponents(G) == /\ \A T \in SUBSET G.node : S \subseteq T /\ S # T => ~ IsCC(T) } -IsStronglyConnected(G) == - Cardinality(ConnectedComponents(G)) = 1 +\* 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} ----------------------------------------------------------------------------- (****************************************************************************) -(* The set of all possible undirecteddirected graphs whose node set is S. *) +(* The set of all possible undirected graphs whose node set is S. *) (* *) (* Example: *) (* UndirectedGraphs({1, 2}) = { *)