refactor(spec/quint): blocksync files and modules nomenclature (#592)

* mock fix

* test

* spec/quint: re-tabbing bsyncMock.qnt

* spec/quint: bsyncWith* main executable models

* spec/quint: change type of mocked consensus outputs

* spec/quint: rename main state machine model

* spec/quint: fixed mocked output update

* spec/quint: simplifying the import logic

* spec/quint: client and server modules renamed

---------

Co-authored-by: Josef Widder <[email protected]>

specs/quint/specs/blocksync/blocksync.qnt

@@ -1,4 +1,8 @@
 // -*- mode: Bluespec; -*-
+//
+// General definitions for blocksync protocol and state machine for
+// the client-server communication, namely, the network.
+//
 
 module blocksync {
 

specs/quint/specs/blocksync/client.qnt → specs/quint/specs/blocksync/blocksyncClient.qnt

@@ -1,8 +1,9 @@
 // -*- mode: Bluespec; -*-
 //
-// Blocksync protocol: client side.
+// Blocksync protocol: client side that requests and downloads decisions.
+//
 
-module bsync_client {
+module blocksyncClient {
 
   import blocksync.* from "./blocksync"
 

specs/quint/specs/blocksync/server.qnt → specs/quint/specs/blocksync/blocksyncServer.qnt

@@ -1,8 +1,9 @@
 // -*- mode: Bluespec; -*-
 //
-// Blocksync protocol: server side.
+// Blocksync protocol: server side, replies to client requests.
+//
 
-module bsync_server {
+module blocksyncServer {
 
   import blocksync.* from "./blocksync"
 

specs/quint/specs/blocksync/syncStatemachine.qnt → specs/quint/specs/blocksync/bsyncStatemachine.qnt

@@ -1,12 +1,17 @@
 // -*- mode: Bluespec; -*-
+//
+// State machine for the block sync protocol.
+//
 
-module syncStatemachine {
+module bsyncStatemachine {
 
-  // General definitions
   import blocksync.* from "./blocksync"
+  import blocksyncClient.* from "./blocksyncClient"
+  import blocksyncServer.* from "./blocksyncServer"
 
-  import bsync_client.* from "./client"
-  import bsync_server.* from "./server"
+  export blocksync.*
+  export blocksyncClient.*
+  export blocksyncServer.*
 
   // ****************************************************************************
   // State machine

specs/quint/specs/blocksync/bsyncWithConsensus.qnt

@@ -1,11 +1,13 @@
 // -*- mode: Bluespec; -*-
+//
+// Blocksync executable model running together with the consensus logic.
+//
 
 module bsyncWithConsensus {
-
-  import blocksync.* from "./blocksync"
-  import bsync_client.* from "./client"
-  import bsync_server.* from "./server"
 
+  import bsyncStatemachine.* from "./bsyncStatemachine"
+
+  /// Consensus state machine setup
   import statemachineAsync(
     validators = Set("v1", "v2", "v3", "v4"),
     validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
@@ -15,8 +17,6 @@ module bsyncWithConsensus {
     Heights = Set(0) // , 1, 2, 3)
   ).* from "../statemachineAsync"
 
-  import syncStatemachine.* from "./syncStatemachine"
-
   /// initialize consensus and block sync
   action initAll = all {
     init,
@@ -117,7 +117,7 @@ module bsyncWithConsensus {
   action syncStep =
     nondet v = oneOf(Correct)
     pureSyncStep(v, unchangedAll)
-  
+
   /// a simple scenario where v4 starts height h
   run syncCycle(h) =
     newHeightActionAll("v4", validatorSet, h)
@@ -153,17 +153,17 @@ module bsyncWithConsensus {
     initHeight(2)
     // FIXME: I had to put it here, instead of syncCycle(h)
     // This is not ideal, but it works.
-    .then(syncUpdateServer("v2"))     
+    .then(syncUpdateServer("v2"))
     .then(newHeightActionAll("v4", validatorSet, 0))
-    .then(all{unchangedAll, syncStatusStep("v2")}) 
-    .then(all{unchangedAll, syncDeliverStatus("v4")})   
+    .then(all{unchangedAll, syncStatusStep("v2")})
+    .then(all{unchangedAll, syncDeliverStatus("v4")})
     .then(syncStepClient("v4", putSyncOutputIntoNode, 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{unchangedAll, syncStatusStep("v3")}) 
-    .then(all{unchangedAll, syncDeliverStatus("v4")}) 
+    .then(syncUpdateServer("v3"))
+    .then(all{unchangedAll, syncStatusStep("v3")})
+    .then(all{unchangedAll, syncDeliverStatus("v4")})
     // v4's request to v2 times out...
     .then(all{unchangedAll, syncClientTimeout("v4")})
     // after handling the timeout a request for certificate is sent to v3

specs/quint/specs/blocksync/bsyncMock.qnt → specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt

@@ -1,27 +1,24 @@
 // -*- mode: Bluespec; -*-
+//
+// Blocksync executable model running with a mocked consensus logic.
+//
 
-module bsyncMock {
+module bsyncWithMockedConsensus {
 
-  import blocksync.* from "./blocksync"
-  import bsync_client.* from "./client"
-  import bsync_server.* from "./server"
-  import syncStatemachine.* from "./syncStatemachine"
+  import bsyncStatemachine.* from "./bsyncStatemachine"
 
   val validators = Set("v1", "v2", "v3", "v4")
   val Correct = Set("v2", "v3", "v4")
   val validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1)
 
-  type Output = {
-    v : Address,
-    out: BsyncClientOutput
-  }
+  // State machine
 
-  var outputs: List[Output]
+  var outputs: Address -> List[BsyncClientOutput]
   var chains: Address -> List[BlockStoreEntry]
 
   /// initialize consensus and synchronizer
   action initMockedConsensus = all {
-    outputs' = [],
+    outputs' = validators.mapBy(_ => []),
     chains' = Correct.mapBy(_ => []),
     syncInit(validators)
   }
@@ -67,7 +64,8 @@ module bsyncMock {
   }
 
   action writeAction(v, so) = all {
-    outputs' = outputs.append({v: v, out: so}),
+    val updateOutput = outputs.get(v).append(so)
+    outputs' = outputs.put(v, updateOutput),
     chains' = chains,
   }
 
@@ -104,7 +102,7 @@ module bsyncMock {
         { decision: mkProposal( "", i, 0, "", 0),
           commit: Set() } ))
     ),
-    outputs' = [],
+    outputs' = validators.mapBy(_ => []),
     syncInit(validators)
    }