diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index df994b7f84..dac613337e 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -138,4 +138,8 @@ The available sanity checks are: - CanOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) - CanOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) - CanFailOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +<<<<<<< HEAD - CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +======= +- CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +>>>>>>> 6e075652 (test: MBT: Add partial set security to model (feature branch version) (#1627)) diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index b067ca79b2..37fcd5a15b 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -115,11 +115,6 @@ module ccv_boundeddrift { StepOptOut, } - action stepBoundedDriftKeyAssignment = any { - stepBoundedDrift, - nondetKeyAssignment, - } - // INVARIANT // The maxDrift between chains is never exceeded. // This *should* be ensured by the step function. diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index b3b487d113..3dc0ea1861 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -740,11 +740,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 CurrentBlockEndsEpoch + ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock implies val providerValSetInCurBlock = providerValidatorHistory.head() // ... for each consumer that is running then ... - currentState.providerState.consumersWithPowerChangesInThisEpoch.forall( + runningConsumers.forall( // ...the validator set under key assignment is in a sent packet... val providerState = currentState.providerState consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( diff --git a/tests/mbt/model/run_invariants.sh b/tests/mbt/model/run_invariants.sh index afe079387e..e232bcce8b 100755 --- a/tests/mbt/model/run_invariants.sh +++ b/tests/mbt/model/run_invariants.sh @@ -1,5 +1,6 @@ #!/bin/bash +<<<<<<< HEAD # to stop on any errors set -e @@ -38,4 +39,10 @@ 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 +run_invariant "CanReceiveMaturations" "stepKeyAssignment" '[violation]' +======= +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 +>>>>>>> 6e075652 (test: MBT: Add partial set security to model (feature branch version) (#1627))