From 23a78760f3bc7547c22c2ae227309e21f2b87e2b Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 26 Jul 2023 15:24:45 +0200 Subject: [PATCH 1/4] Mark parameterized modules as N/A in dashboard --- examples/.scripts/run-example.sh | 8 ++++++++ examples/.scripts/run-examples.sh | 1 + examples/README.md | 5 +++-- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index a891b2f04..d4a5ae004 100755 --- 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" || diff --git a/examples/.scripts/run-examples.sh b/examples/.scripts/run-examples.sh index 25a83666b..50c26d1c5 100755 --- 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 index 604e33a2c..3f7d993bc 100644 --- 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:https://github.com/informalsystems/quint/issues/693 | | [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:https://github.com/informalsystems/quint/issues/693,https://github.com/informalsystems/quint/pull/975 | -| [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:https://github.com/informalsystems/quint/pull/1023 | :x:https://github.com/informalsystems/quint/pull/1023 | @@ -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. From 01f9637e649e19210ab71ca74a2a475c0f7b1eb5 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Thu, 27 Jul 2023 09:40:14 +0200 Subject: [PATCH 2/4] Fix verify args for lightclient spec --- examples/.scripts/run-example.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index d4a5ae004..a6a34d713 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -103,9 +103,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}" From 8145fc0bb8382724e8c554b50423c524c2632c9f Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 28 Jul 2023 10:28:07 +0200 Subject: [PATCH 3/4] Add instance to Lightclient spec --- examples/cosmos/lightclient/Lightclient.qnt | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/examples/cosmos/lightclient/Lightclient.qnt b/examples/cosmos/lightclient/Lightclient.qnt index 20a5dfcff..77073ce77 100644 --- 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 + ).* +} From a0c92a319275ce1687588d4bd74c0d8bbb05325f Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Fri, 28 Jul 2023 10:51:29 +0200 Subject: [PATCH 4/4] Add --main for Lightclient.qnt --- examples/.scripts/run-example.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh index a6a34d713..268879b89 100755 --- a/examples/.scripts/run-example.sh +++ b/examples/.scripts/run-example.sh @@ -79,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