diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
index a891b2f04..268879b89 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" ||
@@ -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
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.
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
+ ).*
+}