From 2a682368c7c1df44e017ab6b37b5bf29b9831f84 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Thu, 5 Oct 2023 17:50:44 +0200
Subject: [PATCH] Fix minor issues

---
 tests/difference/core/quint_model/ccv.qnt     | 24 -------------------
 .../core/quint_model/ccv_statemachine.qnt     |  5 ++--
 .../difference/core/quint_model/ccv_test.qnt  | 24 +++++++++++++++++++
 3 files changed, 27 insertions(+), 26 deletions(-)

diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 141b5bf06d..43dca0ccc2 100644
--- 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
index e12fdf7d85..b4229c05e0 100644
--- 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
index a6b09a1a60..7f3e6a69fd 100644
--- 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(