diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index d0a3a525ef..d1727bb515 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -17,16 +17,21 @@ module ccv_types { id: VscId, // the new validator set. in the implementation, this would be a list of validator updates validatorSet: ValidatorSet, - // the time at which the packet was sent. used to check whether packets have timed out. - sendingTime: Time + // the time at which the packet was sent. + sendingTime: Time, + // the time (on the receiver) at which the packet will time out + timeoutTime: Time + } type VscMaturedPacket = { // the id of the VscPacket that matured id: VscId, - // the time at which the packet was sent. used to check whether packets have timed out. - sendingTime: Time + // the time at which the packet was sent. + sendingTime: Time, + // the time (on the receiver) at which the packet will time out + timeoutTime: Time } @@ -276,7 +281,7 @@ module ccv { (Err("No outstanding packets to deliver"), false) } else { val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() - if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.runningTimestamp) { + if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) { // drop consumer val result = stopConsumers( currentState.providerState.consumerStatus, @@ -325,7 +330,7 @@ module ccv { } else { val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() // check if the consumer timed out - if (packet.sendingTime + CcvTimeout.get(PROVIDER_CHAIN) < currentState.consumerStates.get(receiver).chainState.runningTimestamp) { + if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) { // drop consumer val result = stopConsumers( currentState.providerState.consumerStatus, @@ -492,7 +497,8 @@ module ccv { maturedPackets.transform( packet => { id: packet.id, - sendingTime: newChainState.runningTimestamp + sendingTime: newChainState.runningTimestamp, + timeoutTime: newChainState.runningTimestamp + CcvTimeout.get(chain) } ) ) @@ -632,7 +638,8 @@ module ccv { List({ id: providerState.runningVscId, validatorSet: providerState.chainState.currentValidatorSet, - sendingTime: providerState.chainState.runningTimestamp + sendingTime: providerState.chainState.runningTimestamp, + timeoutTime: providerState.chainState.runningTimestamp + CcvTimeout.get(PROVIDER_CHAIN) }) } else { List() diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt index 0c21dffc86..4889fd5061 100644 --- a/tests/difference/core/quint_model/ccv_model.qnt +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -230,6 +230,7 @@ module ccv_model { id: 0, validatorSet: Map(), sendingTime: 9999999999999 * Second, + timeoutTime: 9999999999999 * Second, } packets.fold( latestPossiblePacket, @@ -241,6 +242,7 @@ module ccv_model { id: 0, validatorSet: Map(), sendingTime: -9999999999 * Second, + timeoutTime: -9999999999 * Second, } packets.fold( earliestPossiblePacket, @@ -257,18 +259,21 @@ module ccv_model { id: 1, validatorSet: Map(), sendingTime: 1 * Second, + timeoutTime: 1 * Second, } val packet2 = { id: 2, validatorSet: Map(), sendingTime: 2 * Second, + timeoutTime: 2 * Second, } val packet3 = { id: 3, validatorSet: Map(), sendingTime: 3 * Second, + timeoutTime: 3 * Second, } all { assert(earliest(Set(packet1, packet2, packet3)) == packet1),