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.

Sign up for GitHub

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

Jump to bottom

Refactor value generators in the simulator #1060

Merged
merged 17 commits into from
Jul 20, 2023
Merged

Refactor value generators in the simulator #1060

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
3e7b22e
refactor value generation in the simulator
konnov Jul 19, 2023
dd1ef60
apply formatting
konnov Jul 19, 2023
62a393f
point to a configuration issue
konnov Jul 19, 2023
8e5ef77
Merge branch 'main' into igor/maps954
konnov Jul 19, 2023
188fa1d
update the changelog
konnov Jul 19, 2023
c3c5c06
fixing the seeds and tests
konnov Jul 19, 2023
c03fa53
more fixes
konnov Jul 19, 2023
df3d866
fix the tests
konnov Jul 19, 2023
b967103
simplify the code in bounds
konnov Jul 19, 2023
a47ac13
fix the sample size
konnov Jul 19, 2023
68bbf91
Update CHANGELOG.md
konnov Jul 20, 2023
3ac39e7
update changelog
konnov Jul 20, 2023
3e1431b
add a comment
konnov Jul 20, 2023
2ae62ee
update the dashboard
konnov Jul 20, 2023
53d0d1e
Merge branch 'main' into igor/maps954
konnov Jul 20, 2023
97e8621
ignore the binsearch test in cli-tests
konnov Jul 20, 2023
3a9a0a0
fix the dashboard
konnov Jul 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
### Added

- `quint repl` produces an evaluation trace on errors too (#1056)
- `S.setOfMaps(Int).oneOf()` is now supported (#1060)

### Changed

- `quint run` produces a friendlier message when it meets a `const` (#1050)
- The behavior of `oneOf` has changed, update the seeds in `quint test` (#1060)
konnov marked this conversation as resolved.
Show resolved Hide resolved

### Deprecated
### Removed
Expand Down
5 changes: 3 additions & 2 deletions examples/classic/sequential/BinSearch/BinSearch10.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,6 @@ module BinSearch10 {
INPUT_SEQ=[ 1, 2, 3, 4, 5, 6, 8, 9, 10, 33 ],
INPUT_KEY=7,
INT_WIDTH=16
).* from "./BinSearch"
}
) as BS from "./BinSearch"
Copy link
Contributor Author

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?

Copy link
Contributor

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 😂

Copy link
Contributor Author

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

export BS.*
}
8 changes: 6 additions & 2 deletions examples/solidity/GradualPonzi/gradualPonzi.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,8 +230,12 @@ module gradualPonziTest {
//
// $ quint run --invariant=progressInv --main=gradualPonziTest gradualPonzi.qnt
//
// Also try:
// If quint has not reported a violation, try:
//
// $ quint run --invariant=progressInv --main=gradualPonziTest --seed=0x8385bfe3a7497 gradualPonzi.qnt
//
// It is quite hard for `quint run` to find a violation to this property.
// In contrast, `quint verify` finds it in a few seconds.
val progressInv = {
userAddr.exists(someone =>
receive(evmState, ponziState, someone, MINIMUM_INVESTMENT).error == ""
Expand All @@ -245,7 +249,7 @@ module gradualPonziTest {
// There should be no left over tokens on the contract balance.
//
// This invariant is violated due to rounding errors:
// $ quint run --invariant=noLeftovers --main=gradualPonziTest gradualPonzi.qnt
// $ quint run --invariant=noLeftoversInv --main=gradualPonziTest gradualPonzi.qnt
val noLeftoversInv = {
val sumRewards = addr.fold(0, (s, a) => s + ponziState.rewards.get(a))
sumRewards == evmState.balances.get("contract")
Expand Down
34 changes: 20 additions & 14 deletions quint/cli-tests.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,17 +274,17 @@ fi

<!-- !test exit 1 -->
<!-- !test check lottery - Run -->
quint run --max-samples=10000 --max-steps=10 --seed=0x29f8e8021fae9 \
quint run --max-samples=10000 --max-steps=10 --seed=0x29f8e808de5ed \
--invariant=noBuyInDrawingInv --main=lotteryMempool \
../examples/solidity/icse23-fig7/lottery.qnt

### FAIL on run BinSearch10
### OK on run BinSearch10

<!-- !test exit 1 -->
<!-- !test exit 0 -->
<!-- !test check BinSearch - Run -->
quint run --max-samples=10000 --max-steps=10 --seed=0x29f8e8021fae9 \
--invariant=Postcondition --init=Init --next=Next \
../examples/classic/sequential/BinSearch10.qnt
quint run --max-samples=10000 --max-steps=10 \
--invariant=Postcondition \
../examples/classic/sequential/BinSearch/BinSearch10.qnt

### OK on test simplePonzi

Expand All @@ -308,31 +308,37 @@ fi
<!-- !test check simplePonzi - Run progressInv -->
quint run \
--invariant=progressInv --main=simplePonziTest \
--seed=0x1f035d45bceacb \
--seed=0x1f035d45bcece7 \
../examples/solidity/SimplePonzi/simplePonzi.qnt

### OK on run gradualPonzi::noNegativeInv

<!-- !test exit 0 -->
<!-- !test check gradualPonzi - Run noNegativeInv -->
quint run --max-samples=10000 \
quint run --max-samples=1000 \
--invariant=noNegativeInv --main=gradualPonziTest \
../examples/solidity/GradualPonzi/gradualPonzi.qnt

### FAIL on run gradualPonzi::progressInv
### OK (FAIL?) on run gradualPonzi::progressInv

<!-- !test exit 1 -->
This test should fail. We know that from `quint verify`.
However, `quint run` has hard time finding a counterexample.
If you see this test failing, you are a lucky winner!
thpani marked this conversation as resolved.
Show resolved Hide resolved
Add the seed to the command below and change the exit code to 1.

<!-- !test exit 0 -->
<!-- !test check gradualPonzi - Run progressInv -->
quint run --invariant=progressInv --main=gradualPonziTest \
--max-samples=100000 --max-steps=40 --seed=0x14cfeb23f5e066 \
gradualPonzi.qnt
--max-samples=1000 --max-steps=50 \
../examples/solidity/GradualPonzi/gradualPonzi.qnt

### FAIL on run gradualPonzi::noLeftoversInv

<!-- !test exit 1 -->
<!-- !test check gradualPonzi - Run noLeftoversInv -->
quint run --invariant=noLeftoversInv --main=gradualPonziTest \
--seed=0x1ea5141b0fe9e1 gradualPonzi.qnt
--seed=0x405df8f62fcd7 \
../examples/solidity/GradualPonzi/gradualPonzi.qnt

### OK on test gradualPonzi

Expand All @@ -346,7 +352,7 @@ fi

<!-- !test exit 1 -->
<!-- !test check river - Run noSolution -->
quint run --invariant=noSolution --seed=0x2fa6b93d0df3f \
quint run --invariant=noSolution --seed=0x2fa6b93d1eef3 \
../examples/puzzles/river/river.qnt

### OK on run river::safety
Expand Down
Loading
Loading