From 7cd826bb8ba3990fe4384e81a423c24db8524c6b Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 6 Oct 2023 08:49:27 +0200 Subject: [PATCH] Add Inv to ValidatorUpdatesArePropagated --- tests/difference/core/quint_model/README.md | 4 ++-- tests/difference/core/quint_model/ccv_statemachine.qnt | 2 +- tests/difference/core/quint_model/run_invariants.sh | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md index a2f66945b4..4a36b4976b 100644 --- a/tests/difference/core/quint_model/README.md +++ b/tests/difference/core/quint_model/README.md @@ -38,7 +38,7 @@ or all invariants one after another with the help of the script `run_invariants. Each invariant takes about a minute to run. Invariants are as follows: -- [X] ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. +- [X] ValidatorUpdatesArePropagatedInv: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. - [X] ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider. - [X] SameVSCPacketsInv: Ensure that consumer chains receive the same VSCPackets in the same order. Because of nuances with starting/stopping consumers, this invariant is not as simple as it sounds. In detail: @@ -52,7 +52,7 @@ that were running at the time the packet was sent (and are still running). Invariants can also be model-checked by Apalache, using this command: ``` -quint verify --invariant ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ +quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ --main CCVDefaultStateMachine ccv_statemachine.qnt ``` diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt index b4229c05e0..51edafcf58 100644 --- a/tests/difference/core/quint_model/ccv_statemachine.qnt +++ b/tests/difference/core/quint_model/ccv_statemachine.qnt @@ -170,7 +170,7 @@ module CCVDefaultStateMachine { // Any update in the power of a validator on the provider // MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains val ValUpdatePrecondition = trace[trace.length()-1] == "EndAndBeginBlockForProvider" - val ValidatorUpdatesArePropagated = + val ValidatorUpdatesArePropagatedInv = // when the provider has just entered a validator set into a block... if (ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock) { val providerValSetInCurBlock = providerValidatorHistory.head() diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh index 5ea6b3d387..142095682f 100755 --- a/tests/difference/core/quint_model/run_invariants.sh +++ b/tests/difference/core/quint_model/run_invariants.sh @@ -1 +1 @@ -quint run --invariant "all{ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log \ No newline at end of file +quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log \ No newline at end of file