diff --git a/Makefile b/Makefile index 1078c247f7..1327589cec 100644 --- a/Makefile +++ b/Makefile @@ -133,10 +133,8 @@ test-trace: # Note: this is *not* using the Quint models to test the system, # this tests/verifies the Quint models *themselves*. verify-models: - quint test tests/mbt/model/ccv_test.qnt;\ - quint test tests/mbt/model/ccv_model.qnt;\ - quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200;\ - quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" tests/mbt/model/ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 + cd tests/mbt/model;\ + ../run_invariants.sh diff --git a/tests/mbt/driver/core.go b/tests/mbt/driver/core.go index b9a4293df1..803cd486f1 100644 --- a/tests/mbt/driver/core.go +++ b/tests/mbt/driver/core.go @@ -76,6 +76,10 @@ func (s *Driver) providerChain() *ibctesting.TestChain { return s.chain("provider") } +func (s *Driver) providerHeight() int64 { + return s.providerChain().CurrentHeader.Height +} + func (s *Driver) providerCtx() sdk.Context { return s.providerChain().GetContext() } diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index 183839dc9a..df748ea11f 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/tests/mbt/driver/mbt_test.go @@ -179,17 +179,25 @@ func RunItfTrace(t *testing.T, path string) { nodes[i] = addressMap[valName] } + // very hacky: the system produces a lot of extra blocks, e.g. when setting up consumer chains, when updating clients, etc. + // to be able to compare the model to the system, we make the blocks per epoch a very large number (such that an epoch never ends naturally in the system while running the trace) + // When an epoch in the model ends (which we can detect by the height modulo the epoch length), we produce many, many blocks in the system, such that an epoch actually ends. + blocksPerEpoch := int64(200) + modelBlocksPerEpoch := params["BlocksPerEpoch"].Value.(int64) + driver := newDriver(t, nodes, valNames) driver.DriverStats = &stats driver.setupProvider(modelParams, valSet, signers, nodes, valNames) - - // set `BlocksPerEpoch` to 10: a reasonable small value greater than 1 that prevents waiting for too - // many blocks and slowing down the tests providerParams := driver.providerKeeper().GetParams(driver.providerCtx()) - providerParams.BlocksPerEpoch = 10 + providerParams.BlocksPerEpoch = blocksPerEpoch driver.providerKeeper().SetParams(driver.providerCtx(), providerParams) + // begin enough blocks to end the first epoch + for i := int64(1); i < blocksPerEpoch; i++ { + driver.endAndBeginBlock("provider", 1*time.Nanosecond) + } + // remember the time offsets to be able to compare times to the model // this is necessary because the system needs to do many steps to initialize the chains, // which is abstracted away in the model @@ -200,8 +208,16 @@ func RunItfTrace(t *testing.T, path string) { t.Log("Reading the trace...") for index, state := range trace.States { + t.Log("Height modulo epoch length:", driver.providerChain().CurrentHeader.Height%blocksPerEpoch) + t.Log("Model height modulo epoch length:", ProviderHeight(state.VarValues["currentState"].Value.(itf.MapExprType))%modelBlocksPerEpoch) t.Logf("Reading state %v of trace %v", index, path) + // store the height of the provider state before each step. + // The height should only pass an epoch when it passes an epoch in the model, too, + // otherwise there is an error, and blocksPerEpoch needs to be increased. + // See the comment for blocksPerEpoch above. + heightBeforeStep := driver.providerHeight() + trace := state.VarValues["trace"].Value.(itf.ListExprType) // lastAction will get the last action that was executed so far along the model trace, // i.e. the action we should perform before checking model vs actual system equivalence @@ -239,22 +255,33 @@ func RunItfTrace(t *testing.T, path string) { stats.numStartedChains += len(consumersToStart) stats.numStops += len(consumersToStop) + // get the block height in the model + modelHeight := ProviderHeight(currentModelState) + + if modelHeight%modelBlocksPerEpoch == 0 { + // in the model, an epoch ends, so we need to produce blocks in the system to get the actual height + // to end an epoch with the first of the two subsequent calls to endAndBeginBlock below + actualHeight := driver.providerHeight() + + heightInEpoch := actualHeight % blocksPerEpoch + + // produce blocks until the next block ends the epoch + for i := heightInEpoch; i < blocksPerEpoch; i++ { + driver.endAndBeginBlock("provider", 1*time.Nanosecond) + } + } + // we need at least 2 blocks, because for a packet sent at height H, the receiving chain // needs a header of height H+1 to accept the packet - // so, we do `blocksPerEpoch` time advancements with a very small increment, - // and then increment the rest of the time + // so, we do two blocks, one with a very small increment, + // and then another to increment the rest of the time runningConsumersBefore := driver.runningConsumers() - // going through `blocksPerEpoch` blocks to take into account an epoch - blocksPerEpoch := driver.providerKeeper().GetBlocksPerEpoch(driver.providerCtx()) - for i := int64(0); i < blocksPerEpoch; i = i + 1 { - driver.endAndBeginBlock("provider", 1*time.Nanosecond) - } + driver.endAndBeginBlock("provider", 1*time.Nanosecond) for _, consumer := range driver.runningConsumers() { UpdateProviderClientOnConsumer(t, driver, consumer.ChainId) } - - driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-time.Nanosecond*time.Duration(blocksPerEpoch)) + driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) runningConsumersAfter := driver.runningConsumers() @@ -436,6 +463,14 @@ func RunItfTrace(t *testing.T, path string) { stats.EnterStats(driver) + // should not have ended an epoch, unless we also ended an epoch in the model + heightAfterStep := driver.providerHeight() + + if heightBeforeStep/blocksPerEpoch != heightAfterStep/blocksPerEpoch { + // we changed epoch during this step, so ensure that the model also changed epochs + require.True(t, ProviderHeight(state.VarValues["currentState"].Value.(itf.MapExprType))%modelBlocksPerEpoch == 0, "Height in model did not change epoch, but did in system. increase blocksPerEpoch in the system") + } + t.Logf("State %v of trace %v is ok!", index, path) } t.Log("🟢 Trace is ok!") diff --git a/tests/mbt/driver/model_viewer.go b/tests/mbt/driver/model_viewer.go index ed090b2b86..f1f786c4f0 100644 --- a/tests/mbt/driver/model_viewer.go +++ b/tests/mbt/driver/model_viewer.go @@ -40,6 +40,10 @@ func RunningTime(curStateExpr itf.MapExprType, chain string) int64 { return ChainState(curStateExpr, chain)["runningTimestamp"].Value.(int64) } +func ProviderHeight(curStateExpr itf.MapExprType) int64 { + return ProviderState(curStateExpr)["chainState"].Value.(itf.MapExprType)["currentBlockHeight"].Value.(int64) +} + // PacketQueue returns the queued packets between sender and receiver. // Either sender or receiver need to be the provider. func PacketQueue(curStateExpr itf.MapExprType, sender, receiver string) itf.ListExprType { diff --git a/tests/mbt/driver/setup.go b/tests/mbt/driver/setup.go index 69b385cb77..c0020a4095 100644 --- a/tests/mbt/driver/setup.go +++ b/tests/mbt/driver/setup.go @@ -397,22 +397,6 @@ func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestC // their channel, and are ready for anything to happen. s.consumerKeeper(consumerChainId).SetProviderChannel(s.ctx(consumerChainId), consumerEndPoint.ChannelID) - // Commit a block on both chains, giving us two committed headers from - // the same time and height. This is the starting point for all our - // data driven testing. - lastConsumerHeader, _ := simibc.EndBlock(consumerChain, func() {}) - lastProviderHeader, _ := simibc.EndBlock(providerChain, func() {}) - - // Get ready to update clients. - simibc.BeginBlock(providerChain, 5) - simibc.BeginBlock(consumerChain, 5) - - // Update clients to the latest header. - err = simibc.UpdateReceiverClient(consumerEndPoint, providerEndPoint, lastConsumerHeader, false) - require.NoError(s.t, err, "Error updating client on consumer for chain %v", consumerChain.ChainID) - err = simibc.UpdateReceiverClient(providerEndPoint, consumerEndPoint, lastProviderHeader, false) - require.NoError(s.t, err, "Error updating client on provider for chain %v", consumerChain.ChainID) - // path is ready to go return path } diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 0e42436c50..2a81fe3a2d 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -58,6 +58,8 @@ module ccv_types { // the running timestamp of the current block (that will be put on chain when the block is ended) runningTimestamp: Time, + + currentBlockHeight: int, } // utility function: returns a chain state that is initialized minimally. @@ -67,6 +69,7 @@ module ccv_types { currentValidatorSet: Map(), lastTimestamp: -1, // last timestamp -1 means that in the model, there was no block committed on chain yet. runningTimestamp: 0, + currentBlockHeight: 0 } // Defines the current state of the provider chain. Essentially, all information here is stored by the provider on-chain (or could be derived purely by information that is on-chain). @@ -86,11 +89,8 @@ module ccv_types { // Stores VscPackets which have been sent but where the provider has *not received a response yet*. sentVscPacketsToConsumer: Chain -> List[VscPacket], - // stores whether, in this block, the validator set has changed. - // this is needed because the validator set might be considered to have changed, even though - // it is still technically identical at our level of abstraction, e.g. a validator power change on the provider - // might leave the validator set the same because a delegation and undelegation cancel each other out. - providerValidatorSetChangedInThisBlock: bool, + // stores for which consumer chains, in this epoch, the validator set is considered to have changed and we thus need to send a VscPacket to the consumer chains. + consumersWithPowerChangesInThisEpoch: Set[Chain], // stores, for each consumer chain, its current status - // not consumer, running, or stopped @@ -110,7 +110,7 @@ module ccv_types { consumerAddrToValidator: Chain -> (ConsumerAddr -> Node), // For every consumer chain, stores whether the key assignment for the consumer chain has changed in this block. - consumersWithAddrAssignmentChangesInThisBlock: Set[Chain], + consumersWithAddrAssignmentChangesInThisEpoch: Set[Chain], // the history of validator sets on the provider, but with the key assignments applied. // This is needed to check invariants about the validator set when key assignments are in play. @@ -130,7 +130,7 @@ module ccv_types { outstandingPacketsToConsumer: Map(), receivedMaturations: Set(), sentVscPacketsToConsumer: Map(), - providerValidatorSetChangedInThisBlock: false, + consumersWithPowerChangesInThisEpoch: Set(), consumerStatus: Map(), runningVscId: 0, validatorToConsumerAddr: Map(), @@ -138,7 +138,7 @@ module ccv_types { consumerAddrToValidator: Map(), consumerAddrsToPrune: Map(), keyAssignmentsForVSCPackets: Map(), - consumersWithAddrAssignmentChangesInThisBlock: Set() + consumersWithAddrAssignmentChangesInThisEpoch: Set() } @@ -271,6 +271,10 @@ module ccv { // they expire and the channel will be closed. const TrustingPeriodPerChain: Chain -> int + // The number of blocks in an epoch. + // VscPackets are only sent to consumer chains at the end of every epoch. + const BlocksPerEpoch: int + // =================== // PROTOCOL LOGIC contains the meat of the protocol // functions here roughly correspond to API calls that can be triggered from external sources @@ -294,7 +298,7 @@ module ccv { } else { // set the validator set changed flag val newProviderState = currentState.providerState.with( - "providerValidatorSetChangedInThisBlock", true + "consumersWithPowerChangesInThisEpoch", getRunningConsumers(currentState.providerState) ) pure val tmpState = currentState.with( "providerState", newProviderState @@ -455,10 +459,16 @@ module ccv { // send vsc packets (will be a noop if no sends are necessary) val providerStateAfterSending = - providerStateAfterTimeAdvancement.sendVscPackets( - currentProviderState.chainState.runningTimestamp, - CcvTimeout.get(PROVIDER_CHAIN) - ) + // if currentBlockHeight is a multiple of BlocksPerEpoch, send VscPackets + if (providerStateAfterTimeAdvancement.chainState.currentBlockHeight % BlocksPerEpoch == 0) { + providerStateAfterTimeAdvancement.sendVscPackets( + currentProviderState.chainState.runningTimestamp, + CcvTimeout.get(PROVIDER_CHAIN) + ) + } else { + // otherwise, just do a noop + providerStateAfterTimeAdvancement + } // start/stop chains @@ -471,8 +481,6 @@ module ccv { val err = res._2 val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( "consumerStatus", newConsumerStatus - ).with( - "providerValidatorSetChangedInThisBlock", false ) if (err != "") { @@ -609,17 +617,17 @@ module ccv { // check whether the validator has positive power pure val provValSet = currentState.providerState.chainState.currentValidatorSet pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0 - pure val consumersWithAddrAssignmentChangesInThisBlock = + pure val consumersWithAddrAssignmentChangesInThisEpoch = if (provValPower > 0) { // if the consumer has positive power, the relevant key assignment for the consumer changed - currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock.union(Set(consumer)) + currentState.providerState.consumersWithAddrAssignmentChangesInThisEpoch.union(Set(consumer)) } else { // otherwise, the consumer doesn't need to know about the change, so no change - currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock + currentState.providerState.consumersWithAddrAssignmentChangesInThisEpoch } pure val tmpStateAfterKeyAssignmentReplacement = tmpState.with( "providerState", tmpState.providerState.with( - "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock + "consumersWithAddrAssignmentChangesInThisEpoch", consumersWithAddrAssignmentChangesInThisEpoch ) ) diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index f997198b6e..1509ad439f 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -13,6 +13,7 @@ module ccv_model { pure val unbondingPeriods = chains.mapBy(chain => defUnbondingPeriod) pure val trustingPeriods = chains.mapBy(chain => defUnbondingPeriod - 1 * Hour) pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) + pure val epochLength = 3 pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10") // possible consumer addresses that nodes can assign their key to @@ -24,7 +25,8 @@ module ccv_model { CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, - TrustingPeriodPerChain = trustingPeriods + TrustingPeriodPerChain = trustingPeriods, + BlocksPerEpoch = epochLength ).* from "./ccv" type Parameters = { @@ -36,6 +38,7 @@ module ccv_model { Nodes: Set[Node], ConsumerAddresses: Set[ConsumerAddr], InitialValidatorSet: Node -> int, + BlocksPerEpoch: int, } // The params variable is never actually changed, and @@ -129,6 +132,7 @@ module ccv_model { InitialValidatorSet: InitialValidatorSet, TrustingPeriodPerChain: TrustingPeriodPerChain, ConsumerAddresses: consumerAddresses, + BlocksPerEpoch: epochLength, } } @@ -235,6 +239,25 @@ module ccv_model { stepCommon } + // Runs epochLength many blocks on the provider. + // The first block will start all consumers in consumersToStart and stop all consumers in consumersToStop, + // and advance time by timeAdvancement - ((epochLength-1) * Seconds). + // The rest of the blocks will not start or stop any consumers, and will advance time by 1 second each. + // As a a `Run`, it is only used in tests, not during simulation or verification. + run EndProviderEpoch( + timeAdvancement: Time, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain] + ): bool = + epochLength.reps( + i => + if (i == 0) { + EndAndBeginBlockForProvider(timeAdvancement-((epochLength-1)*Second), consumersToStart, consumersToStop) + } else { + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + } + ) + // ================== // UTILITY FUNCTIONS // ================== @@ -319,16 +342,19 @@ module ccv_model { ) ) + + val CurrentBlockEndsEpoch = currentState.providerState.chainState.currentBlockHeight % epochLength == 0 + // 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].kind == "EndAndBeginBlockForProvider" val ValidatorUpdatesArePropagatedInv = - // when the provider has just entered a validator set into a block... - ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock + // when the an epoch ends and the provider has just entered a validator set into a block... + ValUpdatePrecondition and CurrentBlockEndsEpoch implies val providerValSetInCurBlock = providerValidatorHistory.head() - // ... for each consumer that is running then ... - runningConsumers.forall( + // ... for each consumer for which we need to send a vsc packet ... + currentState.providerState.consumersWithPowerChangesInThisEpoch.forall( // ...the validator set is in a sent packet... consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( packet => packet.validatorSet == providerValSetInCurBlock @@ -517,9 +543,10 @@ module ccv_model { assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)), // change voting power on provider again VotingPowerChange("node1", 50).then( - // end another block - EndAndBeginBlockForProvider(1 * Second, Set(), Set()) - ).then( + // end the epoch + EndProviderEpoch(epochLength * Second, Set(), Set()) + ) + .then( // deliver packet to consumer1 DeliverVscPacket("consumer1") ) @@ -588,7 +615,7 @@ module ccv_model { VotingPowerChange("node1", 50) ).then( // send packet to consumer1 and consumer2 - EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + EndProviderEpoch(epochLength * Second, Set(), Set()) ).then( // deliver the packets DeliverVscPacket("consumer1") @@ -603,7 +630,7 @@ module ccv_model { VotingPowerChange("node2", 50) ).then( // send packets - EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + EndProviderEpoch(epochLength * Second, Set(), Set()) ).then( //deliver to consumer1 DeliverVscPacket("consumer1") @@ -636,7 +663,7 @@ module ccv_model { ) .then( // send packets - EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + EndProviderEpoch(epochLength * Second, Set(), Set()) ) .then( // advance time on provider by VscTimeout + 1 Second @@ -715,11 +742,11 @@ module ccv_model { // and the key assignment of each validator should be applied in that VSCPacket. val ValidatorUpdatesArePropagatedKeyAssignmentInv = // when the provider has just entered a validator set into a block... - ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock + ValUpdatePrecondition and CurrentBlockEndsEpoch implies val providerValSetInCurBlock = providerValidatorHistory.head() // ... for each consumer that is running then ... - runningConsumers.forall( + currentState.providerState.consumersWithPowerChangesInThisEpoch.forall( // ...the validator set under key assignment is in a sent packet... val providerState = currentState.providerState consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( @@ -849,7 +876,7 @@ module ccv_model { ) .then( // end and begin block to make sure the key assignment is processed and the packet is sent - EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + EndProviderEpoch(epochLength * Second, Set(), Set()) ) .then( // receive the packet on the consumer diff --git a/tests/mbt/model/ccv_test.qnt b/tests/mbt/model/ccv_test.qnt index 62ab03b5e0..ab47df50b7 100644 --- a/tests/mbt/model/ccv_test.qnt +++ b/tests/mbt/model/ccv_test.qnt @@ -12,8 +12,9 @@ module ccv_test { pure val unbondingPeriods = chains.mapBy(chain => 2 * Week) pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) pure val trustingPeriods = chains.mapBy(chain => 2 * Week - 1 * Hour) + pure val epochLength = 3 - import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain=trustingPeriods).* from "./ccv" + import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain=trustingPeriods, BlocksPerEpoch=epochLength).* from "./ccv" val votingPowerTestInitState = GetEmptyProtocolState.with( @@ -25,6 +26,10 @@ module ccv_test { "validator2", 5 ) ) + ).with( + "consumerStatus", Map( + "consumer" -> RUNNING + ) ) ) @@ -78,7 +83,7 @@ module ccv_test { ) // still should set the flag not(finalResult.hasError()) and - finalResult.newState.providerState.providerValidatorSetChangedInThisBlock + finalResult.newState.providerState.consumersWithPowerChangesInThisEpoch.contains("consumer") } diff --git a/tests/mbt/model/ccv_utils.qnt b/tests/mbt/model/ccv_utils.qnt index 4d881828ef..476ef923dc 100644 --- a/tests/mbt/model/ccv_utils.qnt +++ b/tests/mbt/model/ccv_utils.qnt @@ -183,9 +183,16 @@ module ccv_utils { runningTimestamp: chainState.runningTimestamp + timeAdvancement, } + pure def incrementBlockHeight(chainState: ChainState): ChainState = + { + chainState.with( + "currentBlockHeight", chainState.currentBlockHeight + 1 + ) + } + // common logic to update the chain state, used by both provider and consumers. pure def endAndBeginBlockShared(chainState: ChainState, timeAdvancement: Time): ChainState = { - chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement) + chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement).incrementBlockHeight() } // returns the providerState with the following modifications: @@ -201,8 +208,8 @@ module ccv_utils { val newSentPacketsPerConsumer = providerState.getConsumers().mapBy( // compute, for each consumer, a list of new packets to be sent (consumer) => // if validator set changed or the key assignments for this chain changed, and the consumer is running, send a packet - if ((providerState.providerValidatorSetChangedInThisBlock or - providerState.consumersWithAddrAssignmentChangesInThisBlock.contains(consumer)) + if ((providerState.consumersWithPowerChangesInThisEpoch.contains(consumer) or + providerState.consumersWithAddrAssignmentChangesInThisEpoch.contains(consumer)) and isRunningConsumer(consumer, providerState)) { // send a packet, i.e. use a list with one element (the packet to be sent) @@ -240,8 +247,8 @@ module ccv_utils { runningVscId: providerState.runningVscId + 1, // we ended the block and processed that the valset or key assignments changed, // so reset the flags - providerValidatorSetChangedInThisBlock: false, - consumersWithAddrAssignmentChangesInThisBlock: Set(), + consumersWithPowerChangesInThisEpoch: Set(), + consumersWithAddrAssignmentChangesInThisEpoch: Set(), // remember the key assignments that were applied to send the packets keyAssignmentsForVSCPackets: providerState.keyAssignmentsForVSCPackets.put( providerState.runningVscId, diff --git a/tests/mbt/run_invariants.sh b/tests/mbt/run_invariants.sh index df22b97702..afe079387e 100755 --- a/tests/mbt/run_invariants.sh +++ b/tests/mbt/run_invariants.sh @@ -1,6 +1,41 @@ #!/bin/bash +# to stop on any errors +set -e + quint test ccv_model.qnt quint test ccv_test.qnt quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 -quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 \ No newline at end of file +quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 + + +# do not stop on errors anymore, so we can give better output if we error +set +e + +run_invariant() { + local invariant=$1 + local step=$2 + local match=$3 + + if [[ -z "$step" ]]; then + quint run --invariant $invariant ccv_model.qnt | grep -q $match + else + quint run --invariant $invariant --step $step ccv_model.qnt | grep -q $match + fi + + if [[ $? -eq 0 ]]; then + echo "sanity check $invariant ok" + else + echo "sanity check $invariant not ok" + exit 1 + fi +} + +run_invariant "CanRunConsumer" "" '[violation]' +run_invariant "CanStopConsumer" "" '[violation]' +run_invariant "CanTimeoutConsumer" "" '[violation]' +run_invariant "CanSendVscPackets" "" '[violation]' +run_invariant "CanSendVscMaturedPackets" "" '[violation]' +run_invariant "CanAssignConsumerKey" "stepKeyAssignment" '[violation]' +run_invariant "CanHaveConsumerAddresses" "stepKeyAssignment" '[violation]' +run_invariant "CanReceiveMaturations" "stepKeyAssignment" '[violation]' \ No newline at end of file