Update model for bug reporting]

cosmos · Oct 2, 2023 · 289ccad · 289ccad
1 parent e494a09
commit 289ccad
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 10 deletions.
diff --git 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
-
+
+Run all sanity checks by running `run_sanity_checks.sh`.
diff --git 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
@@ -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
@@ -0,0 +1 @@
+quint run --invariant "all{CanRunConsumer,CanStopConsumer,CanTimeoutConsumer,CanSendVSCPackets,CanSendVSCMaturedPackets}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 2000 --max-samples 200