Incorporate Karolos' comments

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
+go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1

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
+go run ./... -modelPath=../model/ccv_sync.qnt -init initHappy -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1

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.

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)

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(

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