Add Inv to ValidatorUpdatesArePropagated

cosmos · Oct 6, 2023 · 7cd826b · 7cd826b
1 parent 2000272
commit 7cd826b
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
+quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log
Original file line number	Diff line number	Diff line change
		@@ -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
		quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log