Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Model ledgerBranches sparsely. #6138

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Model ledgerBranches sparsely. #6138

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
230c2be
Make TypeOK an invariant of all configs.
lemmy Apr 19, 2024
eeaa616
Refactor modeling of ledgerBranch[i] from seq into function.
lemmy Apr 19, 2024
fbf6ab2
Merge branch 'main' into mku-SparseLedger
achamayou Apr 23, 2024
fd01a84
Merge branch 'main' into mku-SparseLedger
lemmy Apr 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion tla/consistency/ExternalHistory.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,37 +3,37 @@
\* The history differs for traditional client histories, as clients receive responses to
\* transactions before they have been committed.

EXTENDS Naturals, Sequences, SequencesExt, FiniteSets, FiniteSetsExt

Check notice on line 6 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The EXTENDS clause includes modules that are not part of the standard TLA+ library, such as SequencesExt and FiniteSetsExt, which suggests they are custom modules defined elsewhere in the specification context.

\* Event types recorded in the history
\* Note that transaction status requests are not modelled to reduce state space
\* Currently only read-write (Rw) transactions and read-only (Ro) transactions are modelled
\* Both transaction types are modelled as forward-always transactions
\* This could be extended to support more types of read-only transactions

Check notice on line 12 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment mentions that "Both transaction types are modelled as forward-always transactions" which is consistent with the TLA+ declarations of `RwTxRequest`, `RwTxResponse`, `RoTxRequest`, and `RoTxResponse` as constants, implying that they are always moving forward in the model.
CONSTANTS RwTxRequest, RwTxResponse, RoTxRequest, RoTxResponse, TxStatusReceived


\* Transaction statuses
\* This model does not include the unknown and pending status to reduce state space
CONSTANTS CommittedStatus, InvalidStatus

Check notice on line 18 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment states that the model does not include the unknown and pending status to reduce state space, which is consistent with the TLA+ declarations of `CommittedStatus` and `InvalidStatus` as the only elements of `TxStatuses`.
TxStatuses == {
CommittedStatus,
InvalidStatus

Check failure on line 21 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about not including unknown and pending status is inconsistent with the TLA+ definition of `TxStatuses` which includes `InvalidStatus`. The term "invalid" is not equivalent to "unknown" or "pending", and the comment does not mention "invalid" status.
}

\* Views start at 1, 0 is used a null value

Check notice on line 24 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "Views start at 1, 0 is used a null value" is consistent with the definition of Views as Nat, since Nat in TLA+ starts at 1, and the comment implies that 0 is treated specially.
Views == Nat

Check failure on line 25 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about views starting at 1 is inconsistent with the TLA+ definition of `Views` as `Nat`, which includes 0. The comment implies that 0 should not be a valid view, but `Nat` allows it.

\* Sequence numbers start at 1, 0 is used a null value

Check notice on line 27 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "Sequence numbers start at 1, 0 is used a null value" is consistent with the definition of SeqNums as Nat, for the same reason as the Views.
SeqNums == Nat

Check notice on line 28 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about views and sequence numbers starting at 1 and using 0 as a null value is consistent with the TLA+ definitions of `Views` and `SeqNums` as `Nat`, since `Nat` includes 0 and all positive integers.

Check failure on line 28 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about sequence numbers starting at 1 is inconsistent with the TLA+ definition of `SeqNums` as `Nat`, which includes 0. The comment implies that 0 should not be a valid sequence number, but `Nat` allows it.

\* TxIDs consist of a view and sequence number and thus start at (1,1)
TxIDs == Views \X SeqNums

Check failure on line 31 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about `TxIDs` starting at (1,1) is inconsistent with the TLA+ definition of `TxIDs` as `Views \X SeqNums`, since both `Views` and `SeqNums` include 0, thus (0,0) is included in `TxIDs` which contradicts the comment.

\* This models uses a dummy application where read-write transactions
\* append an integer to a list and then reads the list
\* Read-only transactions simply read the list
Txs == Nat

Check notice on line 36 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about the dummy application and the definition of Txs as Nat are consistent, as the comment describes a simple model where transactions are represented by natural numbers.

Check notice on line 36 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment describes a dummy application where read-write transactions append an integer to a list and read-only transactions read the list, which is consistent with the TLA+ definition of `Txs` as `Nat`, representing the list of integers.

\* History of events visible to clients
VARIABLES history
Expand All @@ -44,16 +44,17 @@
/\ history[i].tx \in Txs
\/ /\ history[i].type \in {RwTxResponse, RoTxResponse}
/\ history[i].tx \in Txs
/\ history[i].observed \in Seq(Txs)
/\ DOMAIN history[i].observed \subseteq Views
/\ Range(history[i].observed) \subseteq Txs
/\ history[i].tx_id \in TxIDs
\/ /\ history[i].type = TxStatusReceived
/\ history[i].tx_id \in TxIDs
/\ history[i].status \in TxStatuses

\* History is append-only
\* Like HistoryTypeOK, this property should always hold
HistoryMonoProp ==
[][IsPrefix(history, history')]_history

Check notice on line 57 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "History is append-only" is consistent with the definition of HistoryMonoProp, which uses the temporal formula [][IsPrefix(history, history')]_history to ensure that history can only grow.

Check notice on line 57 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about the history being append-only is consistent with the TLA+ definition of `HistoryMonoProp` using the `IsPrefix` operator, which ensures that `history` can only grow.

\* Indexes into history for events where a committed status is received
CommittedEventIndexes ==
Expand All @@ -76,9 +77,9 @@
InvalidTxIDs ==
{history[i].tx_id: i \in InvalidEventIndexes}

\* Highest commit sequence number
CommitSeqNum ==
Max({i[2]: i \in CommittedTxIDs} \cup {0})

Check notice on line 82 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "Highest commit sequence number" is consistent with the definition of CommitSeqNum, which calculates the maximum sequence number from committed transaction IDs.

Check notice on line 82 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about the highest commit sequence number is consistent with the TLA+ definition of `CommitSeqNum` using the `Max` operator to find the maximum sequence number from `CommittedTxIDs`.

RwTxResponseEventIndexes ==
{x \in DOMAIN history : history[x].type = RwTxResponse}
Expand All @@ -90,23 +91,23 @@
RwTxResponseEventIndexes \union RoTxResponseEventIndexes


\* Note these index are the events where the transaction was responded to
RwTxResponseCommittedEventIndexes ==
{x \in DOMAIN history :
/\ history[x].type = RwTxResponse
/\ history[x].tx_id \in CommittedTxIDs}

Check notice on line 98 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about indexes being events where the transaction was responded to is consistent with the TLA+ definition of `RwTxResponseCommittedEventIndexes` which selects indexes from `history` where `RwTxResponse` events with committed transaction IDs occur.

RwTxRequestCommittedEventIndexes ==
{x \in DOMAIN history :
/\ history[x].type = RwTxRequest
/\ \E y \in RwTxResponseCommittedEventIndexes:
history[y].tx = history[x].tx}

Check notice on line 104 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comments "Note these index are the events where the transaction was responded to" are consistent with the definitions of RwTxResponseCommittedEventIndexes and RoTxResponseCommittedEventIndexes, which select indexes of history for committed response events.

\* Note these index are the events where the transaction was responded to
RoTxResponseCommittedEventIndexes ==
{x \in DOMAIN history :
/\ history[x].type = RoTxResponse
/\ history[x].tx_id \in CommittedTxIDs}

Check notice on line 110 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about indexes being events where the transaction was responded to is consistent with the TLA+ definition of `RoTxResponseCommittedEventIndexes` which selects indexes from `history` where `RoTxResponse` events with committed transaction IDs occur.

RoTxRequestCommittedEventIndexes ==
{x \in DOMAIN history :
Expand All @@ -114,11 +115,11 @@
/\ \E y \in RoTxResponseCommittedEventIndexes:
history[y].tx = history[x].tx}

TxStatusReceivedEventIndexes ==
{x \in DOMAIN history : history[x].type = TxStatusReceived}

Check notice on line 119 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The definition of TxStatusReceivedEventIndexes is consistent with the comment, as it selects indexes where the event type is TxStatusReceived.

Check failure on line 119 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about `TxStatusReceivedEventIndexes` being indexes into history for events where a committed status is received is inconsistent with the TLA+ definition which selects indexes from `history` where any `TxStatusReceived` event occurs, not just committed ones.

RoTxRequestedCommittedEventIndexes ==
{x \in DOMAIN history :
/\ history[x].type = RoTxRequest
/\ history[x].tx_id \in CommittedTxIDs}

Check failure on line 124 in tla/consistency/ExternalHistory.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about `RoTxRequestedCommittedEventIndexes` being indexes into history for events where a committed status is received is inconsistent with the TLA+ definition which selects indexes from `history` where `RoTxRequest` events with committed transaction IDs occur, not where a committed status is received.

Expand Down
12 changes: 6 additions & 6 deletions tla/consistency/ExternalHistoryInvars.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,25 +1,25 @@
---- MODULE ExternalHistoryInvars ----

EXTENDS ExternalHistory
EXTENDS ExternalHistory, Functions

\* Read-write transaction responses always follow an associated request
AllRwReceivedIsFirstSentInv ==
\A i \in DOMAIN history :
history[i].type = RwTxResponse
=> \E j \in DOMAIN history :
/\ j < i
/\ history[j].type = RwTxRequest
/\ history[j].tx = history[i].tx

Check notice on line 12 in tla/consistency/ExternalHistoryInvars.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "Read-write transaction responses always follow an associated request" is consistent with the definition of AllRwReceivedIsFirstSentInv, which ensures that for every RwTxResponse, there is a preceding RwTxRequest for the same transaction.

Check failure on line 12 in tla/consistency/ExternalHistoryInvars.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about read-write transaction responses always following an associated request is inconsistent with the TLA+ definition of `AllRwReceivedIsFirstSentInv` which allows for the possibility of a `RwTxResponse` without a preceding `RwTxRequest` with the same transaction, as it only checks for the existence of any request earlier in the history, not necessarily an associated one.

\* Read-only transaction responses always follow an associated request
\* TODO: extend this to handle the fact that separate reads might get the same transaction ID
AllRoReceivedIsFirstSentInv ==
\A i \in DOMAIN history :
history[i].type = RoTxResponse
=> \E j \in DOMAIN history :
/\ j < i
/\ history[j].type = RoTxRequest
/\ history[j].tx = history[i].tx

Check notice on line 22 in tla/consistency/ExternalHistoryInvars.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment "Read-only transaction responses always follow an associated request" is consistent with the definition of AllRoReceivedIsFirstSentInv, which ensures that for every RoTxResponse, there is a preceding RoTxRequest for the same transaction.

\* All responses must have an associated request earlier in the history (except tx status)
AllReceivedIsFirstSentInv ==
Expand Down Expand Up @@ -127,7 +127,7 @@
\A k \in RwTxResponseCommittedEventIndexes :
/\ history[k].tx = history[j].tx
/\ i < j
=> Contains(history[k].observed, history[i].tx)
=> \E idx \in DOMAIN history[k].observed : history[k].observed[idx] = history[i].tx

\* All committed read-only txs observe all previously committed txs (wrt to real-time)
\* Note that this requires committed txs to be observed from their response,
Expand Down Expand Up @@ -178,8 +178,8 @@
\A i,j \in DOMAIN history:
/\ history[i].type = RwTxResponse
/\ history[j].type = RwTxResponse
=> \/ IsPrefix(history[i].observed, history[j].observed)
\/ IsPrefix(history[j].observed, history[i].observed)
=> \/ IsRestriction(history[i].observed, history[j].observed)
\/ IsRestriction(history[j].observed, history[i].observed)

\* A weaker version of RwSerializableInv which only considers committed requests
\* If any committed request observes A before B then every committed request must observe A before B
Expand All @@ -195,8 +195,8 @@
/\ history[l].type = TxStatusReceived
/\ history[l].status = CommittedStatus
/\ history[j].tx_id = history[l].tx_id
=> \/ IsPrefix(history[i].observed, history[j].observed)
\/ IsPrefix(history[j].observed, history[i].observed)
=> \/ IsRestriction(history[i].observed, history[j].observed)
\/ IsRestriction(history[j].observed, history[i].observed)

\* Linearizability for read-write transactions
\* Or equivalently, strict serializability as we are modeling a single object system
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNode.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllReceivedIsFirstSentInv
AllCommittedObservedInv
OnlyObserveSentRequestsInv
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNodeCommitReachability.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
MultiCommittedTxDebugInv

CHECK_DEADLOCK
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNodeInvalidReachability.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
SomeInvalidTxDebugInv

CHECK_DEADLOCK
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNodeReads.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllReceivedIsFirstSentInv
AllCommittedObservedInv
OnlyObserveSentRequestsInv
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNodeReadsAlt.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllReceivedIsFirstSentInv
AllCommittedObservedInv
OnlyObserveSentRequestsInv
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCMultiNodeReadsNotLinearizable.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllCommittedObservedRoInv

CHECK_DEADLOCK
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCSingleNode.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllReceivedIsFirstSentInv
AllCommittedObservedInv
OnlyObserveSentRequestsInv
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCSingleNodeCommitReachability.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
SomeCommittedTxDebugInv

CHECK_DEADLOCK
Expand Down
1 change: 1 addition & 0 deletions tla/consistency/MCSingleNodeReads.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ CONSTANTS
InvalidStatus = InvalidStatus

INVARIANTS
TypeOK
AllReceivedIsFirstSentInv
AllCommittedObservedInv
OnlyObserveSentRequestsInv
Expand Down
12 changes: 5 additions & 7 deletions tla/consistency/SingleNode.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,9 @@

EXTENDS ExternalHistoryInvars, TLC


\* Abstract ledgers that contains only client transactions (no signatures)
\* Indexed by view, each ledger is the ledger associated with leader of that view
\* In practice, the ledger of every CCF node is one of these or a prefix for one of these

Check failure on line 11 in tla/consistency/SingleNode.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about abstract ledgers containing only client transactions is inconsistent with the TLA+ definition of `ledgerBranches` which does not explicitly restrict the ledger to client transactions, as there is no check for the type of transaction within the ledger entries.
\* This could be switched to a tree which can represent forks more elegantly
VARIABLES ledgerBranches

Expand All @@ -21,9 +20,9 @@
/\ ledgerBranches[view][seqnum].view \in Views
\* /\ ledgerBranches[view][seqnum].tx \in Txs

\* In this abstract version of CCF's consensus layer, each ledger is append-only
LedgersMonoProp ==
[][\A view \in DOMAIN ledgerBranches: IsPrefix(ledgerBranches[view], ledgerBranches'[view])]_ledgerBranches

Check failure on line 25 in tla/consistency/SingleNode.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about each ledger being append-only is inconsistent with the TLA+ definition of `LedgersMonoProp` which uses the `IsPrefix` operator that allows for the ledger to remain unchanged, not strictly append-only as the comment suggests.

vars == << history, ledgerBranches >>

Expand All @@ -41,14 +40,14 @@
NextRequestId ==
IF IndexOfLastRequested = 0 THEN 0 ELSE history[IndexOfLastRequested].tx+1

\* Submit new read-write transaction
\* This could be extended to add a notion of session and then check for session consistency
RwTxRequestAction ==
/\ history' = Append(
history,
[type |-> RwTxRequest, tx |-> NextRequestId]
)
/\ UNCHANGED ledgerBranches

Check failure on line 50 in tla/consistency/SingleNode.tla

View workflow job for this annotation

GitHub Actions / tlai-linter 

The comment about submitting new read-write transactions does not mention any constraints on the transactions, but the TLA+ definition of `RwTxRequestAction` includes a constraint on the next request ID, which is inconsistent with the comment's lack of mention of such a constraint.

\* Execute a read-write transaction
RwTxExecuteAction ==
Expand All @@ -63,11 +62,11 @@
\* that it can be picked up by the current leader or any former leader
/\ \E view \in DOMAIN ledgerBranches:
ledgerBranches' = [ledgerBranches EXCEPT ![view] =
Append(@,[view |-> view, tx |-> history[i].tx])]
@ @@ (Max(DOMAIN ledgerBranches[view] \cup {0})+1) :> [view |-> view, tx |-> history[i].tx]]
Copy link
Member

@eddyashton eddyashton Apr 22, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have this pattern in multiple places, can we pull it out and name it?

SparseLen(s) == Max(DOMAIN s \cup {0})

SparseAppend(s, e) == s @@ (SparseLen(s) + 1 :> e)

For the others that don't have multiple callers its less clear-cut, but maybe still more readable to introduce SparseSelectSeq and SparseSubSeq?

/\ UNCHANGED history

LedgerBranchTxOnly(branch) ==
LET SubBranch == SelectSeq(branch, LAMBDA e : "tx" \in DOMAIN e)
LET SubBranch == [ i \in {j \in DOMAIN branch : "tx" \in DOMAIN branch[j] } |-> branch[i] ]
IN [i \in DOMAIN SubBranch |-> SubBranch[i].tx]

\* Response to a read-write transaction
Expand All @@ -87,7 +86,7 @@
history,[
type |-> RwTxResponse,
tx |-> history[i].tx,
observed |-> LedgerBranchTxOnly(SubSeq(ledgerBranches[view],1,seqnum)),
observed |-> LedgerBranchTxOnly([j \in DOMAIN ledgerBranches[view] \cap 1..seqnum |-> ledgerBranches[view][j]]),
tx_id |-> <<ledgerBranches[view][seqnum].view, seqnum>>] )
/\ UNCHANGED ledgerBranches

Expand All @@ -96,7 +95,7 @@
StatusCommittedResponseAction ==
/\ \E i \in DOMAIN history :
/\ history[i].type = RwTxResponse
/\ Len(ledgerBranches[Len(ledgerBranches)]) >= history[i].tx_id[2]
/\ Max(DOMAIN ledgerBranches[Len(ledgerBranches)]) >= history[i].tx_id[2]
/\ ledgerBranches[Len(ledgerBranches)][history[i].tx_id[2]].view = history[i].tx_id[1]
\* Reply
/\ history' = Append(
Expand All @@ -110,8 +109,7 @@
\* Append a transaction to the ledger which does not impact the state we are considering
AppendOtherTxnAction ==
/\ \E view \in DOMAIN ledgerBranches:
ledgerBranches' = [ledgerBranches EXCEPT ![view] =
Append(@,[view |-> view])]
ledgerBranches' = [ledgerBranches EXCEPT ![view] = @ @@ (Max(DOMAIN ledgerBranches[view] \cup {0})+1) :> [view |-> view] ]
/\ UNCHANGED history

\* A CCF service with a single node will never have a view change
Expand Down
4 changes: 2 additions & 2 deletions tla/consistency/SingleNodeReads.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,13 +23,13 @@ RoTxResponseAction ==
/\ history[j].type = RoTxResponse
/\ history[j].tx = history[i].tx} = {}
/\ \E view \in DOMAIN ledgerBranches:
/\ Len(ledgerBranches[view]) > 0
/\ ledgerBranches[view] # <<>>
/\ history' = Append(
history,[
type |-> RoTxResponse,
tx |-> history[i].tx,
observed |-> LedgerBranchTxOnly(ledgerBranches[view]),
tx_id |-> <<ledgerBranches[view][Len(ledgerBranches[view])].view, Len(ledgerBranches[view])>>] )
tx_id |-> <<ledgerBranches[view][Max(DOMAIN ledgerBranches[view])].view, Max(DOMAIN ledgerBranches[view])>>] )
/\ UNCHANGED ledgerBranches

NextSingleNodeReadsAction ==
Expand Down
Loading