From 18e7f254cbd6ecf15231f5b161cce652caef3521 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 13 Mar 2024 11:25:06 +0100 Subject: [PATCH] Remove more conflict markers --- tests/mbt/model/ccv_boundeddrift.qnt | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index 125de8004e..eb59781124 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -104,7 +104,6 @@ module ccv_boundeddrift { nondet timeAdvancement = possibleAdvancements.oneOf() EndAndBeginBlockForConsumer(chain, timeAdvancement), } -<<<<<<< HEAD } action stepBoundedDriftKeyAssignment = any { @@ -119,8 +118,6 @@ module ccv_boundeddrift { nondetKeyAssignment, StepOptIn, StepOptOut, -======= - }, // advance a block for the provider val maxAdv = findMaxTimeAdvancement(GetChainState(Ccvt::PROVIDER_CHAIN), GetOtherChainStates(Ccvt::PROVIDER_CHAIN), maxDrift) @@ -136,14 +133,8 @@ module ccv_boundeddrift { nondet timeAdvancement = oneOf(possibleAdvancements) EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), } ->>>>>>> main } - - action stepBoundedDriftKeyAssignment = any { - stepBoundedDrift, - nondetKeyAssignment, - } - + // INVARIANT // The maxDrift between chains is never exceeded. // This *should* be ensured by the step function.