Add ccv_happy module as a happyPath variant

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,
+        }
+    }
+}

tests/difference/core/quint_model/ccv_model.qnt

@@ -5,17 +5,21 @@ 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")
     pure val InitialValidatorSet = nodes.mapBy(node => 100)
 
     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 =>