From 40142af3d70eec76dfe4f4a58de4bb4d2dedbe5d Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Thu, 21 Nov 2024 10:07:51 +0100 Subject: [PATCH] spec/quint: re-tabbing bsyncMock.qnt --- specs/quint/specs/blocksync/bsyncMock.qnt | 26 +++++++++++------------ 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/specs/quint/specs/blocksync/bsyncMock.qnt b/specs/quint/specs/blocksync/bsyncMock.qnt index 913cf1f75..fbcca0da1 100644 --- a/specs/quint/specs/blocksync/bsyncMock.qnt +++ b/specs/quint/specs/blocksync/bsyncMock.qnt @@ -28,11 +28,11 @@ module bsyncMock { action unchangedMock = all { outputs' = outputs, - chains' = chains, + chains' = chains, } /// Consensus mocked logic decides the latest height. - /// The blockchain increases in size. + /// The blockchain increases in size. /// The server becomes aware of that once `updateServer` is invoked. /// The client becomes aware of that once `newHeightAction` is invoked. /// This is an abstract version. We just add a (mocked) block with the right @@ -88,7 +88,7 @@ module bsyncMock { any { pureSyncStep(v, unchangedMock), // consensus-specific steps - syncStepClient(v, writeAction, false), // is checking if there are responses and check whether it need to requ + syncStepClient(v, writeAction, false), syncUpdateServer(v), newHeightActionAll(v, validators, chains.get(v).length()), decideMock(v), @@ -103,29 +103,27 @@ module bsyncMock { chains' = Correct.mapBy(v => range(0, h).foldl(List(), (acc, i) => acc.append( { decision: mkProposal( "", i, 0, "", 0), commit: Set() } )) - ), - outputs' = [], + ), + outputs' = [], syncInit(validators) } - + run lausanneRetreat = initHeight(2) - .then(syncUpdateServer("v2")) + .then(syncUpdateServer("v2")) .then(newHeightActionAll("v4", validatorSet, 0)) - .then(all{unchangedMock, syncStatusStep("v2")}) - .then(all{unchangedMock, syncDeliverStatus("v4")}) + .then(all{unchangedMock, syncStatusStep("v2")}) + .then(all{unchangedMock, syncDeliverStatus("v4")}) .then(syncStepClient("v4", writeAction, false)) // ask for certificate // request for certificate is sent to v2 .expect(requestsBuffer.get("v2").contains({ client: "v4", height: 0, rtype: SyncCertificate, server: "v2" })) // v3 wakes up and sends it status to v4 - .then(syncUpdateServer("v3")) - .then(all{unchangedMock, syncStatusStep("v3")}) - .then(all{unchangedMock, syncDeliverStatus("v4")}) + .then(syncUpdateServer("v3")) + .then(all{unchangedMock, syncStatusStep("v3")}) + .then(all{unchangedMock, syncDeliverStatus("v4")}) // v4's request to v2 times out... .then(all{unchangedMock, syncClientTimeout("v4")}) // after handling the timeout a request for certificate is sent to v3 .expect(requestsBuffer.get("v3").contains({ client: "v4", height: 0, rtype: SyncCertificate, server: "v3" })) - - }