Remove hasError field and make it a function

tests/difference/core/quint_model/ccv.qnt

@@ -148,17 +148,15 @@ module ccv_types {
     }
 
     // we return either a result or an error.
-    // if hasError is true, newState may be arbitrary, but the error will be meaningful.
-    // if hasError is false, error may be arbitrary, but newState will be meaningful.
+    // if hasError() is true, newState may be arbitrary, but the error will be meaningful.
+    // if hasError() is false, error may be arbitrary, but newState will be meaningful.
     type Result = {
-        hasError: bool,
         newState: ProtocolState,
         error: Error
     }
 
     pure def Ok(newState: ProtocolState): Result = {
         {
-            hasError: false,
             newState: newState,
             error: {
                 message: ""
@@ -168,7 +166,6 @@ module ccv_types {
 
     pure def Err(msg: str): Result = {
         {
-            hasError: true,
             newState: {
                 providerState: {
                     chainState: {
@@ -191,6 +188,8 @@ module ccv_types {
         }
     }
 
+    pure def hasError(result: Result): bool = result.error.message != ""
+
     // possible consumer statuses
     pure val STOPPED = "stopped" // the chain was once a consumer chain, but has been voluntarily dropped by the provider.
     pure val TIMEDOUT = "timedout" // the chain has timed out and was dropped by the provider. This is only used for involuntary drops.
@@ -308,7 +307,7 @@ module ccv {
                 // the packet has not timed out, so receive it on the provider
                 val result = recvPacketOnProvider(currentState, sender, packet)
                 val tmpState = result.newState
-                if (result.hasError) {
+                if (result.hasError()) {
                     (Err(result.error.message), false)
                 } else {
                     (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out
@@ -357,7 +356,7 @@ module ccv {
                 // the packet has not timed out, so receive it on the consumer
                 val result = recvPacketOnConsumer(currentState, receiver, packet)
                 val tmpState = result.newState
-                if (result.hasError) {
+                if (result.hasError()) {
                     (Err(result.error.message), false)
                 } else {
                     (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out

tests/difference/core/quint_model/ccv_statemachine.qnt

@@ -131,7 +131,7 @@ module ccv_statemachine {
     action VotingPowerChange(validator: Node, newVotingPower: int): bool = 
         val result = votingPowerChange(currentState, validator, newVotingPower)
         all {
-            result.hasError == false,
+            result.hasError() == false,
             currentState' = result.newState,
             trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower))
         }
@@ -142,7 +142,7 @@ module ccv_statemachine {
         val resultAndTimeout = deliverPacketToConsumer(currentState, receiver)
         val result = resultAndTimeout._1
         all {
-            result.hasError == false,
+            result.hasError() == false,
             currentState' = result.newState,
             trace' = trace.append(emptyAction.with("kind", "DeliverVscPacket").with("consumerChain", receiver))
         }
@@ -153,7 +153,7 @@ module ccv_statemachine {
         val resultAndTimeout = deliverPacketToProvider(currentState, sender)
         val result = resultAndTimeout._1
         all {
-            result.hasError == false,
+            result.hasError() == false,
             currentState' = result.newState,
             trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender))
         }
@@ -164,7 +164,7 @@ module ccv_statemachine {
         consumersToStop: Set[Chain]): bool = 
         val result = endAndBeginBlockForProvider(currentState, timeAdvancement, consumersToStart, consumersToStop)
         all {
-            result.hasError == false,
+            result.hasError() == false,
             currentState' = result.newState,
             trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForProvider").with("timeAdvancement", timeAdvancement).with("consumersToStart", consumersToStart).with("consumersToStop", consumersToStop))
         }
@@ -174,7 +174,7 @@ module ccv_statemachine {
         timeAdvancement: Time): bool = 
         val result = endAndBeginBlockForConsumer(currentState, chain, timeAdvancement)
         all {
-            result.hasError == false,
+            result.hasError() == false,
             currentState' = result.newState,
             trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForConsumer").with("consumerChain", chain).with("timeAdvancement", timeAdvancement))
         }

tests/difference/core/quint_model/ccv_test.qnt

@@ -20,7 +20,7 @@ module ccv_test {
             GetEmptyProtocolState,
             "validator",
             -1
-        ).hasError
+        ).hasError()
     }
 
     run VotingPowerOkTest =
@@ -30,7 +30,7 @@ module ccv_test {
             "validator",
             5
         )
-        not(result.hasError) and
+        not(result.hasError()) and
         result.newState.providerState.chainState.currentValidatorSet.keys().contains("validator") and
         result.newState.providerState.chainState.currentValidatorSet.get("validator") == 5
     }
@@ -48,7 +48,7 @@ module ccv_test {
             "validator",
             0
         )
-        not(finalResult.hasError) and
+        not(finalResult.hasError()) and
         finalResult.newState.providerState.chainState.currentValidatorSet.get("validator") == 0
     }
 
@@ -67,7 +67,7 @@ module ccv_test {
             0
         )
         // still should set the flag
-        not(finalResult.hasError) and
+        not(finalResult.hasError()) and
         finalResult.newState.providerState.providerValidatorSetChangedInThisBlock
     }
 
@@ -80,7 +80,7 @@ module ccv_test {
             "validator",
             0
         )
-        not(result.hasError) and
+        not(result.hasError()) and
         result.newState.providerState.chainState.votingPowerHistory == List()
     }
 
@@ -138,7 +138,7 @@ module ccv_test {
     {
         val result = DeliverPacketToProviderHappyPathTest_resultAndTimeout._1
         val timeout = DeliverPacketToProviderHappyPathTest_resultAndTimeout._2
-        not(result.hasError) and
+        not(result.hasError()) and
         not(timeout)
     }
 
@@ -147,7 +147,7 @@ module ccv_test {
         val result = DeliverPacketToProviderHappyPathTest_resultAndTimeout._1
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
-        not(result.hasError) and
+        not(result.hasError()) and
         newProviderState.receivedMaturations.size() == 1 and
         newConsumerState.outstandingPacketsToProvider.length() == 0
     }
@@ -170,7 +170,7 @@ module ccv_test {
         val timeout = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
-        not(result.hasError) and
+        not(result.hasError()) and
         timeout
     }
 
@@ -179,7 +179,7 @@ module ccv_test {
         val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1
         val newProviderState = result.newState.providerState
         val newConsumerState = result.newState.consumerStates.get("sender")
-        not(result.hasError) and
+        not(result.hasError()) and
         newProviderState.receivedMaturations.size() == 0 and
         newProviderState.consumerStatus.get("sender") == TIMEDOUT
     }