Skip to content

Commit

Permalink
spec/quint: re-tabbing client.qnt
Browse files Browse the repository at this point in the history
  • Loading branch information
cason committed Nov 20, 2024
1 parent 7532923 commit cfc493b
Showing 1 changed file with 7 additions and 11 deletions.
18 changes: 7 additions & 11 deletions specs/quint/specs/blocksync/client.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -87,14 +87,13 @@ module bsync_client {
so: SOBlock(p),
req: None}

/// we have received a blockstore entry (block and certificate).
/// now we need to generate a block output
pure def syncHandleBlockStoreEntry (s: BsyncClient, b: BlockStoreEntry) : ClientResult =
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlockStoreEntry(b),
req: None}

/// we have received a blockstore entry (block and certificate).
/// now we need to generate a block output
pure def syncHandleBlockStoreEntry (s: BsyncClient, b: BlockStoreEntry) : ClientResult =
{ sync: {...s, openRequests: Set(), // If we have parallelization we need to remove one element,
lastSyncedHeight: s.height }, // blockheight,
so: SOBlockStoreEntry(b),
req: None}

/// step of a client:
/// 1. update peer statuses, 2. if there is no open request, request something
Expand Down Expand Up @@ -148,8 +147,6 @@ module bsync_client {
so: SONoOutput,
req: None}



// State machine

var bsyncClients: Address -> BsyncClient
Expand Down Expand Up @@ -204,5 +201,4 @@ module bsync_client {
responsesBuffer' = responsesBuffer,
}


}

0 comments on commit cfc493b

Please sign in to comment.