Merge pull request #1037 from informalsystems/821/fix-examples

Fix more examples

examples/README.md

@@ -68,17 +68,17 @@ listed without any additional command line arguments.
 | [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
 | [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/booleans.qnt](./language-features/booleans.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [language-features/imports.qnt](./language-features/imports.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [language-features/instances.qnt](./language-features/instances.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [language-features/instancesFrom.qnt](./language-features/instancesFrom.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [language-features/counters.qnt](./language-features/counters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/importFrom.qnt](./language-features/importFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/imports.qnt](./language-features/imports.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/instances.qnt](./language-features/instances.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [language-features/instancesFrom.qnt](./language-features/instancesFrom.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/integers.qnt](./language-features/integers.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/lists.qnt](./language-features/lists.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/maps.qnt](./language-features/maps.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [language-features/nondet.qnt](./language-features/nondet.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [language-features/nondetEx.qnt](./language-features/nondetEx.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [language-features/sets.qnt](./language-features/sets.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |

examples/language-features/counters.qnt

@@ -3,7 +3,7 @@ module counters {
   var n: int
 
   // initialize the state machine
-  action Init = {
+  action init = {
     n' = 1
   }
 
@@ -31,7 +31,7 @@ module counters {
   //  - increment n, when n is positive
   //
   // Note that the three actions are not mutually exclusive.
-  action Next = any {
+  action step = any {
     OnEven,
     OnDivByThree,
     OnPositive
@@ -46,43 +46,45 @@ module counters {
       .then(n' = 3)
   }
 
-  // the run that initialized with Init and
+  // the run that initialized with init and
   // executes OnPositive twice, OnDivByThree, and OnEven
   run run2 = {
-    Init
+    init
       .then(OnPositive)
       .then(OnPositive)
       .then(OnDivByThree)
       .then(OnEven)
   }
 
-  // execute Init and then Next four times
+  // execute init and then step four times
   run run3 = {
-    Init.then(4.reps(_ => Next))
+    init.then(4.reps(_ => step))
   }
 
-  // execute Init and then Next ten times, while asserting n < 5
+  // execute init and then step ten times, while asserting n < 5
   run run4 = {
-    Init.then(10.reps(_ => all {
+    init.then(10.reps(_ => all {
       assert(n < 5),
-      Next,
+      step,
     }))
   }
 
   // this test should not fail
   run passingTest = {
-    Init.then(10.reps(_ => all {
+    init.then(10.reps(_ => all {
         assert(n > 0),
-        Next,
+        step,
     }))
   }
 
-  // this test should fail
+  // this tests for a failing condition
   run failingTest = {
-    Init.then(10.reps(_ => all {
-        assert(n == 0),
-        Next,
-    }))
+    init
+      .then(10.reps(_ => all {
+         n == 0,
+         step,
+       }))
+      .fail()
   }
 
   // this is just a value, and it should be ignored as a test

examples/language-features/importFrom.qnt

@@ -7,4 +7,7 @@ module importFrom {
   run importTest = {
     assert(pow(5, 2) == sqr(5))
   }
-}
+
+  action init = true
+  action step = true
+}

examples/language-features/imports.qnt

@@ -80,15 +80,20 @@ module F {
   export basics as ExportedBasics
 }
 
-module G {
+module imports {
   import E
   import F as MyF
 
+  val test_exported1 = E::Math::pow(2, 2) == 4
+  val test_exported2 = MyF::ExportedBasics::double(2) == 4
+
   action init = all {
     E::init,
     MyF::init
   }
 
-  val test_exported1 = E::Math::pow(2, 2) == 4
-  val test_exported2 = MyF::ExportedBasics::double(2) == 4
+  action step = all {
+    E::x' = E::x,
+    MyF::y' = MyF::y,
+  }
 }

examples/language-features/instances.qnt

@@ -7,7 +7,7 @@ module A {
   pure def g(b) = not(b)
 }
 
-module Instances {
+module instances {
   pure val MyY = true
   pure val z = "world"
 
@@ -26,4 +26,7 @@ module Instances {
 
   export A1
   export A2
+
+  action init = true
+  action step = true
 }

examples/language-features/instancesFrom.qnt

@@ -1,4 +1,4 @@
-module InstancesFrom {
+module instancesFrom {
   pure val MyY = true
   pure val z = "world"
 
@@ -17,4 +17,7 @@ module InstancesFrom {
 
   export A1
   export A2
+
+  action init = true
+  action step = true
 }

examples/language-features/records.qnt

@@ -1,4 +1,4 @@
-module Records {
+module records {
     var rec1: { f1: int, f2: str | r1 }
     var rec2: { f2: str, f3: bool | r2 }
     var rec3: { f1: int }
@@ -13,13 +13,13 @@ module Records {
 
     def updateF1(r) = r.with("f1", 1) 
 
-    action Init = all {
+    action init = all {
         rec1' = { f1: 1, f2: "hello" },
         rec2' = { f2: "world", f3: true },
         rec3' = { f1: 2 },
     }
 
-    action Next = all {
+    action step = all {
         rec1' = updateF1(rec1),
         rec2' = rec2.with("f3", true),
         rec3' = updateF1(rec3),

quint/cli-tests.md

@@ -182,41 +182,6 @@ Temporarily disabled.
 <!-- !test check LamportMutex - Types & Effects -->
     quint typecheck ../examples/classic/distributed/LamportMutex/LamportMutex.qnt
 
-### OK on parse counters
-
-<!-- !test check counters -->
-    quint parse ../examples/language-features/counters.qnt
-
-### OK on parse records
-
-<!-- !test check records -->
-    quint parse ../examples/language-features/records.qnt
-
-### OK on typecheck records
-
-<!-- !test check records - Types & Effects-->
-    quint typecheck ../examples/language-features/records.qnt
-
-### OK on parse tuples
-
-<!-- !test check tuples -->
-    quint parse ../examples/language-features/tuples.qnt
-
-### OK on typecheck tuples
-
-<!-- !test check tuples - Types & Effects-->
-    quint typecheck ../examples/language-features/tuples.qnt
-
-### OK on typecheck counters
-
-<!-- !test check counters - Types & Effects-->
-    quint typecheck ../examples/language-features/counters.qnt
-
-### OK on typecheck booleans
-
-<!-- !test check booleans - Types & Effects-->
-    quint typecheck ../examples/language-features/booleans.qnt
-
 ### OK on typecheck coin
 
 <!-- !test check coin - Types & Effects-->
@@ -227,11 +192,6 @@ Temporarily disabled.
 <!-- !test check SimpleAuctionNonComposable - Syntax/Types & Effects/Unit tests -->
     quint test --main=SimpleAuction ../examples/solidity/SimpleAuction/SimpleAuctionNonComposable.qnt
 
-### OK on test nondet.qnt
-
-<!-- !test check nondet - Syntax/Types & Effects/Unit tests -->
-    quint test --main=nondetEx ../examples/language-features/nondet.qnt
-
 ### OK on test lottery.qnt
 
 <!-- TODO: Spec test is erroneous https://github.com/informalsystems/quint/issues/775 -->

quint/io-cli-tests.md

@@ -190,7 +190,7 @@ echo "import counters.*" | quint -r ../examples/language-features/counters.qnt 2
 
 <!-- !test in repl loads a file and a module -->
 ```
-echo "Init" | quint -r ../examples/language-features/counters.qnt::counters 2>&1 | tail -n +3
+echo "init" | quint -r ../examples/language-features/counters.qnt::counters 2>&1 | tail -n +3
 ```
 
 <!-- !test out repl loads a file and a module -->
@@ -222,7 +222,7 @@ echo ".save tmp-counters.qnt" \
   | quint -r ../examples/language-features/counters.qnt::counters 2>&1 \
   | tail -n +3
 # do not auto-import counters, as it is imported already
-echo "Init" \
+echo "init" \
   | quint -r tmp-counters.qnt 2>&1 \
   | tail -n +3
 rm tmp-counters.qnt
@@ -244,27 +244,24 @@ The command `test` finds failing tests and prints error messages.
 <!-- !test exit 1 -->
 <!-- !test in test runs -->
 ```
-output=$(quint test --main counters --seed 1 ../examples/language-features/counters.qnt)
+output=$(quint test --main failingTestCounters --seed 1 ./testFixture/simulator/failingTestCounters.qnt)
 exit_code=$?
-echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*counters.qnt#      HOME/counters.qnt#g'
+echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*failingTestCounters.qnt#      HOME/failingTestCounters.qnt#g'
 exit $exit_code
 ```
 
 <!-- !test out test runs -->
 ```
 
-  counters
-    ok passingTest passed 10000 test(s)
+  failingTestCounters
     1) failingTest failed after 1 test(s)
 
-  1 passing (duration)
   1 failed
-  1 ignored
 
   1) failingTest:
-      HOME/counters.qnt:83:9 - error: Assertion failed
-      83:         assert(n == 0),
-    Use --seed=0x1109d --match=failingTest to repeat.
+      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      45:          assert(n == 0),
+    Use --seed=0x1 --match=failingTest to repeat.
 
 
   Use --verbosity=3 to show executions.
@@ -278,31 +275,28 @@ recorded yet.
 <!-- !test exit 1 -->
 <!-- !test in test empty trace -->
 ```
-output=$(quint test --seed 1 --verbosity=3 ../examples/language-features/counters.qnt)
+output=$(quint test --seed 1 --verbosity=3 ./testFixture/simulator/failingTestCounters.qnt)
 exit_code=$?
-echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*counters.qnt#      HOME/counters.qnt#g'
+echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*failingTestCounters.qnt#      HOME/failingTestCounters.qnt#g'
 exit $exit_code
 ```
 
 <!-- !test out test empty trace -->
 ```
 
-  counters
-    ok passingTest passed 10000 test(s)
+  failingTestCounters
     1) failingTest failed after 1 test(s)
 
-  1 passing (duration)
   1 failed
-  1 ignored
 
   1) failingTest:
-      HOME/counters.qnt:83:9 - error: Assertion failed
-      83:         assert(n == 0),
+      HOME/failingTestCounters.qnt:45:10 - error: Assertion failed
+      45:          assert(n == 0),
 
 [Frame 0]
-Init() => true
+init() => true
 
-    Use --seed=0x1109d --match=failingTest to repeat.
+    Use --seed=0x1 --match=failingTest to repeat.
 ```
 
 ### Run finds an invariant violation
@@ -311,7 +305,7 @@ The command `run` finds an invariant violation.
 
 <!-- !test in run finds violation -->
 ```
-output=$(quint run --init=Init --step=Next --seed=0x308623f2a48e7 --max-steps=4 \
+output=$(quint run --seed=0x308623f2a48e7 --max-steps=4 \
   --invariant='n < 10' ../examples/language-features/counters.qnt 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' -e 's#^.*counters.qnt#      HOME/counters.qnt#g'
@@ -345,8 +339,7 @@ The command `run` finds an example.
 
 <!-- !test in run finds example -->
 ```
-quint run --init=Init --step=Next --seed=17 --max-steps=4 \
-  --invariant='n < 100' ../examples/language-features/counters.qnt 2>&1 | \
+quint run --seed=17 --max-steps=4 --invariant='n < 100' ../examples/language-features/counters.qnt 2>&1 | \
   sed 's/([0-9]*ms)/(duration)/g' | \
   sed 's#^.*counters.qnt#      HOME/counters.qnt#g'
 ```
@@ -757,7 +750,7 @@ error: --seed must be a big integer, found: NotANumber
 
 <!-- !test in compile imports -->
 ```
-echo "init" | quint -r ../examples/language-features/imports.qnt::G 2>&1 | tail -n +3
+echo "init" | quint -r ../examples/language-features/imports.qnt::imports 2>&1 | tail -n +3
 ```
 
 <!-- !test out compile imports -->
@@ -771,7 +764,7 @@ echo "init" | quint -r ../examples/language-features/imports.qnt::G 2>&1 | tail
 
 <!-- !test in compile instances -->
 ```
-echo -e "A1::f(1)\nA2::f(1)" | quint -r ../examples/language-features/instances.qnt::Instances 2>&1 | tail -n +3
+echo -e "A1::f(1)\nA2::f(1)" | quint -r ../examples/language-features/instances.qnt::instances 2>&1 | tail -n +3
 ```
 
 <!-- !test out compile instances -->