diff --git a/tests/mbt/driver/generate_more_traces.sh b/tests/mbt/driver/generate_more_traces.sh index 49089c5232..2b9fad2d90 100755 --- a/tests/mbt/driver/generate_more_traces.sh +++ b/tests/mbt/driver/generate_more_traces.sh @@ -5,6 +5,6 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -tr echo "Generating bounded drift traces with maturations" go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 20 -numSteps 100 -numSamples 20 echo "Generating synced traces with maturations" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 20 -numSteps 300 -numSamples 20 +go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 20 -numSteps 300 -numSamples 20 echo "Generating long synced traces without invariants" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1 \ No newline at end of file +go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1 \ No newline at end of file diff --git a/tests/mbt/driver/generate_traces.sh b/tests/mbt/driver/generate_traces.sh index 418d7004dc..e792a2cf3c 100755 --- a/tests/mbt/driver/generate_traces.sh +++ b/tests/mbt/driver/generate_traces.sh @@ -5,6 +5,6 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -tr echo "Generating bounded drift traces with maturations" go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanReceiveMaturations -traceFolder traces/bound_mat -numTraces 1 -numSteps 100 -numSamples 20 echo "Generating synced traces with maturations" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20 +go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20 echo "Generating long synced traces without invariants" -go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepHappy -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1 \ No newline at end of file +go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1 \ No newline at end of file diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 99e1f00229..6080ae9be7 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -622,9 +622,9 @@ module ccv { // Advances the timestamp in the chainState by timeAdvancement pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = { + ...chainState, lastTimestamp: chainState.runningTimestamp, runningTimestamp: chainState.runningTimestamp + timeAdvancement, - ...chainState } // common logic to update the chain state, used by both provider and consumers. diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index b4678b8430..21a53074c0 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -16,6 +16,8 @@ module ccv_boundeddrift { // In particular, it will ensure that the lastTime of any chain // does not differ from the runningTime of any other chain by more than // this value. + // We choose unbondingPeriod - 2 * Hour here, because we want this to be less than the trustingPeriod, + // which is currently defined as unbondingPeriod - 1 * Hour pure val maxDrift = defUnbondingPeriod - 2 * Hour // The chance, in percentage points, that we will stop consumer chains, whenever we begin a block on the provider chain. @@ -54,7 +56,7 @@ module ccv_boundeddrift { // thus the clock times are always in sync. // This is useful to test happy paths. action stepBoundedDrift = any { - step_common, // allow actions that do not influence time + stepCommon, // allow actions that do not influence time // advance a block for a consumer all { @@ -77,7 +79,7 @@ module ccv_boundeddrift { // 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 likelyhood: + // make it so we stop consumers only with small likelihood: nondet stopConsumers = oneOf(1.to(100)) nondet consumersToStop = if (stopConsumers <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() nondet timeAdvancement = oneOf(possibleAdvancements) diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index c1d91ca796..0f06850dc9 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -34,6 +34,10 @@ module ccv_model { InitialValidatorSet: Node -> int, } + // The params variable is never actually changed, and + // just exists so the parameters are entered into the .itf file when we generate traces. + // This should be removed when/if Quint adds support to put the + // constant initializations in its output. var params: Parameters var currentState: ProtocolState @@ -64,7 +68,7 @@ module ccv_model { // Note that these can still be combined, so in effect we can get all time advancements by any amount of seconds. // These should be smaller than the minimal TrustingPeriodPerChain, // otherwise connections will break down. - pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week - 1 * Hour) // 4 * Week) + pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week - 1 * Hour, 4 * Week) pure def emptyAction = { @@ -175,8 +179,8 @@ module ccv_model { params' = params, } - // step_common is the core functionality of steps that does not have anything to do with time. - action step_common = any { + // stepCommon is the core functionality of steps that does not have anything to do with time. + action stepCommon = any { nondet node = oneOf(nodes) // very restricted set of voting powers. exact values are not important, // and this keeps the state space smaller. @@ -218,38 +222,38 @@ module ccv_model { nondet timeAdvancement = oneOf(timeAdvancements) EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), - step_common + stepCommon } // ================== // UTILITY FUNCTIONS // ================== - pure def earliest(packets: Set[VscPacket]): VscPacket = - val latestPossiblePacket: VscPacket = { + pure def oldest(packets: Set[VscPacket]): VscPacket = + val newestPossiblePacket: VscPacket = { id: 0, validatorSet: Map(), sendingTime: 9999999999999 * Second, timeoutTime: 9999999999999 * Second, } packets.fold( - latestPossiblePacket, + newestPossiblePacket, (res, pack) => if(res.sendingTime < pack.sendingTime) { res } else { pack } ) - pure def latest(packets: Set[VscPacket]): VscPacket = - val earliestPossiblePacket: VscPacket = { + pure def newest(packets: Set[VscPacket]): VscPacket = + val oldestPossiblePacket: VscPacket = { id: 0, validatorSet: Map(), sendingTime: -9999999999 * Second, timeoutTime: -9999999999 * Second, } packets.fold( - earliestPossiblePacket, + oldestPossiblePacket, (res, pack) => if(res.sendingTime >= pack.sendingTime) { res } else { pack } ) - run earliestLatestTest = { + run oldestnewestTest = { val packet1 = { id: 1, validatorSet: Map(), @@ -271,10 +275,10 @@ module ccv_model { timeoutTime: 3 * Second, } all { - assert(earliest(Set(packet1, packet2, packet3)) == packet1), - assert(earliest(Set(packet3, packet2, packet1)) == packet1), - assert(latest(Set(packet1, packet2, packet3)) == packet3), - assert(latest(Set(packet3, packet2, packet1)) == packet3), + assert(oldest(Set(packet1, packet2, packet3)) == packet1), + assert(oldest(Set(packet3, packet2, packet1)) == packet1), + assert(newest(Set(packet1, packet2, packet3)) == packet3), + assert(newest(Set(packet3, packet2, packet1)) == packet3), } } @@ -328,8 +332,8 @@ module ccv_model { if (commonPackets.size() == 0) { true // they don't share any packets, so nothing to check } else { - val newestCommonPacket = commonPackets.latest() - val oldestCommonPacket = commonPackets.earliest() + val newestCommonPacket = commonPackets.newest() + val oldestCommonPacket = commonPackets.oldest() // get all packets sent between the oldest and newest common packet val packetsBetween1 = packets1.select( packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime @@ -508,6 +512,8 @@ module ccv_model { assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 200)), // advance time on provider and consumer until unbonding period is over - ensure that the consumer and provider // stay in sync relative to each other + // We want to make sure the steps we make are shorter the trusting period, + // since that would time out clients in reality. 4.reps( i => EndAndBeginBlockForProvider(UnbondingPeriodPerChain.get("consumer1")/4, Set(), Set()).then( @@ -614,7 +620,7 @@ module ccv_model { EndAndBeginBlockForProvider(VscTimeout + 1 * Second, Set(), Set()) ) .then( - // eenter the advanced time on chain + // enter the advanced time on chain EndAndBeginBlockForProvider(1 * Second, Set(), Set()) ) .then( diff --git a/tests/mbt/model/ccv_sync.qnt b/tests/mbt/model/ccv_sync.qnt index 99bbcdc720..d828b88a76 100644 --- a/tests/mbt/model/ccv_sync.qnt +++ b/tests/mbt/model/ccv_sync.qnt @@ -13,21 +13,21 @@ module ccv_sync { // "action scheduling", essentially using a variable to // determine the next action to be taken. - // QueuedEndBlocks contains a list of chains which will end their blocks next, + // QueuedChainsToEndBlock contains a list of chains which will end their blocks next, // together with the time advancement they should advance by. - // When stepHappy selects an action, it checks if there are any chains in this list, + // When stepSync selects an action, it checks if there are any chains in this list, // and if so, it will only select actions that end blocks on the head of the list. - // QueuedEndBlocks is thus used to schedule actions. - var QueuedEndBlocks: List[(ccvt::Chain, Time)] + // QueuedChainsToEndBlock is thus used to schedule actions. + var QueuedChainsToEndBlock: List[(ccvt::Chain, Time)] // runs init, then ends and begins a block for each chain, while also starting all consumers. // necessary because we want the happy path to have all consumer chains started. - action initHappy = + action initSync = all { init.then( EndAndBeginBlockForProvider(1 * Second, consumerChains, Set()) ), - QueuedEndBlocks' = consumerChainList.foldl( + QueuedChainsToEndBlock' = consumerChainList.foldl( List(), (acc, consumer) => acc.append((consumer, 1 * Second)) ), @@ -38,30 +38,30 @@ module ccv_sync { // step will advance time for all chains at the same rate, // thus the clock times are always in sync. // This is useful to test happy paths. - action stepHappy = any { + action stepSync = any { // choose any of the three "all" blocks nondet timeAdvancement = oneOf(timeAdvancements) all { - QueuedEndBlocks.length() == 0, - EndAndBeginBlockForProvider(timeAdvancement, Set(), Set()), - QueuedEndBlocks' = consumerChainList.foldl( + QueuedChainsToEndBlock.length() == 0, // no queued action needs to be taken + EndAndBeginBlockForProvider(timeAdvancement, Set(), Set()), // end a block for the provider + QueuedChainsToEndBlock' = consumerChainList.foldl( // queue all consumers to end a block List(), (acc, consumer) => acc.append((consumer, timeAdvancement)) ), }, all { - QueuedEndBlocks.length() > 0, - val pair = QueuedEndBlocks.head() + QueuedChainsToEndBlock.length() > 0, // there is a consumer that needs to end a block next + val pair = QueuedChainsToEndBlock.head() val chain = pair._1 val timeAdv = pair._2 - EndAndBeginBlockForConsumer(chain, timeAdv), - QueuedEndBlocks' = QueuedEndBlocks.tail(), + EndAndBeginBlockForConsumer(chain, timeAdv), // end a block for that consumer + QueuedChainsToEndBlock' = QueuedChainsToEndBlock.tail(), // remove that consumer from the queue }, - all { - QueuedEndBlocks.length() == 0, - step_common, - QueuedEndBlocks' = QueuedEndBlocks, + all { + QueuedChainsToEndBlock.length() == 0, // no action is queued + stepCommon, // do one of the actions that are NOT ending a block, like delivering packets, voting power changes, ... + QueuedChainsToEndBlock' = QueuedChainsToEndBlock, } } } \ No newline at end of file