Repository navigation
Conversation
muenchnerkindl
approved these changes
Oct 30, 2026
muenchnerkindl
left a comment
muenchnerkindl
left a comment
Collaborator
There was a problem hiding this comment.
LGTM, thanks! I would probably have tried to structure the proof a little differently, see suggestions in the comments.
Collaborator
|
P.S.: It seems to me that the same issue affects |
lemmy
changed the title
Apalache looks up modules only in the directory of the spec, in its own standard library, and in its working directory. It ignores TLA-Library, and the classpath that lets TLC find TLAPS.tla does not reach it. A spec that extends TLAPS, or instantiates a module that does, therefore fails to parse with "Cannot find source file for module TLAPS". Running Apalache from the TLAPS library directory lets it find the module. All paths passed to Apalache are now absolute, and --out-dir keeps its output in _apalache-out at the root of the repository. https://github.com/tlaplus/Examples/actions/runs/41087129395/job/124171232756 Co-authored-by: Claude Opus 5.5 <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it instantiates a module. If the module with the INSTANCE does not extend TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found". With tlapm#321, every instantiated WF contains ENABLED, so EWD840_proof hits this bug through TD == INSTANCE SyncTerminationDetection. tlaplus/tlapm#250 tlaplus/tlapm#321 Co-authored-by: Claude Opus 5.5 <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]>
Instantiation does not distribute over ENABLED, and hence not over WF. The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination) matching the fairness conjunct of TD!Spec, which tlapm#321 no longer allows. SyncTerminationDetection now names its fairness condition Fair, and the proof derives TD!Fair from the new lemma SyncTerminationDetection_proof!Fairness. Apalache accepts only fairness written out in Spec, so APSyncTerminationDetection.cfg now names Init and Next instead. tlaplus/tlapm#69 tlaplus/tlapm#321 Co-authored-by: Stephan Merz <[email protected]> Co-authored-by: Claude Opus 5.5 <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlapm rewrites ENABLED into EnabledWrapper from the TLAPS module when it instantiates a module. If the module with the INSTANCE does not extend TLAPS, ExpandENABLED fails with "Operator EnabledWrapper not found". With tlapm#321, every instantiated WF contains ENABLED, so EWD998_proof hits this bug through TD == INSTANCE AsyncTerminationDetection. tlaplus/tlapm#250 tlaplus/tlapm#321 Co-authored-by: Claude Opus 5.5 <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]>
Instantiation does not distribute over ENABLED, and hence not over WF. The proof of Spec => TD!Spec relied on WF_TD!vars(TD!DetectTermination) matching the fairness conjunct of TD!Spec, which tlapm#321 no longer allows. AsyncTerminationDetection now names its fairness condition Fair, and the proof derives TD!Fair from the new lemma AsyncTerminationDetection_proof!Fairness. tlaplus/tlapm#69 tlaplus/tlapm#321 Co-authored-by: Stephan Merz <[email protected]> Co-authored-by: Claude Opus 5.5 <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]>
Member
Author
|
Merging, as the remaining failing checks are unrelated to this change. |
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.
tlapm distributes instantiation over
WFandSF, which is unsound (tlaplus/tlapm#69). Once fixed (tlaplus/tlapm#321),EWD840_proof.tlafails (https://github.com/tlaplus/tlapm/actions/runs/40806417736/job/123226446658?pr=321) for two independent reasons. Each commit fixes one of them:ENABLEDintoEnabledWrapperfrom theTLAPSmodule when it instantiates a module.ExpandENABLEDfails if the module with theINSTANCEdoesn't extendTLAPS(compare TLAPM fails when instantiating a module containing ENABLEDaxioms (Error: Operator "EnabledWrapper" not found) tlapm#250). Once TLAPM identifies instantiated fairness condition with fairness of instantiated action tlapm#69 is fixed, every instantiatedWFcontainsENABLED, soTD == INSTANCE SyncTerminationDetectiontriggers the bug. This can be reverted once TLAPM fails when instantiating a module containing ENABLEDaxioms (Error: Operator "EnabledWrapper" not found) tlapm#250 has been addressed.Spec => TD!Specrelied onWF_TD!vars(TD!DetectTermination)matching the fairness conjunct ofTD!Spec. The proof now refers to the instantiatedENABLEDthrough the new operatorSyncTerminationDetection!EnabledDT.