several theorems about graphs by muenchnerkindl · Pull Request #125 · tlaplus/CommunityModules

muenchnerkindl · 2026-07-01T17:13:21Z

This PR adds a number of theorems about graphs, including those required for the safety proof of the Dijkstra-Scholten algorithm (https://github.com/tlaplus/Examples/tree/master/specifications/ewd687a). I'll do a PR for that proof once these theorems are in.

Besides changing some (LOCAL) INSTANCE to EXTENDS due to current limitations of the PM – including in some modules imported here – I also made a few changes to Graphs.tla:

simplified the definition of SimplePath and renamed the old definition to MCSimplePath: it applies only to finite graphs but can be evaluated by TLC,
similar changes to AreConnectedIn and IsStronglyConnected,
modified the definition of IsTreeWithRoot so that it requires the root to be a node in the graph: the previous definition was vacuously true for an graph with an empty set of nodes, for any root, and this requires case distinctions when adding a new leaf to a tree. IMHO the present definition is reasonable and more uniform.

The above changes may break some existing specification projects in that SimplePath should be overridden by MCSimplePath etc. when using TLC.

I also noticed that the definition of TransitiveClosure in Relations.tla is correct only for finite relations and suggest to eventually make analogous changes there, introducing an operator MCTransitiveClosure.

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl · 2026-07-01T17:18:18Z

OK, I should have realized that the operators must be renamed in the test module for the tests to work.

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl · 2026-07-08T13:56:34Z

@lemmy could you please have a look? I'd be particularly interested in your comments on my changes to existing operators.

lemmy · 2026-07-08T17:03:34Z

LGTM. However, wouldn't it be better to override the new generic operators using Java module overrides instead of introducing separate MC* definitions? That would free users from redefining the operators while still giving TLC an efficient definition, and follow the same approach already used elsewhere in this repository.

muenchnerkindl · 2026-07-08T17:15:39Z

Agreed, will try to do that.

lemmy · 2026-07-08T17:18:11Z

I will open a new draft PR soon with the three overrides.

muenchnerkindl · 2026-07-08T17:22:04Z

Also note that the definition of IsTreeWithRoot is slightly different from the previous one for graphs with an empty set of nodes. That's an edge case, and it's not fundamental, but I found that it avoids a few extra cases for the theorems.

lemmy · 2026-07-08T17:29:43Z

Also note that the definition of IsTreeWithRoot is slightly different from the previous one for graphs with an empty set of nodes. That's an edge case, and it's not fundamental, but I found that it avoids a few extra cases for the theorems.

The amended definition now differs from https://github.com/tlaplus/Examples/blob/47b0e2cc0268836b89f5ce451f38e5df5f1cf773/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla#L29-L33. Perhaps, we should also amend SS def?

Also, we should check if https://github.com/tlaplus/Examples/blob/master/specifications/ewd687a/EWD687a_proof.tla#L789 still proves and TLC continues to check the corresponding spec.

muenchnerkindl · 2026-07-08T17:35:10Z

Oh, I had not realized that Graphs was part of Specifying Systems ...

As for EWD687a, I have a complete proof of the safety property (amended for the changed definition of IsTreeWithRoot) and will open a PR as soon as this one is settled.

lemmy · 2026-07-08T18:44:33Z

#126

lemmy · 2026-07-08T19:06:30Z

@muenchnerkindl Are you also going to align the defs in https://github.com/tlaplus/CommunityModules/blob/master/modules/UndirectedGraphs.tla?

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 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

…nglyConnected 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 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

* 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 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * 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 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> * theorems about sequences, finite sets, and quorum systems Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * fixing two apparently brittle proofs Signed-off-by: Stephan Merz <stephan.merz@loria.fr> * align theorem statements in SequencesExtTheorems with those in the _proofs module Signed-off-by: Stephan Merz <stephan.merz@loria.fr> --------- Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Signed-off-by: Stephan Merz <stephan.merz@loria.fr> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Co-authored-by: Stephan Merz <stephan.merz@loria.fr>

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl · 2026-07-17T14:27:55Z

@lemmy I believe that the Graphs and UndirectedGraphs modules are now in a state to be merged, could you please have a look?

As for https://github.com/tlaplus/Examples/blob/47b0e2cc0268836b89f5ce451f38e5df5f1cf773/specifications/SpecifyingSystems/AdvancedExamples/Graphs.tla#L29-L33, I suggest not to change the definitions there (which would rewrite history) but to add a comment that a more recent Graphs module can be found here.

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

lemmy · 2026-07-17T19:02:49Z

-             /\ 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}
+    \* NB: TLC uses a Java override instead of this definition,


The TLA+ modules of the standard operators include a general note about overrides instead of repeating it.

https://github.com/tlaplus/tlaplus/blob/30cc3601321c3fc02e044d0ecb5c58d8921e18df/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla#L7-L11

lemmy · 2026-07-17T19:06:49Z

+
+-----------------------------------------------------------------------------
+(****************************************************************************)
+(* The set of all possible undirecteddirected graphs whose node set is S.   *)


lemmy · 2026-07-17T20:55:56Z

@@ -1,5 +1,5 @@
 ---------------------------- MODULE SequencesExt ----------------------------
-EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags
+EXTENDS Sequences, Naturals, FiniteSets, FiniteSetsExt, Folds, Functions, Bags, TLC


Not a blocker for this PR, but perhaps, we should consider adding preliminary support to TLAPS to handle the instantiation of constant-level/variable-free modules. This would prevent the namespace from becoming cluttered. Since CommunityModules are becoming TLA+’s standard library, EXTENDS will cause too many problems in the future.

lemmy · 2026-07-17T21:10:02Z

+	}
+
+	/*
+	 * Compute the strongly connected components of an undirected graph: initially


Should "strongly" be removed here?

lemmy · 2026-07-17T21:15:52Z

+    PROVE  IsDirectedGraph(Transpose(G))
+
+\* Note that the reverse implication does not hold in general.
+\* Consider G = [node |-> {1}, edge |-> {<<1,1,1}>>, root |-> {1}]


}>> swapped

lemmy · 2026-07-17T21:58:45Z

    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)


I'd suggest adding theorems that fail to prove for the initial, broken definition.

… undirected graph modules Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

lemmy

LGTM - I had AI refactor the two overrides to share code (last commit).

muenchnerkindl added 2 commits July 1, 2026 19:02

several theorems about graphs

45e83ab

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

rename operators in tests for graphs

7e67a80

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl added 2 commits July 2, 2026 08:57

rename proofs module so that it will be picked up by CI

a7d55df

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

fix two proof steps that appear to be shaky in the CI check

b76466a

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

muenchnerkindl assigned lemmy Jul 8, 2026

lemmy and others added 9 commits July 9, 2026 06:25

several theorems about graphs

e381d19

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

rename operators in tests for graphs

3019bc3

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

rename proofs module so that it will be picked up by CI

ee0bb01

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

fix two proof steps that appear to be shaky in the CI check

9501bcd

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

align undirected graphs with changes in directed graphs

8a968e4

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

minor changes

94c8ae4

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

make SCCs maximal

837b16f

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

lemmy reviewed Jul 17, 2026

View reviewed changes

Add AbstractGraphs class to share implementation between directed and…

5b5f16a

… undirected graph modules Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com> Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

lemmy approved these changes Jul 18, 2026

View reviewed changes

Uh oh!

Conversation

muenchnerkindl commented Jul 1, 2026

Uh oh!

muenchnerkindl commented Jul 1, 2026

Uh oh!

muenchnerkindl commented Jul 8, 2026

Uh oh!

lemmy commented Jul 8, 2026

Uh oh!

muenchnerkindl commented Jul 8, 2026

Uh oh!

lemmy commented Jul 8, 2026

Uh oh!

muenchnerkindl commented Jul 8, 2026

Uh oh!

lemmy commented Jul 8, 2026

Uh oh!

muenchnerkindl commented Jul 8, 2026

Uh oh!

lemmy commented Jul 8, 2026

Uh oh!

lemmy commented Jul 8, 2026

Uh oh!

muenchnerkindl commented Jul 17, 2026

Uh oh!

lemmy Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

lemmy Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

lemmy Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

lemmy Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

lemmy Jul 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lemmy Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

lemmy left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

lemmy Jul 17, 2026 •

edited

Loading