Skip to content
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

Introduce a new run operator expect #1303

Merged
merged 12 commits into from
Dec 12, 2023
Merged

Introduce a new run operator expect #1303

merged 12 commits into from
Dec 12, 2023

Conversation

konnov
Copy link
Contributor

@konnov konnov commented Dec 12, 2023

Closes #1252. Following the discussion raised by @hvanz, I have implemented the operator A.expect(P) with the following semantics:

  • Evaluate action A:
    • When A's result is false, emit a runtime error.
    • When A's result is true:
      • Commit the variable updates.
      • Evaluate P:
        • If P evaluates to false, emit a runtime error (similar to assert).
        • If P evaluates to true, rollback to the previous state and return true.

Its semantics looks a bit complex, but this is basically what we want, if we do not want to have an extra stuttering step that calls assert(P).

Here are the examples from the unit tests:

image

  • Tests added for any new code
  • Documentation added for any new functionality
  • Entries added to the respective CHANGELOG.md for any new functionality

@konnov konnov marked this pull request as ready for review December 12, 2023 10:42
Comment on lines 1346 to 1349
// rollback to the previous state in any case
this.recoverVars(savedVarsAfterAction)
this.recoverNextVars(savedNextVarsAfterAction)
this.resetTrace(just(rv.mkList(savedTraceAfterAction)))
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we really need the rollback if the effect is already preventing updates inside the expect argument? I found the "rollback" explanation in the documentation confusing.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm also not clear on why a rollback is needed.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have added clarifying comments about why we have to do that in the simulator

@thpani
Copy link
Contributor

thpani commented Dec 12, 2023

have implemented the operator A.except(P) with the following semantics

I think this should say expect?
Had me confused for a while 😄

Copy link
Contributor

@thpani thpani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

CHANGELOG.md Outdated Show resolved Hide resolved
doc/lang.md Outdated Show resolved Hide resolved
@konnov
Copy link
Contributor Author

konnov commented Dec 12, 2023

have implemented the operator A.except(P) with the following semantics

I think this should say expect? Had me confused for a while 😄

Yeah, I keep typing except all the time. This probably comes from TLA+

@konnov konnov merged commit e61c083 into main Dec 12, 2023
15 checks passed
@konnov konnov deleted the igor/expect1252 branch December 12, 2023 17:37
@shonfeder shonfeder mentioned this pull request Jan 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

write post-condition assertions without introducing a new step
4 participants