Skip to content

Commit

Permalink
Fix vsc timeouts should happen during endblock
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Nov 29, 2023
1 parent 680f3c4 commit 4238978
Showing 1 changed file with 10 additions and 8 deletions.
18 changes: 10 additions & 8 deletions tests/difference/core/quint_model/ccv.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -381,8 +381,17 @@ module ccv {
// forced stops, e.g. because a consumer timed out,
// will be added automatically.
consumersToStop: Set[Chain]): Result = {
// commit the current running validator set on chain
val currentProviderState = currentState.providerState

// check for Vsc timeouts
val timedOutConsumers = getRunningConsumers(currentProviderState).filter(
consumer =>
val res = TimeoutDueToVscTimeout(currentState, consumer)
res._1
)


// run the shared core chainState logic
val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement)
val providerStateAfterTimeAdvancement = currentProviderState.with(
"chainState", newChainState
Expand All @@ -392,13 +401,6 @@ module ccv {
"providerState", providerStateAfterTimeAdvancement
)

// check for Vsc timeouts
// needs to be done with the old provider state, since this happens during EndBlock
val timedOutConsumers = getRunningConsumers(currentProviderState).filter(
consumer =>
val res = TimeoutDueToVscTimeout(tmpState, consumer)
res._1
)

// send vsc packets
val providerStateAfterSending =
Expand Down

0 comments on commit 4238978

Please sign in to comment.