Skip to content

Commit

Permalink
spec/quint: invariant renamed, comments adapted
Browse files Browse the repository at this point in the history
  • Loading branch information
cason committed Nov 22, 2024
1 parent c022992 commit 85f2284
Showing 1 changed file with 6 additions and 7 deletions.
13 changes: 6 additions & 7 deletions specs/quint/specs/blocksync/bsyncStatemachine.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -34,30 +34,29 @@ module bsyncStatemachine {
)
)

/// A server only replies to a request
// Should be braken due to timeouts
/// A server only replies to a request received from a client.
/// This witness should report a scenario where a request timeouts, the
/// client submits a new one, and a late response is received.
val serverRespondsToRequestingPeersWitness = bsyncClients.keys().forall(c =>
responsesBuffer.get(c).forall(m =>
bsyncClients.get(c).openRequests.exists(req =>
matchingMessages(req, m))
)
)

/// A server only replies to a request (current or timed-out)
val serverRespondsToRequestingPeersInv = bsyncClients.keys().forall(c =>
/// A server only replies to a request received from a client.
/// The client request might have timed out.
val serverRespondsToRequestingPeersInvariant = bsyncClients.keys().forall(c =>
responsesBuffer.get(c).forall(m =>
bsyncClients.get(c).openRequests.union(expiredTimeouts.get(c))
.exists(req => matchingMessages(req, m))
)
)



//
// Actions
//


/// initializing the variables of the sync part of the state machine
action syncInit(validators) = all {
initClient(validators),
Expand Down

0 comments on commit 85f2284

Please sign in to comment.