-
-
Notifications
You must be signed in to change notification settings - Fork 40
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 ScalaCheck shrinker to Nitpicker #1683
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1683 +/- ##
============================================
- Coverage 76.85% 76.84% -0.01%
============================================
Files 383 383
Lines 11849 11849
Branches 537 537
============================================
- Hits 9106 9105 -1
- Misses 2743 2744 +1
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.
Looks like a great start! This'll be awesome. I've suggested a few small fixes and posed a few broader questions. I am maybe getting up to speed here too, so may just need some pointers on understanding, e.g., what's up with the expression shrinker.
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/CrossTestEncodings.scala
Outdated
Show resolved
Hide resolved
Co-authored-by: Shon Feder <shon@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.
LGTM!
To produce smaller counter-examples for easier human inspection:
TlaType1
(witness type) in Nitpicker.TlaEx
(witness expression) sets to sets with fewer elements.Closes #1667, closes #1588.