diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index df994b7f84..865fabe016 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -50,12 +50,15 @@ As an optional module, it can also include KeyAssignment. To run with key assignment, specify the step flag: `--step stepKeyAssignment`. KeyAssignment also needs some different invariants, see below. +<<<<<<< HEAD #### Partial Set Security To run with Partial Set Security, specify the step flag `--step stepBoundedDriftKeyAndPSS`. This runs both PSS and Key Assignment. It also requires running with `ccv_boundeddrift.qnt`, see below. +======= +>>>>>>> main #### ccv_boundeddrift.qnt This state machine layer is more restricted to generate more interesting traces: diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 68d08e88a3..6941dc8a73 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -89,12 +89,6 @@ 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], @@ -147,7 +141,6 @@ module ccv_types { outstandingPacketsToConsumer: Map(), receivedMaturations: Set(), sentVscPacketsToConsumer: Map(), - providerValidatorSetChangedInThisBlock: false, consumersWithPowerChangesInThisEpoch: Set(), consumerStatus: Map(), runningVscId: 0, @@ -156,9 +149,9 @@ module ccv_types { consumerAddrToValidator: Map(), consumerAddrsToPrune: Map(), keyAssignmentsForVSCPackets: Map(), - consumersWithAddrAssignmentChangesInThisEpoch: Set(), optedInVals: Map(), topNByConsumer: Map(), + consumersWithAddrAssignmentChangesInThisEpoch: Set() } @@ -510,7 +503,7 @@ module ccv { consumersToStop, timedOutConsumers ) - val providerStateAfterConsumerAdvancement = res._1.with("providerValidatorSetChangedInThisBlock", false) + val providerStateAfterConsumerAdvancement = res._1 val err = res._2 val consumerAdditions = consumersToStart.map(consumer => consumer.chain) diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index b067ca79b2..125de8004e 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -104,6 +104,12 @@ module ccv_boundeddrift { nondet timeAdvancement = possibleAdvancements.oneOf() EndAndBeginBlockForConsumer(chain, timeAdvancement), } +<<<<<<< HEAD + } + + action stepBoundedDriftKeyAssignment = any { + stepBoundedDrift, + nondetKeyAssignment, } action stepBoundedDriftKeyAndPSS = any { @@ -113,6 +119,24 @@ module ccv_boundeddrift { nondetKeyAssignment, StepOptIn, StepOptOut, +======= + }, + + // advance a block for the provider + val maxAdv = findMaxTimeAdvancement(GetChainState(Ccvt::PROVIDER_CHAIN), GetOtherChainStates(Ccvt::PROVIDER_CHAIN), maxDrift) + val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv) + all { + possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense + // advance a block for the provider + val consumerStatus = currentState.providerState.consumerStatus + nondet consumersToStart = oneOf(nonConsumers.powerset()) + // make it so we stop consumers only with small likelihood: + nondet stopConsumersRand = oneOf(1.to(100)) + nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() + nondet timeAdvancement = oneOf(possibleAdvancements) + EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + } +>>>>>>> main } action stepBoundedDriftKeyAssignment = any { diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index a4f1ad4cf3..3061f7039b 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -109,7 +109,7 @@ module ccv_model { val consumerStates = ConsumerChains.mapBy(chain => GetEmptyConsumerState) val providerStateWithConsumers = providerState.with( "consumerStatus", - ConsumerChains.mapBy(chain => NOT_CONSUMER) + ConsumerChains.mapBy(chain => NOT_CONSUMER) ).with( "outstandingPacketsToConsumer", ConsumerChains.mapBy(chain => List()) @@ -255,7 +255,7 @@ module ccv_model { // As a a `Run`, it is only used in tests, not during simulation or verification. run EndProviderEpoch( timeAdvancement: Time, - consumersToStart: Set[ConsumerAdditionMsg], + consumersToStart: Set[Chain], consumersToStop: Set[Chain] ): bool = epochLength.reps( @@ -270,7 +270,6 @@ module ccv_model { // ================== // UTILITY FUNCTIONS // ================== - pure def oldest(packets: Set[VscPacket]): VscPacket = val newestPossiblePacket: VscPacket = { id: 0, @@ -740,11 +739,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(