Add more tests and Java module overrides for Graphs SimplePath, AreConnectedIn and IsStronglyConnected#126
Merged
Merged
Conversation
lemmy
force-pushed
the
mku-GraphsOverrides
branch
from
3757257 to
861f2f7
Compare
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>
lemmy
force-pushed
the
mku-GraphsOverrides
branch
from
861f2f7 to
fdeaf96
Compare
lemmy
changed the title
lemmy
force-pushed
the
mku-GraphsOverrides
branch
3 times, most recently
from
3d12680 to
9c46ed8
Compare
…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>
lemmy
force-pushed
the
mku-GraphsOverrides
branch
from
9c46ed8 to
effde97
Compare
Contributor
|
LGTM, thanks! |
muenchnerkindl
approved these changes
Jul 9, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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]
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]