diff --git a/specs/quint/specs/blocksync/blocksyncClient.qnt b/specs/quint/specs/blocksync/blocksyncClient.qnt index 66265f531..6894cb87c 100644 --- a/specs/quint/specs/blocksync/blocksyncClient.qnt +++ b/specs/quint/specs/blocksync/blocksyncClient.qnt @@ -47,19 +47,19 @@ module blocksyncClient { /// Auxiliary function to iterate over the received status messages pure def updatePeerStatus (ps: Address -> BlockRange, msgs: Set[StatusMsg]) : Address -> BlockRange = msgs.fold(ps, (newStatus , msg) => - if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base? - newStatus.put(msg.peer, {base: msg.base, top: msg.top}) - else - newStatus + if (newStatus.get(msg.peer).top < msg.top) // TODO: think about base? + newStatus.put(msg.peer, {base: msg.base, top: msg.top}) + else + newStatus ) /// inform the synchronizer that consensus has entered height h pure def syncNewHeight (s: BsyncClient, h: Height) : BsyncClient = if (h <= s.height) - s + s else - { ... s, height: h, - openRequests: s.openRequests.filter(req => req.height >= h)} + { ... s, height: h, + openRequests: s.openRequests.filter(req => req.height >= h)} /// returned by the synchronizer: sync is the new state, so is the output towards /// the consensus driver, req are messages sent towards peers/servers @@ -70,30 +70,30 @@ module blocksyncClient { } /// We have received a certificate. now we need to issue the - /// corresponding block request and generate a certificate output. + /// corresponding block request and generate a certificate output. pure def syncHandleCertificate (s: BsyncClient, cert: Set[Vote], peer: str ) : ClientResult = - val blockReq = { client: s.id, - server: peer, - rtype: SyncBlock, - height: s.height} - { sync: {...s, openRequests: Set(blockReq)}, // If we have parallelization we need to be more precise here - so: SOCertificate(cert), - req: Some(blockReq)} + val blockReq = {client: s.id, + server: peer, + rtype: SyncBlock, + height: s.height} + { sync: {...s, openRequests: Set(blockReq)}, // If we have parallelization we need to be more precise here + so: SOCertificate(cert), + req: Some(blockReq)} - /// we have received a block. now we need to generate a block output + /// we have received a block. now we need to generate a block output pure def syncHandleBlock (s: BsyncClient, p: Proposal) : ClientResult = - { sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element, - lastSyncedHeight: s.height }, // blockheight, - so: SOBlock(p), - req: None} + { sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element, + lastSyncedHeight: s.height }, // blockheight, + so: SOBlock(p), + req: None} /// we have received a blockstore entry (block and certificate). - /// now we need to generate a block output + /// now we need to generate a block output pure def syncHandleBlockStoreEntry (s: BsyncClient, b: BlockStoreEntry) : ClientResult = - { sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element, - lastSyncedHeight: s.height }, // blockheight, - so: SOBlockStoreEntry(b), - req: None} + { sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element, + lastSyncedHeight: s.height }, // blockheight, + so: SOBlockStoreEntry(b), + req: None} /// step of a client: /// 1. update peer statuses, 2. if there is no open request, request something @@ -102,48 +102,48 @@ module blocksyncClient { val newPeerStates = updatePeerStatus(s.peerStatus, s.statusMsgs) val newS = { ...s, peerStatus: newPeerStates} if (s.lastSyncedHeight >= s.height) - // nothing to do - { sync: newS, - so: SONoOutput, - req: None} + // nothing to do + { sync: newS, + so: SONoOutput, + req: None} else - val goodPeers = s.peerStatus.keys().filter(p => newPeerStates.get(p).base <= s.height - and s.height <= newPeerStates.get(p).top ) - if (goodPeers.size() > 0) - if (s.openRequests.size() == 0) - // we start the sync "round" by asking for a certificate - val req = { client: s.id, - server: goodPeers.fold("", (acc, i) => i), //chooseSome(), - rtype: if (fullEntries) - SyncBlockStoreEntry - else - SyncCertificate, - height: s.height} - { sync: {... newS, openRequests: s.openRequests.union(Set(req))}, - so: SONoOutput, - req: Some(req) - } - else - // we issued a request before, let's see whether there is a response - if (s.responseMsgs.size()> 0) - val resp = s.responseMsgs.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization - val ns = {... newS, responseMsgs: newS.responseMsgs.exclude(Set(resp))} - match resp.response { - | RespBlock(prop) => syncHandleBlock(newS, prop) - | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) - | RespBlockStoreEntry(b) => syncHandleBlockStoreEntry(ns, b) - } - else - // I don't have response - // this might be timeout logic - { sync: newS, - so: SONoOutput, - req: None} - else - // no peers - { sync: newS, - so: SONoOutput, - req: None} + val goodPeers = s.peerStatus.keys().filter(p => newPeerStates.get(p).base <= s.height + and s.height <= newPeerStates.get(p).top ) + if (goodPeers.size() > 0) + if (s.openRequests.size() == 0) + // we start the sync "round" by asking for a certificate + val req = { client: s.id, + server: goodPeers.fold("", (acc, i) => i), //chooseSome(), + rtype: if (fullEntries) + SyncBlockStoreEntry + else + SyncCertificate, + height: s.height} + { sync: {... newS, openRequests: s.openRequests.union(Set(req))}, + so: SONoOutput, + req: Some(req) + } + else + // we issued a request before, let's see whether there is a response + if (s.responseMsgs.size()> 0) + val resp = s.responseMsgs.fold(emptyResponseMsg, (acc, i) => i) //chooseSome() // in the future there might be parallelization + val ns = {... newS, responseMsgs: newS.responseMsgs.exclude(Set(resp))} + match resp.response { + | RespBlock(prop) => syncHandleBlock(newS, prop) + | RespCertificate(cert) => syncHandleCertificate(newS, cert, goodPeers.fold("", (s,x) => x)) + | RespBlockStoreEntry(b) => syncHandleBlockStoreEntry(ns, b) + } + else + // I don't have response + // this might be timeout logic + { sync: newS, + so: SONoOutput, + req: None} + else + // no peers + { sync: newS, + so: SONoOutput, + req: None} /// step of a client upon timeout: We send the same request to a different server // FIXME: what to do if goodPeers is empty? diff --git a/specs/quint/specs/blocksync/bsyncStatemachine.qnt b/specs/quint/specs/blocksync/bsyncStatemachine.qnt index d9e76541c..bf18ac3da 100644 --- a/specs/quint/specs/blocksync/bsyncStatemachine.qnt +++ b/specs/quint/specs/blocksync/bsyncStatemachine.qnt @@ -63,15 +63,12 @@ module bsyncStatemachine { ) /// Every request will eventually terminate. - /// We cannot verify it. + /// We cannot currently verify it with Apalache. temporal terminationRequest = bsyncClients.keys().forall(c => always (bsyncClients.get(c).openRequests.forall(req => eventually (not(bsyncClients.get(c).openRequests.contains(req)))))) - - - // // Actions // diff --git a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt index 4dfd06ad2..cd85a21f9 100644 --- a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt +++ b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt @@ -29,8 +29,8 @@ module bsyncWithConsensus { // // With the default `init` action, it is unlikely to observe this scenario, // even with 200 steps (around 30 minutes) execution: - // $ quint run --invariant anyClientOuputWitness bsyncWithConsensus.qnt - val anyClientOuputWitness = Correct.forall(p => + // $ quint run --invariant anyClientOutputWitness bsyncWithConsensus.qnt + val anyClientOutputWitness = Correct.forall(p => system.get(p).incomingSyncCertificates == Set()) // @@ -147,7 +147,7 @@ module bsyncWithConsensus { .then(all{unchangedAll, syncDeliverResp("v4")}) .then(syncStepClient("v4", putSyncOutputIntoNode, false)) // ask for block and give certificate to node .expect(system.get("v4").incomingSyncCertificates.size() > 0) - .expect(not(anyClientOuputWitness)) + .expect(not(anyClientOutputWitness)) .then(all{unchangedAll, syncDeliverReq("v2")}) .then(all{unchangedAll, syncStepServer("v2")}) .then(all{unchangedAll, syncDeliverResp("v4")}) diff --git a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt index 532bb1d7d..c473c83e4 100644 --- a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt +++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt @@ -27,11 +27,11 @@ module bsyncWithMockedConsensus { /// received a certificate, or a block, or both (a block store entry). // // Use the `initSetup` initialization to have faster runs: - // $ quint run --invariant anyClientOuputWitness bsyncWithMockedConsensus.qnt --init initSetup --seed=0x131cbef6acef78 + // $ quint run --invariant anyClientOutputWitness bsyncWithMockedConsensus.qnt --init initSetup --seed=0x131cbef6acef78 // // With the default `init` action more steps are required, e.g.: - // $ quint run --invariant anyClientOuputWitness bsyncWithMockedConsensus.qnt --max-steps 100 --seed=0x4e9afa1aeb815 - val anyClientOuputWitness = Correct.forall(p => + // $ quint run --invariant anyClientOutputWitness bsyncWithMockedConsensus.qnt --max-steps 100 --seed=0x4e9afa1aeb815 + val anyClientOutputWitness = Correct.forall(p => outputs.get(p).length() > 0 implies outputs.get(p).foldl(Set(), (s, x) => s.union(Set(x))).forall(so => so == SONoOutput)