Resolve comments

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

Hide file tree

Showing 2 changed files with 2 additions and 14 deletions.
diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -18,15 +18,6 @@ module ccv_statemachine {
 
     var currentState: ProtocolState
 
-
-    pure def ACTIONS = Set(
-        "VotingPowerChange",
-        "DeliverVscPacket",
-        "DeliverVscMaturedPacket",
-        "EndAndBeginBlockForProvider",
-        "EndAndBeginBlockForConsumer"
-    )
-
     // a type storing the parameters used in actions.
     // this is used in the trace to store
     // the name of the last action, plus the parameters we passed to it.
@@ -85,7 +76,6 @@ module ccv_statemachine {
         nondet node = oneOf(nodes)
         // very restricted set of voting powers. exact values are not important,
         // and this keeps the state space smaller.
-        // 0 for getting a validator out of the validator set, and two non-zero values
         nondet newVotingPower = oneOf(Set(0, 50, 100))
         VotingPowerChange(node, newVotingPower),
 

diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt
@@ -145,7 +145,6 @@ module ccv_test {
     run StateModificationOK_DeliverPacketToProviderHappyPathTest =
     {
         val result = DeliverPacketToProviderHappyPathTest_resultAndTimeout._1
-        val timedOut = DeliverPacketToProviderHappyPathTest_resultAndTimeout._2
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
         not(result.hasError) and
@@ -168,17 +167,16 @@ module ccv_test {
     run DidTimeOut_DeliverPacketToProviderTimeoutTest =
     {
         val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1
-        val timedOut = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2
+        val timeout = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
         not(result.hasError) and
-        timedOut
+        timeout
     }
 
     run StateModificationOK_DeliverPacketToProviderTimeoutTest =
     {
         val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1
-        val timedOut = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
         not(result.hasError) and