-
-
Notifications
You must be signed in to change notification settings - Fork 40
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Update TLC cfg file syntax #2752
Conversation
TLCModelLaunchDelegate is Toolbox code. I don't think that TLC ever accepted the hyphenated variants; at least not within the last 15 years: https://github.com/tlaplus/tlaplus/blob/a401ad39044e5014cb07a9588611041c1d55596d/tlatools/src/tlc2/tool/ModelConfig.java#L43-L44 |
Thanks @lemmy for clarifying. Perhaps, this is based on the grammar from the specifying systems books which uses the hyphenated version |
Thanks for the update @heidihoward ! 🙏 |
Codecov Report
@@ Coverage Diff @@
## main #2752 +/- ##
=======================================
Coverage 78.88% 78.88%
=======================================
Files 464 464
Lines 15876 15876
Branches 2550 2550
=======================================
+ Hits 12523 12524 +1
+ Misses 3353 3352 -1 see 1 file with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks @heidihoward for taking care of it! It may be that I've copied this definition from the book.
Action constraints in cfg files are labelled with
ACTION_CONSTRAINT
orACTION_CONSTRAINTS
, notACTION-CONSTRAINT
orACTION-CONSTRAINTS
(underscore instead of a hyphen).Based on this comment in the TLC source code, I believe it changed from a hyphen to an underscore in 2009 https://github.com/tlaplus/tlaplus/blob/a41cbafc66b1dd225156aaca38ad35ec330f4ae9/toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java#L588