diff --git a/tests/difference/core/quint_model/ccv_happy.qnt b/tests/difference/core/quint_model/ccv_happy.qnt new file mode 100644 index 0000000000..60e2574422 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_happy.qnt @@ -0,0 +1,67 @@ +module ccv_happy { + import ccv_model.* from "ccv_model" + import ccv_types as ccvt from "ccv" + import ccv from "ccv" + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + + + // The happy path module has its own init and step functions. + // They ensure that chains do not drift from each other in terms of time, + // and all chains produce blocks synchronously. + // To do so, it makes use of + // "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, + // together with the time advancement they should advance by. + // When stepHappyPath 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)] + + // 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 = + all { + init.then( + EndAndBeginBlockForProvider(1 * Second, consumerChains, Set()) + ), + QueuedEndBlocks' = consumerChainList.foldl( + List(), + (acc, consumer) => acc.append((consumer, 1 * Second)) + ), + } + + + + // 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 { + nondet timeAdvancement = oneOf(timeAdvancements) + all { + QueuedEndBlocks.length() == 0, + EndAndBeginBlockForProvider(timeAdvancement, Set(), Set()), + QueuedEndBlocks' = consumerChainList.foldl( + List(), + (acc, consumer) => acc.append((consumer, timeAdvancement)) + ), + }, + + all { + QueuedEndBlocks.length() > 0, + val pair = QueuedEndBlocks.head() + val chain = pair._1 + val timeAdv = pair._2 + EndAndBeginBlockForConsumer(chain, timeAdv), + QueuedEndBlocks' = QueuedEndBlocks.tail(), + }, + + all { + QueuedEndBlocks.length() == 0, + step_common, + QueuedEndBlocks' = QueuedEndBlocks, + } + } +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt index c253824e43..80e414e3fa 100644 --- a/tests/difference/core/quint_model/ccv_model.qnt +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -5,10 +5,12 @@ module ccv_model { import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" - pure val consumerChains = Set("consumer1", "consumer2", "consumer3") + pure val consumerChainList = List("consumer1", "consumer2", "consumer3") + pure val consumerChains = consumerChainList.toSet() pure val chains = consumerChains.union(Set(PROVIDER_CHAIN)) - pure val unbondingPeriods = chains.mapBy(chain => 2 * Week) - pure val trustingPeriods = chains.mapBy(chain => 1 * Week) + pure val defUnbondingPeriod = 2 * Week + 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 nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10") @@ -16,6 +18,8 @@ module ccv_model { import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain = trustingPeriods).* from "./ccv" + // TODO: introduce max clock drift to produce traces with bounded drift + type Parameters = { VscTimeout: Time, CcvTimeout: Chain -> Time, @@ -69,46 +73,6 @@ module ccv_model { changeAmount: 0, } - // step allows the most generic nondeterminism, in particular it becomes relatively likely - // that over a long enough runtime, all consumers would time out by mismatching their time advancements, - // and each endblock has a good chance to stop consumers, ... - // step is thus suited to test also unhappy paths. - action step = any { - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet chain = oneOf(runningConsumers) - nondet timeAdvancement = oneOf(timeAdvancements) - EndAndBeginBlockForConsumer(chain, timeAdvancement), - }, - - val consumerStatus = currentState.providerState.consumerStatus - nondet consumersToStart = oneOf(nonConsumers.powerset()) - nondet consumersToStop = oneOf(runningConsumers.powerset()) - nondet timeAdvancement = oneOf(timeAdvancements) - EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), - - nondet node = oneOf(nodes) - // very restricted set of voting powers. exact values are not important, - // and this keeps the state space smaller. - nondet newVotingPower = oneOf(Set(-50, 50)) - VotingPowerChange(node, newVotingPower), - - // try to send a packet. we could filter by chains that can actually send, - // but it's probably not much faster than just trying and failing. - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet sender = oneOf(runningConsumers) - DeliverVscMaturedPacket(sender), - }, - - // again, we could filter by chains that can actually receive, - // but it's probably not much faster than just trying and failing. - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet recciver = oneOf(runningConsumers) - DeliverVscPacket(recciver), - }, - } // some utility stateful vals to make invariants easier to define val providerValidatorHistory = currentState.providerState.chainState.votingPowerHistory @@ -207,6 +171,53 @@ module ccv_model { params' = params, } + // step_common is the core functionality of steps that does not have anything to do with time. + // Thus, it is part of both step and stepBoundedDrift. + action step_common = any { + nondet node = oneOf(nodes) + // very restricted set of voting powers. exact values are not important, + // and this keeps the state space smaller. + nondet newVotingPower = oneOf(Set(-50, 50)) + VotingPowerChange(node, newVotingPower), + + // try to send a packet. we could filter by chains that can actually send, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet sender = oneOf(runningConsumers) + DeliverVscMaturedPacket(sender), + }, + + // again, we could filter by chains that can actually receive, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet recciver = oneOf(runningConsumers) + DeliverVscPacket(recciver), + }, + } + + // step allows the most generic nondeterminism, in particular it becomes relatively likely + // that over a long enough runtime, all consumers would time out by mismatching their time advancements, + // and each endblock has a good chance to stop consumers, ... + // step is thus suited to test also unhappy paths. + action step = any { + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet chain = oneOf(runningConsumers) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForConsumer(chain, timeAdvancement), + }, + + val consumerStatus = currentState.providerState.consumerStatus + nondet consumersToStart = oneOf(nonConsumers.powerset()) + nondet consumersToStop = oneOf(runningConsumers.powerset()) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + + step_common + } + // ================== // UTILITY FUNCTIONS // ================== @@ -400,6 +411,9 @@ module ccv_model { currentState.providerState.outstandingPacketsToConsumer.get(consumer).length() > 0 )) + val CanReceiveVscPackets = + not(trace[length(trace)-1].kind == "DeliverVscPacket") + val CanSendVscMaturedPackets = not(ConsumerChains.exists( consumer =>