-
-
Notifications
You must be signed in to change notification settings - Fork 41
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 the operator Guess
#1590
Add the operator Guess
#1590
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1590 +/- ##
============================================
+ Coverage 74.99% 75.00% +0.01%
============================================
Files 361 361
Lines 11753 11771 +18
Branches 571 576 +5
============================================
+ Hits 8814 8829 +15
- Misses 2939 2942 +3
Continue to review full report at Codecov.
|
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.
LGTM! Few minor comments below
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/ChooseRule.scala
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala
Outdated
Show resolved
Hide resolved
tlair/src/main/scala/at/forsyte/apalache/tla/lir/oper/ApalacheOper.scala
Outdated
Show resolved
Hide resolved
I think we also need to update #888. It says:
|
Co-authored-by: Thomas Pani <[email protected]>
Co-authored-by: Thomas Pani <[email protected]>
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.
LGTM
Co-authored-by: Kukovec <[email protected]>
Closes #888. This PR adds the operator
Guess
inApalache.tla
. The operatorGuess(S)
non-deterministically picks a value out of the setS
. In this PR,Guess(S)
andCHOOSE x \in S: TRUE
behave the same. When #841 is closed,CHOOSE
will become deterministic, whereasGuess
will stay non-deterministic.make fmt-fix
(or had formatting run automatically on all files edited)