Refactor value generators in the simulator

CHANGELOG.md

@@ -10,9 +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
 
+- **Breaking**: the behavior of `oneOf` has changed, existing seed values for `quint test`
+  can exhibit different behavior than before (#1060)
 - `quint run` produces a friendlier message when it meets a `const` (#1050)
 
 ### Deprecated

examples/classic/sequential/BinSearch/BinSearch10.qnt

@@ -5,4 +5,5 @@ module BinSearch10 {
     INPUT_KEY=7,
     INT_WIDTH=16
   ).* from "./BinSearch"
-}
+  // quint run does not for at the moment, since it expects an export
+}

examples/solidity/GradualPonzi/gradualPonzi.qnt

@@ -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 == ""
@@ -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")

quint/cli-tests.md

@@ -274,17 +274,21 @@ 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
+### IGNORE on run BinSearch10
+
+This test should work, but due to a problem with flattening, it does not.
+Hence, we ignore it. When flattening is repaired, this test will start
+to work. Fix the exit code to 0 and IGNORE to OK.
 
 <!-- !test exit 1 -->
 <!-- !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
 
@@ -308,31 +312,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
+### IGNORE 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!
+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
 
@@ -346,7 +356,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