-
Notifications
You must be signed in to change notification settings - Fork 201
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
Add version of Voting.tla that can be analyzed by Apalache. #112
base: master
Are you sure you want to change the base?
Conversation
This includes an inductive invariant that establishes consistency. Signed-off-by: Giuliano Losa <[email protected]>
Thanks for adding this! See above for two minor remarks on comments in the TLA module. Also, the module should be added to the manifest for the CI to succeed. |
@muenchnerkindl Thanks for having a look. I cannot find your remarks? Where are they? |
Signed-off-by: Giuliano Losa <[email protected]>
Signed-off-by: Giuliano Losa <[email protected]>
/\ NoVoteAfterMaxBal | ||
/\ Consistency | ||
|
||
\* To install `^Apalache,^' see the `^Apalache^' website at `^https://apalache.informal.systems/^' |
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.
This could additionally mention that Apalache is installed into this repo's devcontainer, which can also be used with, e.g., Gitpod or Codespaces.
Signed-off-by: Giuliano Losa <[email protected]>
This looks good to me, interesting to learn that Apalache doesn't use a separate model file for constants but defines everything in one file. |
Maybe a better way would be to be to make a few changes to
Then I think |
Signed-off-by: Giuliano Losa <[email protected]>
Instead of changing |
Signed-off-by: Giuliano Losa <[email protected]>
@nano-o One comment was about a spurious "for" in the introductory comment, which I believe you removed already. The second one was about your remark about |
I tried to make it a little cleaner by moving the definitions of constants to a different file.
Module instantiation is supported, but I don't think you can redefine things like you can with a |
About making |
You're right, this comment does not make sense. |
Signed-off-by: Giuliano Losa <[email protected]>
@@ -0,0 +1,32 @@ | |||
--------------------------- MODULE MCVotingApalache ------------------------------- |
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.
Elsewhere, we recently discussed TLA+ naming conventions. MC*Apalache
is really verbose. Perhaps, we want to adopt and encourage a less verbose convention? IIRC, Apalache already prefixes some operators with Apa
. So how about ApaMCVoting
or APAMCVoting
? Would then even be the same number of chars if users want to do APAMCVoting
and TLCMCVoting
. On the other hand, we might just as well drop MC
.
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.
The MC
prefix seems superfluous in that case. In this particular example, do you have a suggestion for the name of the specification module? Voting2.tla
and ApaVoting2.tla
?
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.
ApaVoting2
and TLCVoting2
looks like a sensible convention to me. If one want to distinguish between different modes, she can add a prefix like TLCSimVoting2
to tag this module for simulation.
By the way, the VSCode extension simulates a model/config pair whenever the prefix Smoke*
is used. This happens when the editor is saved. Once we establish a convention, we can integrate similar functionalities like type checking.
Signed-off-by: Giuliano Losa <[email protected]>
I don't think Apalache supports uninterpreted types of unspecified cardinality. So you would have to explicitly define the set of ballots anyway. |
I understand that the question is not very relevant for model checking, but |
Sorry, I lost track of the context. I think that just assuming that |
I think you can replace constants with constant expressions in the |
Did you create the prefix convention before introducing type annotations? It appears to me that using some annotation to defining overrides is more preferable than a prefix convention. |
That's true. This convention was introduced way before annotations in comments. It's actually quite a good idea to do overrides in annotations. Update: see apalache-mc/apalache#2818. |
Unfortunately Apalache cannot currently cope with However, it seems like like a small refactor may be enough to make it Apalache compatible? |
Refactoring of Apalache or Voting.tla? In my opinion, TLA+ examples should not be customized for a specific tool unless it is limited to a model checking (MC) file. Specifications are primarily meant to be readable by humans. |
For Apalache we need to add a new feature. The refactor would be of the Voting spec. The 5 line refactor I propose in the link would not impact readability afaict. But I have no opinion here nor an agenda. Just sharing the current limitations and the known workaround. Cheers. |
I completely agree. However, separating the proof in |
@muenchnerkindl if you want to do that, make a different PR and then I'll rebase on yours. |
@muenchnerkindl @nano-o is this still blocked? I'm happy to do a bit of work to get this unblocked if so. Stephan I just need to take the proofs from the TLAPS repo for Paxos and get them set up here? |
@ahelwer this is blocked until we factor out the proofs that cause Apalache to fail. |
No description provided.