From d71dad347a3a9d39b135e6d2e9479fffb0eba64d Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 13 Oct 2023 10:18:49 +0200 Subject: [PATCH] Remove hasError field and make it a function --- tests/difference/core/quint_model/ccv.qnt | 13 ++++++------- .../core/quint_model/ccv_statemachine.qnt | 10 +++++----- tests/difference/core/quint_model/ccv_test.qnt | 18 +++++++++--------- 3 files changed, 20 insertions(+), 21 deletions(-) diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index e23bbb8532..e1d78c273b 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/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 diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt index 9585073224..cb62f560ee 100644 --- a/tests/difference/core/quint_model/ccv_statemachine.qnt +++ b/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)) } diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt index 621df175c2..6bbe884d52 100644 --- a/tests/difference/core/quint_model/ccv_test.qnt +++ b/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 }