Rename sentVscPackets to sentVscPacketsToConsumer

cosmos · Oct 12, 2023 · 4d87372 · 4d87372
1 parent f294eec
commit 4d87372
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 16 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -69,7 +69,7 @@ module ccv_types {
             receivedMaturations: Set[VscMaturedPacket],
 
             // Stores VscPackets which have been sent but where the provider has *not received a response yet*.
-            sentVscPackets: Chain -> List[VscPacket],
+            sentVscPacketsToConsumer: Chain -> List[VscPacket],
 
             // stores whether, in this block, the validator set has changed.
             // this is needed because the validator set might be considered to have changed, even though
@@ -92,7 +92,7 @@ module ccv_types {
             chainState: GetEmptyChainState,
             outstandingPacketsToConsumer: Map(),
             receivedMaturations: Set(),
-            sentVscPackets: Map(),
+            sentVscPacketsToConsumer: Map(),
             providerValidatorSetChangedInThisBlock: false,
             consumerStatus: Map(),
             runningVscId: 0,
@@ -178,7 +178,7 @@ module ccv_types {
                     },
                     outstandingPacketsToConsumer: Map(),
                     receivedMaturations: Set(),
-                    sentVscPackets: Map(),
+                    sentVscPacketsToConsumer: Map(),
                     providerValidatorSetChangedInThisBlock: false,
                     consumerStatus: Map(),
                     runningVscId: 0,
@@ -634,10 +634,10 @@ module ccv {
             )
             ).with(
                 // update the sent VscPackets
-                "sentVscPackets",
+                "sentVscPacketsToConsumer",
                 ConsumerChains.mapBy(
                     (consumer) => 
-                    providerState.sentVscPackets.get(consumer).concat(
+                    providerState.sentVscPacketsToConsumer.get(consumer).concat(
                         newSentPacketsPerConsumer.get(consumer)
                     )
                 )
@@ -688,7 +688,7 @@ module ccv {
     pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = {
         if (not(isRunningConsumer(sender, currentState.providerState))) {
             Err("Sender is not currently a consumer - must have 'running' status!")
-        } else if (currentState.providerState.sentVscPackets.get(sender).head().id != packet.id) {
+        } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) {
             // the packet is not the oldest sentVscPacket, something went wrong
             Err("Received maturation is not for the oldest sentVscPacket")
         } else {
@@ -698,7 +698,7 @@ module ccv {
                 "receivedMaturations", newReceivedMaturations
             )
             // prune the sentVscPacket
-            val newSentVscPacket = currentState.providerState.sentVscPackets.get(sender).tail()
+            val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail()
             val newState = currentState.with(
                 "providerState", newProviderState
             )
@@ -784,9 +784,9 @@ module ccv {
             val consumerState = currentState.consumerStates.get(consumer)
 
             // has a packet been sent on the provider more than VscTimeout ago, but we have not received an answer since then?
-            val sentVscPackets = providerState.sentVscPackets.get(consumer)
-            if(sentVscPackets.length() > 0) {
-                val oldestSentVscPacket = sentVscPackets.head() // if length is 0, this is undefined, but we check for this before we use it
+            val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer)
+            if(sentVscPacketsToConsumer.length() > 0) {
+                val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it
                 if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.lastTimestamp) {
                     (true, "")
                 } else {

diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -121,7 +121,7 @@ module ccv_statemachine {
             "outstandingPacketsToConsumer", 
             ConsumerChains.mapBy(chain => List())
         ).with(
-            "sentVscPackets", 
+            "sentVscPacketsToConsumer", 
             ConsumerChains.mapBy(chain => List())
         ).with(
             // set the validator set to be the initial validator set in the history
@@ -213,7 +213,7 @@ module ccv_statemachine {
             // ... for each consumer that is running then ...
             runningConsumers.forall(
                 // ...the validator set is in a sent packet
-                consumer => currentState.providerState.sentVscPackets.get(consumer).toSet().exists(
+                consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
                     packet => packet.validatorSet == providerValSetInCurBlock
                 )
             )
@@ -272,14 +272,14 @@ module ccv_statemachine {
 
     // If we send a VscPacket, this is eventually responded to by all consumers
     // that were running at the time the packet was sent (and are still running).
-    // Since we remove sentVscPackets when we receive responses for them,
+    // Since we remove sentVscPacketsToConsumer when we receive responses for them,
     // we just check that if a sentVscPacket has been sent more than
     // VscTimeout ago, the consumer must have been dropped.
     // In practice, when this is true, a pending unbonding can mature.
     val EventuallyMatureOnProviderInv =
         runningConsumers.forall(
             consumer => {
-                val sentPackets = currentState.providerState.sentVscPackets.get(consumer).toSet()
+                val sentPackets = currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet()
                 sentPackets.forall(
                     packet =>
                         // consumer still has time to respond
@@ -363,7 +363,7 @@ module ccv_statemachine {
                     "consumer2" -> List(),
                     "consumer3" -> List()
                 )),
-                assert(currentState.providerState.sentVscPackets == Map(
+                assert(currentState.providerState.sentVscPacketsToConsumer == Map(
                     "consumer1" -> List(),
                     "consumer2" -> List(),
                     "consumer3" -> List()

diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt
@@ -121,7 +121,7 @@ module ccv_test {
     ).with(
         // put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer
         "providerState", _DeliverPacketToProvider_TestState.providerState.with(
-            "sentVscPackets", _DeliverPacketToProvider_TestState.providerState.sentVscPackets.put(
+            "sentVscPacketsToConsumer", _DeliverPacketToProvider_TestState.providerState.sentVscPacketsToConsumer.put(
                 "sender", List({
                     id: 0,
                     validatorSet: _DeliverPacketToProvider_TestState.providerState.chainState.currentValidatorSet,