spec/quint: re-tabbing bsyncMock.qnt

informalsystems · Nov 21, 2024 · 40142af · 40142af
1 parent 4c6836a
commit 40142af
Showing 1 changed file with 12 additions and 14 deletions.
diff --git 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" }))
 
-
-
 }