Fix minor issues

cosmos · Oct 5, 2023 · 2a68236 · 2a68236
1 parent 8da4cfe
commit 2a68236
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 26 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -324,30 +324,6 @@ module CCV {
         }
     }   
 
-    // Defines a test state to test the deliverPacketToProvider function against.
-    pure val _DeliverPacketToProvider_TestState =
-        val currentState = GetEmptyProtocolState
-        val sender = "sender"
-        val providerState = currentState.providerState
-        val consumerState = GetEmptyConsumerState
-        // add the consumer to the consumerStates
-        val consumerStates = currentState.consumerStates.put(sender, consumerState)
-        val providerState2 = providerState.with(
-            "consumerStatus", providerState.consumerStatus.put(sender, RUNNING)
-        )
-        val providerState3 = providerState2.with(
-            "outstandingPacketsToConsumer", providerState2.outstandingPacketsToConsumer.put(sender, List({
-                id: 0,
-                validatorSet: Map(),
-                sendingTime: 0
-            }))
-        )
-        currentState.with(
-            "providerState", providerState3
-        ).with(
-            "consumerStates", consumerStates
-        )
-
     // Delivers the next queued VSCPacket from the provider chain to a consumer chain.
     // Only argument is the consumer chain, to which the packet will be delivered.
     // If this packet will time out on the consumer on delivery,

diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -169,9 +169,10 @@ module CCVDefaultStateMachine {
 
     // Any update in the power of a validator on the provider
     // MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains
-    val ValidatorUpdatesArePropagated =
+    val ValUpdatePrecondition = trace[trace.length()-1] == "EndAndBeginBlockForProvider"
+    val ValidatorUpdatesArePropagated = 
         // when the provider has just entered a validator set into a block...
-        if (trace == trace.append("EndAndBeginBlockForProvider")) {
+        if (ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock) {
             val providerValSetInCurBlock = providerValidatorHistory.head()
             // ... for each consumer that is running then ...
             runningConsumers.forall(

diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt
@@ -84,6 +84,30 @@ module CCVTest {
         result.newState.providerState.chainState.votingPowerHistory == List()
     }
 
+    // Defines a test state to test the deliverPacketToProvider function against.
+    pure val _DeliverPacketToProvider_TestState =
+        val currentState = GetEmptyProtocolState
+        val sender = "sender"
+        val providerState = currentState.providerState
+        val consumerState = GetEmptyConsumerState
+        // add the consumer to the consumerStates
+        val consumerStates = currentState.consumerStates.put(sender, consumerState)
+        val providerState2 = providerState.with(
+            "consumerStatus", providerState.consumerStatus.put(sender, RUNNING)
+        )
+        val providerState3 = providerState2.with(
+            "outstandingPacketsToConsumer", providerState2.outstandingPacketsToConsumer.put(sender, List({
+                id: 0,
+                validatorSet: Map(),
+                sendingTime: 0
+            }))
+        )
+        currentState.with(
+            "providerState", providerState3
+        ).with(
+            "consumerStates", consumerStates
+        )
+
     // add a packet on the consumer
     pure val DeliverPacketToProviderHappyPathTest_testState = _DeliverPacketToProvider_TestState.with(
         "consumerStates", _DeliverPacketToProvider_TestState.consumerStates.put(