From 00c811eafcd5e17e47446190d02e0b3e006ceb1b Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Thu, 21 Nov 2024 09:36:49 +0100
Subject: [PATCH 1/9] mock fix

---
 specs/quint/specs/blocksync/bsyncMock.qnt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/specs/quint/specs/blocksync/bsyncMock.qnt b/specs/quint/specs/blocksync/bsyncMock.qnt
index 1aa090f35..6a3e1748c 100644
--- a/specs/quint/specs/blocksync/bsyncMock.qnt
+++ b/specs/quint/specs/blocksync/bsyncMock.qnt
@@ -57,7 +57,7 @@ module bsyncMock {
 
   /// Update server v from the consensus' blockchain
   /// This abstracts as pull-based mechanism: the server consults the chain state.
-  action mockUpdateServer(v) = all {
+  action syncUpdateServer(v) = all {
     all {
       updateServer(v, chains.get(v)),
       unchangedClient,
@@ -87,8 +87,8 @@ module bsyncMock {
     any {
       pureSyncStep(v, unchangedMock),
       // consensus-specific steps
-      syncStepClient(v, writeAction),  // is checking if there are responses and check whether it need to requ
-      mockUpdateServer(v),
+      syncStepClient(v, writeAction, false),  // is checking if there are responses and check whether it need to requ
+      syncUpdateServer(v),
       newHeightActionAll(v, validators, chains.get(v).length()),
       decideMock(v),
    }

From 4c6836a3c16e088463a0143892f600682c9a30b3 Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Thu, 21 Nov 2024 09:59:39 +0100
Subject: [PATCH 2/9] test

---
 specs/quint/specs/blocksync/bsyncMock.qnt | 38 ++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

diff --git a/specs/quint/specs/blocksync/bsyncMock.qnt b/specs/quint/specs/blocksync/bsyncMock.qnt
index 6a3e1748c..913cf1f75 100644
--- a/specs/quint/specs/blocksync/bsyncMock.qnt
+++ b/specs/quint/specs/blocksync/bsyncMock.qnt
@@ -9,6 +9,7 @@ module bsyncMock {
 
   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,
@@ -50,7 +51,7 @@ module bsyncMock {
   /// Environment sends the node to the next height.
   /// This implicitly requires `decideMock(v)` to be previous executed.
   action newHeightActionAll(v, valset, h) = all {
-    chains.get(v).length() == h, // precondition for calling this
+    //chains.get(v).length() == h, // precondition for calling this
     newHeightActionSync(v, valset, h),
     unchangedMock,
   }
@@ -92,4 +93,39 @@ module bsyncMock {
       newHeightActionAll(v, validators, chains.get(v).length()),
       decideMock(v),
    }
+
+
+  /// An action to set up an initial state with some nodes already decided up to height h
+  /// this sets up an initial state where v4 starts late, and v2 and v3 have reached
+  /// height h
+  action initHeight(h) = all {
+    val special = "v4" // TODO proper selection from correct set
+    chains' = Correct.mapBy(v => range(0, h).foldl(List(), (acc, i) => acc.append(
+        { decision: mkProposal( "", i, 0, "", 0),
+          commit: Set() } ))
+    ),            
+    outputs' = [],       
+    syncInit(validators)
+   }
+  
+  run lausanneRetreat =
+    initHeight(2)
+    .then(syncUpdateServer("v2"))     
+    .then(newHeightActionAll("v4", validatorSet, 0))
+    .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")}) 
+    // 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" }))
+
+
+
 }

From 40142af3d70eec76dfe4f4a58de4bb4d2dedbe5d Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:07:51 +0100
Subject: [PATCH 3/9] 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" }))
 
-
-
 }

From 2544f640118afcbb3b1dd8f8cd2cbe455f6fda1a Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:17:29 +0100
Subject: [PATCH 4/9] spec/quint: bsyncWith* main executable models

---
 .../specs/blocksync/bsyncWithConsensus.qnt    | 21 +++++++++++--------
 ...cMock.qnt => bsyncWithMockedConsensus.qnt} |  5 ++++-
 2 files changed, 16 insertions(+), 10 deletions(-)
 rename specs/quint/specs/blocksync/{bsyncMock.qnt => bsyncWithMockedConsensus.qnt} (97%)

diff --git a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
index 0b1dd4964..4196e5ed4 100644
--- a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
@@ -1,7 +1,10 @@
 // -*- 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"
@@ -16,7 +19,7 @@ module bsyncWithConsensus {
   ).* from "../statemachineAsync"
 
   import syncStatemachine.* from "./syncStatemachine"
-  
+
   /// initialize consensus and block sync
   action initAll = all {
     init,
@@ -117,7 +120,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 +156,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
diff --git a/specs/quint/specs/blocksync/bsyncMock.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
similarity index 97%
rename from specs/quint/specs/blocksync/bsyncMock.qnt
rename to specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
index fbcca0da1..81da61eca 100644
--- a/specs/quint/specs/blocksync/bsyncMock.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
@@ -1,6 +1,9 @@
 // -*- mode: Bluespec; -*-
+//
+// Blocksync executable model running with a mocked consensus logic.
+//
 
-module bsyncMock {
+module bsyncWithMockedConsensus {
 
   import blocksync.* from "./blocksync"
   import bsync_client.* from "./client"

From 2dab905f97ce69efcdc83995759f1c4e08e29a68 Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:20:52 +0100
Subject: [PATCH 5/9] spec/quint: change type of mocked consensus outputs

---
 .../specs/blocksync/bsyncWithMockedConsensus.qnt    | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
index 81da61eca..587ff4263 100644
--- a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
@@ -14,17 +14,14 @@ module bsyncWithMockedConsensus {
   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)
   }
@@ -70,7 +67,7 @@ module bsyncWithMockedConsensus {
   }
 
   action writeAction(v, so) = all {
-    outputs' = outputs.append({v: v, out: so}),
+    outputs' = outputs.put(v, so),
     chains' = chains,
   }
 
@@ -107,7 +104,7 @@ module bsyncWithMockedConsensus {
         { decision: mkProposal( "", i, 0, "", 0),
           commit: Set() } ))
     ),
-    outputs' = [],
+    outputs' = validators.mapBy(_ => []),
     syncInit(validators)
    }
 

From ebaaad6ced97708315026d489b8e592a7d410a08 Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:23:47 +0100
Subject: [PATCH 6/9] spec/quint: rename main state machine model

---
 .../{syncStatemachine.qnt => bsyncStatemachine.qnt}          | 5 ++++-
 specs/quint/specs/blocksync/bsyncWithConsensus.qnt           | 2 +-
 specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt     | 2 +-
 3 files changed, 6 insertions(+), 3 deletions(-)
 rename specs/quint/specs/blocksync/{syncStatemachine.qnt => bsyncStatemachine.qnt} (97%)

diff --git a/specs/quint/specs/blocksync/syncStatemachine.qnt b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
similarity index 97%
rename from specs/quint/specs/blocksync/syncStatemachine.qnt
rename to specs/quint/specs/blocksync/bsyncStatemachine.qnt
index 7bc5c699c..9c1d1ed15 100644
--- a/specs/quint/specs/blocksync/syncStatemachine.qnt
+++ b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
@@ -1,6 +1,9 @@
 // -*- mode: Bluespec; -*-
+//
+// State machine for the block sync protocol.
+//
 
-module syncStatemachine {
+module bsyncStatemachine {
 
   // General definitions
   import blocksync.* from "./blocksync"
diff --git a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
index 4196e5ed4..87c8e4d79 100644
--- a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
@@ -18,7 +18,7 @@ module bsyncWithConsensus {
     Heights = Set(0) // , 1, 2, 3)
   ).* from "../statemachineAsync"
 
-  import syncStatemachine.* from "./syncStatemachine"
+  import bsyncStatemachine.* from "./bsyncStatemachine"
 
   /// initialize consensus and block sync
   action initAll = all {
diff --git a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
index 587ff4263..735d0aaed 100644
--- a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
@@ -8,7 +8,7 @@ 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")

From 72b102a15d3e985fc2e9499e9b015e523a056436 Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:44:07 +0100
Subject: [PATCH 7/9] spec/quint: fixed mocked output update

---
 specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
index 735d0aaed..2b25cbba0 100644
--- a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
@@ -67,7 +67,8 @@ module bsyncWithMockedConsensus {
   }
 
   action writeAction(v, so) = all {
-    outputs' = outputs.put(v, so),
+    val updateOutput = outputs.get(v).append(so)
+    outputs' = outputs.put(v, updateOutput),
     chains' = chains,
   }
 

From 8b3829f6ef4e236e10571e14f2720c4c9e41858b Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:48:47 +0100
Subject: [PATCH 8/9] spec/quint: simplifying the import logic

---
 specs/quint/specs/blocksync/bsyncStatemachine.qnt        | 6 ++++--
 specs/quint/specs/blocksync/bsyncWithConsensus.qnt       | 7 ++-----
 specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt | 3 ---
 3 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/specs/quint/specs/blocksync/bsyncStatemachine.qnt b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
index 9c1d1ed15..25ec7461d 100644
--- a/specs/quint/specs/blocksync/bsyncStatemachine.qnt
+++ b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
@@ -5,12 +5,14 @@
 
 module bsyncStatemachine {
 
-  // General definitions
   import blocksync.* from "./blocksync"
-
   import bsync_client.* from "./client"
   import bsync_server.* from "./server"
 
+  export blocksync.*
+  export bsync_client.*
+  export bsync_server.*
+
   // ****************************************************************************
   // State machine
   // ****************************************************************************
diff --git a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
index 87c8e4d79..1ff79e3c7 100644
--- a/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithConsensus.qnt
@@ -5,10 +5,9 @@
 
 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),
@@ -18,8 +17,6 @@ module bsyncWithConsensus {
     Heights = Set(0) // , 1, 2, 3)
   ).* from "../statemachineAsync"
 
-  import bsyncStatemachine.* from "./bsyncStatemachine"
-
   /// initialize consensus and block sync
   action initAll = all {
     init,
diff --git a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
index 2b25cbba0..ce6cb8f74 100644
--- a/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
+++ b/specs/quint/specs/blocksync/bsyncWithMockedConsensus.qnt
@@ -5,9 +5,6 @@
 
 module bsyncWithMockedConsensus {
 
-  import blocksync.* from "./blocksync"
-  import bsync_client.* from "./client"
-  import bsync_server.* from "./server"
   import bsyncStatemachine.* from "./bsyncStatemachine"
 
   val validators = Set("v1", "v2", "v3", "v4")

From 3d54146409f2db9c9188c84918085beca1f37e7e Mon Sep 17 00:00:00 2001
From: Daniel Cason <daniel.cason@informal.systems>
Date: Thu, 21 Nov 2024 10:54:13 +0100
Subject: [PATCH 9/9] spec/quint: client and server modules renamed

---
 specs/quint/specs/blocksync/blocksync.qnt                 | 4 ++++
 .../specs/blocksync/{client.qnt => blocksyncClient.qnt}   | 5 +++--
 .../specs/blocksync/{server.qnt => blocksyncServer.qnt}   | 5 +++--
 specs/quint/specs/blocksync/bsyncStatemachine.qnt         | 8 ++++----
 4 files changed, 14 insertions(+), 8 deletions(-)
 rename specs/quint/specs/blocksync/{client.qnt => blocksyncClient.qnt} (98%)
 rename specs/quint/specs/blocksync/{server.qnt => blocksyncServer.qnt} (97%)

diff --git a/specs/quint/specs/blocksync/blocksync.qnt b/specs/quint/specs/blocksync/blocksync.qnt
index f525817a5..9b236e296 100644
--- a/specs/quint/specs/blocksync/blocksync.qnt
+++ b/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 {
 
diff --git a/specs/quint/specs/blocksync/client.qnt b/specs/quint/specs/blocksync/blocksyncClient.qnt
similarity index 98%
rename from specs/quint/specs/blocksync/client.qnt
rename to specs/quint/specs/blocksync/blocksyncClient.qnt
index 9bc367298..5485aba3f 100644
--- a/specs/quint/specs/blocksync/client.qnt
+++ b/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"
 
diff --git a/specs/quint/specs/blocksync/server.qnt b/specs/quint/specs/blocksync/blocksyncServer.qnt
similarity index 97%
rename from specs/quint/specs/blocksync/server.qnt
rename to specs/quint/specs/blocksync/blocksyncServer.qnt
index 659d54b60..d82756cf3 100644
--- a/specs/quint/specs/blocksync/server.qnt
+++ b/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"
 
diff --git a/specs/quint/specs/blocksync/bsyncStatemachine.qnt b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
index 25ec7461d..8f3fe284f 100644
--- a/specs/quint/specs/blocksync/bsyncStatemachine.qnt
+++ b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
@@ -6,12 +6,12 @@
 module bsyncStatemachine {
 
   import blocksync.* from "./blocksync"
-  import bsync_client.* from "./client"
-  import bsync_server.* from "./server"
+  import blocksyncClient.* from "./blocksyncClient"
+  import blocksyncServer.* from "./blocksyncServer"
 
   export blocksync.*
-  export bsync_client.*
-  export bsync_server.*
+  export blocksyncClient.*
+  export blocksyncServer.*
 
   // ****************************************************************************
   // State machine