-
Notifications
You must be signed in to change notification settings - Fork 31
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
Refactor value generators in the simulator #1060
Conversation
) as BS from "./BinSearch" | ||
export BS.* |
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.
@thpani did I just break the apalache integration?
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.
Yeah, although I don't understand why it breaks with the export 😂
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.
Let's maybe disable this test for now, as it waiting for the fix similar to #1051
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.
One question about oneOf(Nat)
, otw LGTM
// An infinite set, pick an integer from the range [-2^255, 2^255). | ||
// TODO: make it a configurable parameter: | ||
// https://github.com/informalsystems/quint/issues/279 | ||
.or(just(-(2n ** 255n) + this.rand(2n ** 256n))) |
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.
Can't the infinte set be Nat
and shouldn't the lower bound then be non-negative?
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.
Yep, the implementation of pick
for Int/Nat checks that and uses the absolute value in case of Nat
. I just do not want to differentiate them here.
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.
Okay. Maybe leave a comment then, so it's not confusing in the future?
Co-authored-by: Thomas Pani <[email protected]>
Closes #954. To support generation of maps over infinite co-domains, I had to refactor the interface of
pick
inRuntimeValue
. I like the new interface better, as it clearly exposes an iterator instead of doing tricky arithmetic over indices.This is a breaking change. Since it changes how
oneOf()
picks values, the seeds in the tests are not valid anymore.I have an impression that the simulator is slower now. Have to do some measurements.CHANGELOG.md
for any new functionality