From 289ccad3c7d8fc3cd1fbaa9b5116c7737af42414 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 2 Oct 2023 10:46:51 +0200
Subject: [PATCH] Update model for bug reporting]

---
 tests/difference/core/quint_model/README.md   |  3 ++-
 tests/difference/core/quint_model/ccv.qnt     | 27 +++++++++++++++++--
 .../core/quint_model/ccv_statemachine.qnt     | 23 +++++++++++-----
 .../core/quint_model/run_sanity_checks.sh     |  1 +
 4 files changed, 44 insertions(+), 10 deletions(-)
 create mode 100755 tests/difference/core/quint_model/run_sanity_checks.sh

diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md
index a6451b1396..696cb183a9 100644
--- a/tests/difference/core/quint_model/README.md
+++ b/tests/difference/core/quint_model/README.md
@@ -57,4 +57,5 @@ The available sanity checks are:
 - CanTimeoutConsumer
 - CanSendVSCPackets
 - CanSendVSCMaturedPackets
-        
\ No newline at end of file
+        
+Run all sanity checks by running `run_sanity_checks.sh`.
\ No newline at end of file
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index f329955955..7d9edf884e 100644
--- a/tests/difference/core/quint_model/ccv.qnt
+++ b/tests/difference/core/quint_model/ccv.qnt
@@ -445,6 +445,29 @@ module CCV {
         val providerStateAfterConsumerAdvancement = providerStateAfterTimeAdvancement.with(
             "consumerStatus", newConsumerStatus
         )
+
+        // for each consumer we just set to running, set its initial validator set to be the current one on the provider.
+        val newConsumerStateMap =
+            currentState.consumerStates.keys().mapBy(
+                (consumer) => 
+                if (consumersToStart.contains(consumer)) {
+                    val currentConsumerState = currentState.consumerStates.get(consumer)
+                    val newConsumerState = currentConsumerState.with(
+                        "chainState", currentConsumerState.chainState.with(
+                            "currentValidatorSet", providerStateAfterConsumerAdvancement.chainState.currentValidatorSet
+                        )
+                    )
+                    (consumer, newConsumerState)
+                } else {
+                    (consumer, currentState.consumerStates.get(consumer))
+                }
+            )
+        val newState = currentState.with(
+            "providerState", providerStateAfterConsumerAdvancement
+        ).with(
+            "consumerStates", newConsumerStateMap
+        )
+
         if (err != "") {
             Err(err)
         } else {
@@ -456,10 +479,10 @@ module CCV {
                 } else {
                     providerStateAfterConsumerAdvancement
                 }
-            val newState = currentState.with(
+            val finalState = newState.with(
                 "providerState", providerStateAfterSending
             )
-            Ok(newState)
+            Ok(finalState)
         }
     }
 
diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
index a0e81a5186..5c5a4bd00a 100644
--- a/tests/difference/core/quint_model/ccv_statemachine.qnt
+++ b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -115,9 +115,12 @@ module CCVDefaultStateMachine {
     // and each endblock has a good chance to stop consumers, ...
     // step is thus suited to test also unhappy paths.
     action step = any {
-        nondet chain = oneOf(runningConsumers)
-        nondet timeAdvancement = oneOf(timeAdvancements)
-        EndAndBeginBlockForConsumer(chain, timeAdvancement),
+        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),
+        },
 
         val consumerStatus = currentState.providerState.consumerStatus
         nondet consumersToStart = oneOf(unusedConsumers.powerset())
@@ -134,13 +137,19 @@ module CCVDefaultStateMachine {
 
         // try to send a packet. we could filter by chains that can actually send,
         // but it's probably not much faster than just trying and failing.
-        nondet sender = oneOf(runningConsumers)
-        DeliverVSCMaturedPacket(sender),
+        all {
+            runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense
+            nondet sender = oneOf(runningConsumers)
+            DeliverVSCMaturedPacket(sender),
+        },
 
         // again, we could filter by chains that can actually receive,
         // but it's probably not much faster than just trying and failing.
-        nondet recciver = oneOf(runningConsumers)
-        DeliverVSCPacket(recciver),
+        all {
+            runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense
+            nondet recciver = oneOf(runningConsumers)
+            DeliverVSCPacket(recciver),
+        },
     }
 
     // ==================
diff --git a/tests/difference/core/quint_model/run_sanity_checks.sh b/tests/difference/core/quint_model/run_sanity_checks.sh
new file mode 100755
index 0000000000..546d5468f1
--- /dev/null
+++ b/tests/difference/core/quint_model/run_sanity_checks.sh
@@ -0,0 +1 @@
+quint run --invariant "all{CanRunConsumer,CanStopConsumer,CanTimeoutConsumer,CanSendVSCPackets,CanSendVSCMaturedPackets}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 2000 --max-samples 200
\ No newline at end of file