Merge pull request #1079 from informalsystems/th/fix-ex-lightclient

Update example runner + dashboard for lightclient spec
informalsystems · Jul 31, 2023 · 0fc8fbf · 0fc8fbf
2 parents 1f41cdb + a0c92a3
commit 0fc8fbf
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 5 deletions.
diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
@@ -13,8 +13,16 @@ result () {
     local args="$2"
     local file="$3"
 
+    # Skip tests for parameterized modules
+    if [[ "$cmd" == "test" && (
+            "$file" == "cosmos/lightclient/Blockchain.qnt" ||
+            "$file" == "cosmos/lightclient/LCVerificationApi.qnt" ) ]] ; then
+      printf "N/A[^parameterized]"; return
+    fi
     # Skip verification for specs that do not define a state machine
     if [[ "$cmd" == "verify" && (
+            "$file" == "cosmos/lightclient/Blockchain.qnt" ||
+            "$file" == "cosmos/lightclient/LCVerificationApi.qnt" ||
             "$file" == "cosmos/lightclient/typedefs.qnt" ||
             "$file" =~ ^spells/ ||
             "$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
@@ -71,6 +79,8 @@ get_main () {
     main="--main=properChannelsTests"
   elif [[ "$file" == "cosmos/ics20/ics20.qnt" ]] ; then
     main="--main=ics20Test"
+  elif [[ "$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
+    main="--main=Lightclient_4_3_correct"
   elif [[ "$file" == "puzzles/prisoners/prisoners.qnt" ]] ; then
     main="--main=prisoners3"
   elif [[ "$file" == "solidity/ERC20/erc20.qnt" ]] ; then
@@ -95,9 +105,9 @@ get_test_args () {
 get_verify_args () {
   local file="$1"
   local args=""
-  if [[ "$file" == "classic/distributed/LamportMutex/LamportMutex.qnt" ]] ; then
-    args="--init=Init --step=Next"
-  elif [[ "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ]] ; then
+  if [[ "$file" == "classic/distributed/LamportMutex/LamportMutex.qnt" ||
+        "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ||
+        "$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
     args="--init=Init --step=Next"
   fi
   echo "${args}"

diff --git a/examples/.scripts/run-examples.sh b/examples/.scripts/run-examples.sh
@@ -25,3 +25,4 @@ find . -name "*.qnt" | cut -c3- | parallel "${SCRIPT_DIR}/run-example.sh" | env
 
 echo
 echo "[^nostatemachine]: This specification does not define a state machine."
+echo "[^parameterized]: This specification is parameterized, and instantiated in another module."
diff --git a/examples/README.md b/examples/README.md
@@ -60,8 +60,8 @@ listed without any additional command line arguments.
 | [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:<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/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
+| [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [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: | 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> |
@@ -95,3 +95,4 @@ listed without any additional command line arguments.
 | [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.
+[^parameterized]: This specification is parameterized, and instantiated in another module.
diff --git a/examples/cosmos/lightclient/Lightclient.qnt b/examples/cosmos/lightclient/Lightclient.qnt
@@ -545,3 +545,16 @@ module Lightclient {
     the algorithm has indeed terminated there.
     */
 }
+
+module Lightclient_4_3_correct {
+    import Lightclient(
+        AllNodes = Set("n1", "n2", "n3", "n4"),
+        TRUSTED_HEIGHT = 1,
+        TARGET_HEIGHT = 3,
+        TRUSTING_PERIOD = 1400,   // two weeks, one day is 100 time units :-)
+        CLOCK_DRIFT = 10,         // how much we assume the local clock is drifting
+        REAL_CLOCK_DRIFT = 3,     // how much the local clock is actually drifting
+        IS_PRIMARY_CORRECT = true,
+        FAULTY_RATIO = (1, 3)     // < 1/3 faulty validators
+    ).*
+}