Merge pull request #1077 from informalsystems/th/exdashboard-add-info

Track remaining issues in the examples dashboard
informalsystems · Jul 26, 2023 · e0eefb5 · e0eefb5
2 parents 4d66a86 + 16f97de
commit e0eefb5
Show file tree

Hide file tree

Showing 9 changed files with 99 additions and 45 deletions.
diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
@@ -10,12 +10,50 @@
 
 result () {
     local cmd="$1"
-    if ($cmd &> /dev/null)
+    local args="$2"
+    local file="$3"
+
+    # Skip verification for specs that do not define a state machine
+    if [[ "$cmd" == "verify" && (
+            "$file" == "cosmos/lightclient/typedefs.qnt" ||
+            "$file" =~ ^spells/ ||
+            "$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
+            "$file" == "cosmos/ics20/base.qnt" ) ]] ; then
+      printf "N/A[^nostatemachine]"; return
+    fi
+
+    # Run the command and record success / failure
+    local quint_cmd="quint $cmd $args $file"
+    if ($quint_cmd &> /dev/null)
     then
         printf ":white_check_mark:"
     else
         printf ":x:"
     fi
+
+    # Print additional explanations
+    if [[ "$file" == "classic/distributed/ewd840/ewd840.qnt" && ( "$cmd" != "parse" ) ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/581</sup>"
+    elif [[ "$file" == "classic/distributed/Paxos/Paxos.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
+    elif [[ "$file" == "classic/distributed/Paxos/Voting.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" )]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
+    elif [[ "$file" == "cosmos/ics20/ics20.qnt" && "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
+    elif [[ "$file" == "cosmos/ics23/ics23.qnt" && "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/693,</sup>"
+      printf "<sup>https://github.com/informalsystems/quint/pull/975</sup>"
+    elif [[ "$file" == "cosmos/tendermint/TendermintAcc005.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" ) ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/pull/1023</sup>"
+    elif [[ "$file" == "cosmwasm/zero-to-hero/vote.qnt" && "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/693</sup>"
+    elif [[ "$file" == "language-features/option.qnt" && ( "$cmd" == "test" || "$cmd" == "verify" ) ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/244</sup>"
+    elif [[ "$file" == "language-features/tuples.qnt" && "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/apalache/issues/2670</sup>"
+    elif [[ "$file" == "solidity/icse23-fig7/lottery.qnt" && "$cmd" == "verify" ]] ; then
+      printf "<sup>https://github.com/informalsystems/quint/issues/1019</sup>"
+    fi
 }
 
 get_main () {
@@ -25,6 +63,8 @@ get_main () {
     main="--main=LamportMutex_3_10"
   elif [[ "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ]] ; then
     main="--main=ReadersWriters_5"
+  elif [[ "$file" == "classic/sequential/BinSearch/BinSearch.qnt" ]] ; then
+    main="--main=BinSearch10"
   elif [[ "$file" == "cosmos/ics20/bank.qnt" ]] ; then
     main="--main=bankTests"
   elif [[ "$file" == "cosmos/ics20/denomTrace.qnt" ]] ; then
@@ -43,6 +83,15 @@ get_main () {
   echo "${main}"
 }
 
+get_test_args () {
+  local file="$1"
+  local args=""
+  if [[ "$file" == "cosmos/ics20/ics20.qnt" ]] ; then
+    args="--max-samples=1000"  # default of 10000 takes too long
+  fi
+  echo "${args}"
+}
+
 get_verify_args () {
   local file="$1"
   local args=""
@@ -55,11 +104,12 @@ get_verify_args () {
 }
 
 file="$1"
-syntax="$(result "quint parse ${file}")"
-types="$(result "quint typecheck ${file}")"
-main="$(get_main "${file}")"
-tests="$(result "quint test ${main} ${file}")"
-verify_args="$(get_verify_args "${file}")"
-verify="$(result "quint verify --max-steps=3 ${verify_args} ${main} ${file}")"
+syntax=$(result parse "" "$file")
+types=$(result typecheck "" "${file}")
+main_flag=$(get_main "${file}")
+test_args=$(get_test_args "${file}")
+tests=$(result test "${test_args} ${main_flag}" "${file}")
+verify_args=$(get_verify_args "${file}")
+verify=$(result verify "--max-steps=3 ${verify_args} ${main_flag}" "${file}")
 
 echo "| [${file}](./${file}) | ${syntax} | ${types} | ${tests} | ${verify} |"
diff --git a/examples/.scripts/run-examples.sh b/examples/.scripts/run-examples.sh
@@ -22,3 +22,6 @@ export APALACHE_DIST=${APALACHE_DIST:-../quint/_build/apalache}
 # We `cut` the first 2 characters of find to remove the leading `./`, making
 # the output prettier.
 find . -name "*.qnt" | cut -c3- | parallel "${SCRIPT_DIR}/run-example.sh" | env LC_ALL=C sort --ignore-case
+
+echo
+echo "[^nostatemachine]: This specification does not define a state machine."
diff --git a/examples/README.md b/examples/README.md
@@ -49,24 +49,23 @@ listed without any additional command line arguments.
 | Example | Syntax (`parse`) | Types (`typecheck`) | Unit tests (`test`) | Apalache (`verify`) |
 |---------|:----------------:|:-------------------:|:-------------------:|:-------------------:|
 | [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :x: | :x: | :x: |
+| [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/581</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/581</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/581</sup> |
 | [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
+| [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [classic/sequential/BinSearch/BinSearch10.qnt](./classic/sequential/BinSearch/BinSearch10.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [cosmos/ics20/bank.qnt](./cosmos/ics20/bank.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics20/base.qnt](./cosmos/ics20/base.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
+| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693,</sup><sup>https://github.com/informalsystems/quint/pull/975</sup> |
 | [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
 | [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
 | [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
-| [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [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: |
+| [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> |
+| [cosmwasm/zero-to-hero/vote.qnt](./cosmwasm/zero-to-hero/vote.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
 | [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: | :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: |
@@ -77,20 +76,22 @@ listed without any additional command line arguments.
 | [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/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/option.qnt](./language-features/option.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/244</sup> |
 | [language-features/records.qnt](./language-features/records.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [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: |
+| [language-features/tuples.qnt](./language-features/tuples.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/apalache/issues/2670</sup> |
 | [puzzles/prisoners/prisoners.qnt](./puzzles/prisoners/prisoners.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/tictactoe/tictactoe.qnt](./puzzles/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/Coin/coin.qnt](./solidity/Coin/coin.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1019</sup> |
+| [solidity/SimpleAuction/SimpleAuction.qnt](./solidity/SimpleAuction/SimpleAuction.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [solidity/SimplePonzi/simplePonzi.qnt](./solidity/SimplePonzi/simplePonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [spells/commonSpells.qnt](./spells/commonSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
-| [spells/rareSpells.qnt](./spells/rareSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
+| [spells/basicSpells.qnt](./spells/basicSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [spells/commonSpells.qnt](./spells/commonSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
+| [spells/rareSpells.qnt](./spells/rareSpells.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
 | [verification/defaultOpNames.qnt](./verification/defaultOpNames.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+
+[^nostatemachine]: This specification does not define a state machine.
diff --git a/examples/classic/sequential/BinSearch/BinSearch.qnt b/examples/classic/sequential/BinSearch/BinSearch.qnt
@@ -165,3 +165,12 @@ module BinSearch {
       { not(isTerminated) implies
           ((low <= high) implies INPUT_SEQ.indices().contains(mid + 1)) }
 }
+
+// an instance of binary search
+module BinSearch10 {
+  import BinSearch(
+    INPUT_SEQ=[ 1, 2, 3, 4, 5, 6, 8, 9, 10, 33 ],
+    INPUT_KEY=7,
+    INT_WIDTH=16
+  ).*
+}
diff --git a/examples/classic/sequential/BinSearch/BinSearch10.qnt b/examples/classic/sequential/BinSearch/BinSearch10.qnt
diff --git a/examples/language-features/tuples.qnt b/examples/language-features/tuples.qnt
@@ -1,12 +1,12 @@
-module Tuples {
+module tuples {
   var myTup: (int, str)
 
   def combineTuples(t1, t2) = (t1._1, t2._2)
   val combined = combineTuples((true, 1, 2), (false, 2, 2))
 
-  action Init = myTup' = (0, "hello")
+  action init = myTup' = (0, "hello")
 
-  action Next = myTup' = combineTuples(myTup, (1, "world"))
+  action step = myTup' = combineTuples(myTup, (1, "world"))
 
   // Unpacking
   var x: int

diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md
@@ -36,13 +36,13 @@ error: Configuration error (see the manual): Operator invalidInit not found (use
 ## Successful verification
 
 
-### Can verify `../examples/classic/sequential/BinSearch/BinSearch10.qnt`
+### Can verify `../examples/classic/sequential/BinSearch/BinSearch.qnt`
 
 Contains an import + const instantiation.
 
-<!-- !test check can check BinSearch10.qnt -->
+<!-- !test check can check BinSearch.qnt -->
 ```
-quint verify --invariant=Postcondition ../examples/classic/sequential/BinSearch/BinSearch10.qnt
+quint verify --invariant=Postcondition --main=BinSearch10 ../examples/classic/sequential/BinSearch/BinSearch.qnt
 ```
 
 ### Default `step` and `init` operators are found

diff --git a/quint/cli-tests.md b/quint/cli-tests.md
@@ -278,13 +278,13 @@ fi
       --invariant=noBuyInDrawingInv --main=lotteryMempool \
       ../examples/solidity/icse23-fig7/lottery.qnt
 
-### OK on run BinSearch10
+### OK on run BinSearch
 
 <!-- !test exit 0 -->
 <!-- !test check BinSearch - Run -->
     quint run --max-samples=10000 --max-steps=10 \
-      --invariant=Postcondition \
-      ../examples/classic/sequential/BinSearch/BinSearch10.qnt
+      --invariant=Postcondition --main=BinSearch10 \
+      ../examples/classic/sequential/BinSearch/BinSearch.qnt
 
 ### OK on test simplePonzi
 

diff --git a/quint/io-cli-tests.md b/quint/io-cli-tests.md
@@ -80,12 +80,12 @@ jq '.modules[0].name, .table."7".reference' < parse-out-example.json
 rm parse-out-example.json
 ```
 
-`"Tuples"` is the name of the module given in the IR and 5 is the reference for
+`"tuples"` is the name of the module given in the IR and 5 is the reference for
 in the lookup table for the expression with ID 7:
 
 <!-- !test out module AST is output -->
 ```
-"Tuples"
+"tuples"
 5
 ```