From 436aec4136a48adba0a0f33287ccc20dd4b8c520 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Thu, 23 Nov 2023 13:12:45 +0100 Subject: [PATCH] Remove message sends for consumers that were started in this block --- tests/difference/core/quint_model/ccv.qnt | 77 ++++++++++--------- .../difference/core/quint_model/ccv_model.qnt | 22 ++++-- 2 files changed, 55 insertions(+), 44 deletions(-) diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index be7bc74efc..86d34d7334 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -399,60 +399,61 @@ module ccv { res._1 ) + // send vsc packets + val providerStateAfterSending = + if (currentProviderState.providerValidatorSetChangedInThisBlock and + // important: check this on the provider state after the consumer advancement, not on the current state. + getRunningConsumers(providerStateAfterTimeAdvancement).size() > 0) { + providerStateAfterTimeAdvancement.sendVscPackets() + } else { + providerStateAfterTimeAdvancement + } + // start/stop chains - val res = providerStateAfterTimeAdvancement.consumerStatus.StartStopConsumers( + val res = providerStateAfterSending.consumerStatus.StartStopConsumers( consumersToStart, consumersToStop, timedOutConsumers ) val newConsumerStatus = res._1 val err = res._2 - val providerStateAfterConsumerAdvancement = providerStateAfterTimeAdvancement.with( + val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( "consumerStatus", newConsumerStatus - ) - - // for each consumer we just set to running, set its initial validator set to be the current one on the provider. - val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet - val newConsumerStateMap = - tmpState.consumerStates.keys().mapBy( - (consumer) => - if (consumersToStart.contains(consumer)) { - val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) - val newConsumerState: ConsumerState = currentConsumerState.with( - "chainState", currentConsumerState.chainState.with( - "currentValidatorSet", valSet - ).with( - "votingPowerHistory", - List(valSet) - ) - ) - newConsumerState - } else { - currentState.consumerStates.get(consumer) - } - ) - val newState = tmpState.with( - "providerState", providerStateAfterConsumerAdvancement ).with( - "consumerStates", newConsumerStateMap + "providerValidatorSetChangedInThisBlock", false ) if (err != "") { Err(err) } else { - val providerStateAfterSending = - if (currentProviderState.providerValidatorSetChangedInThisBlock and - // important: check this on the provider state after the consumer advancement, not on the current state. - getRunningConsumers(providerStateAfterConsumerAdvancement).size() > 0) { - providerStateAfterConsumerAdvancement.sendVscPackets() - } else { - providerStateAfterConsumerAdvancement - } - val finalState = newState.with( - "providerState", providerStateAfterSending + // for each consumer we just set to running, set its initial validator set to be the current one on the provider. + val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet + val newConsumerStateMap = + tmpState.consumerStates.keys().mapBy( + (consumer) => + if (consumersToStart.contains(consumer)) { + val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) + val newConsumerState: ConsumerState = currentConsumerState.with( + "chainState", currentConsumerState.chainState.with( + "currentValidatorSet", valSet + ).with( + "votingPowerHistory", + List(valSet) + ) + ) + newConsumerState + } else { + currentState.consumerStates.get(consumer) + } + ) + val newState = tmpState.with( + "providerState", providerStateAfterConsumerAdvancement + ).with( + "consumerStates", newConsumerStateMap ) - Ok(finalState) + + Ok(newState) } } diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt index b580be32a5..45035ddfdd 100644 --- a/tests/difference/core/quint_model/ccv_model.qnt +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -299,10 +299,14 @@ module ccv_model { val providerValSetInCurBlock = providerValidatorHistory.head() // ... for each consumer that is running then ... runningConsumers.forall( - // ...the validator set is in a sent packet + // ...the validator set is in a sent packet... consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( packet => packet.validatorSet == providerValSetInCurBlock ) + // or the consumer was just started, which we detect by the consumer having a timestamp of 0 + // and the consumer having the validator set that was just sent in the block + or + (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock) ) // Every consumer chain receives the same sequence of @@ -476,12 +480,18 @@ module ccv_model { all { // consumer1 was started assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING), - // a packet was sent to consumer1 - assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 1), + // but no packet was sent to consumer 1 + assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0), // the validator set on the provider was entered into the history assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)), - // deliver the packet - DeliverVscPacket("consumer1") + // change voting power on provider again + VotingPowerChange("node1", 50).then( + // end another block + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ).then( + // deliver packet to consumer1 + DeliverVscPacket("consumer1") + ) } ) .then( @@ -491,7 +501,7 @@ module ccv_model { // ensure the maturation time was entered on the consumer assert(currentState.consumerStates.get("consumer1").maturationTimes.length() == 1), // the validator set was put as the current validator set - assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)), + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 200)), // advance time on provider until the unbonding period is over EndAndBeginBlockForProvider(UnbondingPeriodPerChain.get("consumer1"), Set(), Set()), }