spec/quint: invariant renamed, comments adapted

informalsystems · Nov 22, 2024 · b5de3e1 · b5de3e1
1 parent 0825086
commit b5de3e1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/specs/quint/specs/blocksync/blocksyncServer.qnt b/specs/quint/specs/blocksync/blocksyncServer.qnt
@@ -72,8 +72,6 @@ module blocksyncServer {
 
   var bsyncServers: Address -> Server
 
-
-
   //
   // Actions
   //

diff --git a/specs/quint/specs/blocksync/bsyncStatemachine.qnt b/specs/quint/specs/blocksync/bsyncStatemachine.qnt
@@ -25,8 +25,10 @@ module bsyncStatemachine {
   // Properties
   //
 
-  /// A request should only be sent to a server who has the requested data
-  val clientRequestsfromKnowingPeersInv = bsyncServers.keys().forall(s =>
+  /// A request should only be sent to a server who has reported, via status
+  /// message, having data for the requested height.
+  // FIXME: this assume no prunning, namely chain.length() == latestHeight.
+  val validRequestInvariant = bsyncServers.keys().forall(s =>
     requestsBuffer.get(s).forall(m =>
       m.height <= bsyncServers.get(s).chain.length()
     )
-Original file line number
+Diff line change
@@ Expand Up / @@ -72,8 +72,6 @@ module blocksyncServer { @@
       var bsyncServers: Address -> Server
       //
       // Actions
       //
@@ Expand Down @@