From 86324b71a9449d24e48601d47db34b3501e13a3c Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 16 Oct 2023 11:17:47 +0200
Subject: [PATCH] Change Error type to string

---
 tests/difference/core/quint_model/ccv.qnt     | 45 ++++++++-----------
 .../difference/core/quint_model/ccv_model.qnt | 20 ++++-----
 2 files changed, 27 insertions(+), 38 deletions(-)

diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 8cab951c99..0e07b4476c 100644
--- a/tests/difference/core/quint_model/ccv.qnt
+++ b/tests/difference/core/quint_model/ccv.qnt
@@ -143,9 +143,7 @@ module ccv_types {
             consumerStates: Map(),
         }
 
-    type Error = {
-        message: str
-    }
+    type Error = str
 
     // we return either a result or an error.
     // if hasError() is true, newState may be arbitrary, but the error will be meaningful.
@@ -158,9 +156,7 @@ module ccv_types {
     pure def Ok(newState: ProtocolState): Result = {
         {
             newState: newState,
-            error: {
-                message: ""
-            }
+            error: ""
         }
     }
 
@@ -182,13 +178,11 @@ module ccv_types {
                 },
                 consumerStates: Map(),
             },
-            error: {
-                message: msg
-            }
+            error: msg
         }
     }
 
-    pure def hasError(result: Result): bool = result.error.message != ""
+    pure def hasError(result: Result): bool = result.error != ""
 
     // possible consumer statuses
     pure val STOPPED = "stopped" // the chain was once a consumer chain, but has been voluntarily dropped by the provider.
@@ -306,7 +300,7 @@ module ccv {
                 val result = recvPacketOnProvider(currentState, sender, packet)
                 val tmpState = result.newState
                 if (result.hasError()) {
-                    (Err(result.error.message), false)
+                    (result, false)
                 } else {
                     (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out
                 }
@@ -355,7 +349,7 @@ module ccv {
                 val result = recvPacketOnConsumer(currentState, receiver, packet)
                 val tmpState = result.newState
                 if (result.hasError()) {
-                    (Err(result.error.message), false)
+                    (result, false)
                 } else {
                     (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out
                 }
@@ -652,21 +646,18 @@ module ccv {
             // update the running validator set, but not the history yet,
             // as that only happens when the next block is started
             val currentConsumerState = currentState.consumerStates.get(receiver)
-            val newConsumerState = currentConsumerState.with(
-                "chainState",
-                currentConsumerState.chainState.with(
-                    "currentValidatorSet", packet.validatorSet
-                )
-            ).with(
-                "maturationTimes",
-                currentConsumerState.maturationTimes.put(
-                    packet, 
-                    currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
-                )
-            ).with(
-                "receivedVscPackets",
-                currentConsumerState.receivedVscPackets.prepend(packet)
-            )
+            val newConsumerState = 
+                {
+                    ...currentConsumerState,
+                    chainState: currentConsumerState.chainState.with(
+                        "currentValidatorSet", packet.validatorSet
+                    ),
+                    maturationTimes: currentConsumerState.maturationTimes.put(
+                        packet, 
+                        currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
+                    ),
+                    receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet)
+                }
             val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState)
             val newState = currentState.with(
                 "consumerStates", newConsumerStates
diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
index 300c543d40..f886fe9e85 100644
--- a/tests/difference/core/quint_model/ccv_model.qnt
+++ b/tests/difference/core/quint_model/ccv_model.qnt
@@ -198,18 +198,16 @@ module ccv_model {
     val ValUpdatePrecondition = trace[trace.length()-1].kind == "EndAndBeginBlockForProvider"
     val ValidatorUpdatesArePropagatedInv = 
         // when the provider has just entered a validator set into a block...
-        if (ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock) {
-            val providerValSetInCurBlock = providerValidatorHistory.head()
-            // ... for each consumer that is running then ...
-            runningConsumers.forall(
-                // ...the validator set is in a sent packet
-                consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
-                    packet => packet.validatorSet == providerValSetInCurBlock
-                )
+        ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock
+            implies
+        val providerValSetInCurBlock = providerValidatorHistory.head()
+        // ... for each consumer that is running then ...
+        runningConsumers.forall(
+            // ...the validator set is in a sent packet
+            consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
+                packet => packet.validatorSet == providerValSetInCurBlock
             )
-        } else {
-            true
-        }
+        )
 
     // Every consumer chain receives the same sequence of 
     // ValidatorSetChangePackets in the same order.