several theorems about graphs#125
Open
muenchnerkindl wants to merge 2 commits into
Open
Conversation
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
Contributor
Author
|
OK, I should have realized that the operators must be renamed in the test module for the tests to work. |
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
1 participant
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.
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:
SimplePathand renamed the old definition toMCSimplePath: it applies only to finite graphs but can be evaluated by TLC,AreConnectedInandIsStronglyConnected,IsTreeWithRootso 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
SimplePathshould be overridden byMCSimplePathetc. when using TLC.I also noticed that the definition of
TransitiveClosureinRelations.tlais correct only for finite relations and suggest to eventually make analogous changes there, introducing an operatorMCTransitiveClosure.