-
Notifications
You must be signed in to change notification settings - Fork 211
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
Minimize number of TLC configuration files. #6511
Conversation
fc978c3
to
20f09f2
Compare
0b7864b
to
b858c90
Compare
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
b858c90
to
99641bf
Compare
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 @lemmy for doing this! The duplication across cfg files meant it was tricky to always keep them all in sync
run: | | ||
set -x | ||
cd tla/ | ||
./tlc.sh -workers auto -config consensus/MCccfraftWithReconfig.cfg consensus/MCccfraft.tla -dumpTrace tla MCccfraftWithReconfig.trace.tla -dumpTrace json MCccfraftWithReconfig.json | ||
Configurations=3C2N MaxTermLimit=4 RequestLimit=1 NoCheckQuorum= ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft3C2N4T1R.trace.tla -dumpTrace json MCccfraft3C2N4T1R.json |
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.
Maybe its just me but I find NoCheckQuorum=
a bit confusing, maybe DisableCheckQuourm=True
would be clearer?
run: | | ||
set -x | ||
cd tla/ | ||
./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft.trace.tla -dumpTrace json MCccfraft.json | ||
Configurations=1C2N MaxTermLimit=2 RequestLimit=3 ./tlc.sh -workers auto consensus/MCccfraft.tla -dumpTrace tla MCccfraft1C2NT2R3.trace.tla -dumpTrace json MCccfraft1C2NT2R3.json |
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.
@lemmy I failed to spot this, but MaxTermLimit=2 here replaces MaxTermLimit=4 that was set in MCccftraft2Nodes.cfg, and effectively means we no longer do view changes in this invocation, or the one below. I am replacing the Limit with a Count, to make it clear that it's the changes from StartTerm that we are setting.
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.
+1 for changed to term count. If no view change then TermCount
should be 0 so it's clear that that is the case
A follow-up is to figure out how to run different logical configs in IDEs such as VSCode or the Toolbox. |
That's a good point, I guess we are now further away from #6490 |
Consolidate config files to reduce redundancy: The previous setup included multiple config files with mostly similar content. This commit replaces the individual config files with a single unified config file and introduces environment variables to handle differences.