safety proof of EWD687a#215
Conversation
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
| (* there is no need to change upEdge[p] in the Idle subaction. *) | ||
| (***************************************************************************) | ||
| Idle(p) == /\ active' = [active EXCEPT ![p] = FALSE] | ||
| Idle(p) == /\ active[p] \* otherwise this step is subsumed by stuttering |
There was a problem hiding this comment.
I suggest elaborating on why this is an issue.
There was a problem hiding this comment.
It would require an extra case distinction in the proof of the tree invariant. But your remark prompted me to adapt the comment explaining the Idle action.
There was a problem hiding this comment.
Incidentally, I noticed that you had added an action constraint to the model used for animation precisely to rule out such stuttering steps caused by the Idle action. I removed that because it has become unnecessary with the changed definition.
| /\ O.edge # {} => G!IsTreeWithRoot(O, Leader) | ||
| \* All nodes of the overlay tree are non-neutral. | ||
| /\ N:: \A n \in O.node: ~neutral(n)) | ||
| \* The original definition includes every node occurring in the tree |
There was a problem hiding this comment.
The comment about the original definition can likely be omitted.
| P3 = P3 | ||
| \* MV CONSTANT definitions | ||
| MaxCounter = 3 | ||
| Leader = L |
|
Can the reduction of proof effort be soley attributed to the introduction of GraphTheorems? |
In fact, the previous proof did not establish DT1Inv (i.e., correctness of the algorithm). It did show that the overlay graph was acyclic, but a dag is not quite enough, one really needs a tree. It had also suggested a strengthening of DT1Inv by adding an additional conjunct to acyclicity. Replacing the acyclicity condition with the tree predicate was enough for the proof to go through, based on the lemmas about graphs. Also, I took inspiration from the way acyclicity was expressed for proving a general lemma that implies that a tree is acyclic. Overall, the work done by Claude was very useful, even it didn't quite manage to prove overall correctness. A technicality was that the tree invariant made use of an instance introduced in a |
Signed-off-by: Stephan Merz <stephan.merz@loria.fr>
That would cripple the current TLC REPL, which relies solely on > % tlcrepl
Welcome to the TLA+ REPL!
TLC2 Version 2026.04.27.203507
Enter a constant-level TLA+ expression.
(tla+) LET B == INSTANCE Bags IN B!SetToBag({})
<<>> |
Understood. |
2 participants
Updated EWD687a according to the changes in the Graphs community module, and contributed a proof of the safety property of the algorithm.