Start writing model with boundeddrift

Author: p-offtermatt

tests/difference/core/quint_model/ccv.qnt

@@ -399,9 +399,10 @@ module ccv {
             res._1
         )
 
+        // check whether the local client for the provider has expired on any consumer
         val expiredConsumers = getRunningConsumers(providerStateAfterTimeAdvancement).filter(
             consumer => 
-            providerStateAfterTimeAdvancement.chainState.runningTimestamp > tmpState.consumerStates.get(consumer).chainState.lastTimestamp + TrustingPeriodPerChain.get("provider")
+            providerStateAfterTimeAdvancement.chainState.lastTimestamp > tmpState.consumerStates.get(consumer).chainState.runningTimestamp + TrustingPeriodPerChain.get(consumer)
         ).exclude(timedOutConsumers)
 
         // send vsc packets
@@ -507,9 +508,9 @@ module ccv {
                         }
                     )
                 )
-                // checks whether the local client for the provider chain has expired on the consumer
+                // checks whether the local client for the consumer has expired on the provider
                 val clientExpired = 
-                    if (newChainState.runningTimestamp > currentState.providerState.chainState.lastTimestamp + TrustingPeriodPerChain.get(chain)) {
+                    if (newChainState.lastTimestamp > currentState.providerState.chainState.runningTimestamp + TrustingPeriodPerChain.get(chain)) {
                         true
                     } else {
                         false

tests/difference/core/quint_model/ccv_boundeddrift.qnt

@@ -0,0 +1,53 @@
+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 boundeddrift module has its own step function.
+    // They ensure that chains do not drift from each other in terms of time
+    // more than a given bound.
+    // It differs from the sync module in that it does not require
+    // the chains to produce blocks at the same time.
+
+    // The maximal drift that this module will allow between chains.
+    // 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.
+    pure val maxDrift = defUnbondingPeriod - 2 * Hour
+
+    // Finds the maximal time advancement that can be done for a given chain
+    // without violating the maxDrift constraint.
+    pure def findMaxTimeAdvancement(advancingChain: ccvt::ChainState, otherChains: Set[ccvt::ChainState]): Time =
+        val otherChainsLastTimes = otherChains.map(c => c.lastTimestamp)
+        0
+        // // start with advancingChain.RunningTime - if this is the minimal element, we can advance by maxDrift anyways
+        // val otherChainsMinLastTime = otherChainsLastTimes.fold(advancingChain.runningTimestamp, (acc, t) => if (acc < t) acc else t)
+        // val maxTime = advancingChain.runningTimestamp - otherChainsMinLastTime + maxDrift
+
+    // 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 stepBoundedDrift = any {
+        step_common, // allow actions that do not influence time
+
+        all {
+            // advance a block for a consumer
+            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),
+            },
+
+            // advance a block for the provider
+            val consumerStatus = currentState.providerState.consumerStatus
+            nondet consumersToStart = oneOf(nonConsumers.powerset())
+            nondet consumersToStop = oneOf(runningConsumers.powerset())
+            nondet timeAdvancement = oneOf(timeAdvancements)
+            EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop),
+        }
+    }
+}

tests/difference/core/quint_model/ccv_model.qnt

@@ -170,7 +170,6 @@ module ccv_model {
         }
 
      // 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,

tests/difference/core/quint_model/ccv_happy.qnt renamed to tests/difference/core/quint_model/ccv_sync.qnt

@@ -1,12 +1,12 @@
-module ccv_happy {
+module ccv_sync {
     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.
+    // The sync 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
@@ -15,7 +15,7 @@ module ccv_happy {
 
     // 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,
+    // When stepHappy 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)]