Checks for misuse of nondet and oneOf
#1431
Merged
Conversation
This file contains 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
bugarela
commented
May 6, 2024
| @@ -66,7 +66,7 @@ listed without any additional command line arguments. | |||
| | [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | |||
| | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] | | |||
| | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] | | |||
| | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: | | |||
| | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | | |||
There was a problem hiding this comment.
Turns out all that was stopping this from working with Apalache was a hidden nondet issue :)
|
Breaking tests are unrelated to this PR. CI is picking up the latest release for Apalache I cut this morning, so I have to updated some test's expectations. I'll do that in a separate PR. |
p-offtermatt
reviewed
May 7, 2024
p-offtermatt
reviewed
May 7, 2024
p-offtermatt
reviewed
May 7, 2024
p-offtermatt
approved these changes
May 7, 2024
Co-authored-by: Philip Offtermatt <[email protected]>
This was referenced May 7, 2024
Merged
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.
Hello
Closes #378 (it actually fails with an "effect" error, which I think it makes more sense than a parse error, but this has been greatly discussed in the past).
It also solves the most important parts of #381, but I still have to see if there's something greater to be accomplished if we make proper effects for non-determinism.
This PR introduces some checks for how
nondetandoneOfcan be used. The usage is quite restrictive because we need to be able to convert this to TLA+ for model checking, and the current syntax makes it seem like you can use non determinism everywhere. Hopefully, the IDE/cli errors will help people understand that these are special keywords that can't be used everywhere. Also, since the simulator allows too much, you'd only notice something is wrong when running verify or compile to TLA+.One of the cases in particular is when
nondetdefinitions are top-level, which is not allowed. This was already being caught, but by the parser, and it was really hard to understand the issue by the parsing error. So I changed the parser to normally parsenondetas any other qualifier, and then properly report the error later on.Test fixtures were updated because I'm now including the definitions themselves in the lookup table, so the tables in all fixtures were updated. We have issue #1422 to address how hard it is to read the diffs - for now: sorry!
CHANGELOG.mdfor any new functionalityREADME.mdupdated for any listed functionality