diff --git a/.gitignore b/.gitignore index 61ead866..2247a5f8 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,4 @@ /vendor + +# TLC Model Checker files +formal-models/*/*.toolbox/ diff --git a/README.md b/README.md index 902ae367..cf4411a5 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,8 @@ [![Report](https://goreportcard.com/badge/github.com/nspcc-dev/dbft)](https://goreportcard.com/report/github.com/nspcc-dev/dbft) # DBFT -This repo contains Go implementation of the dBFT 2.0 consensus algorithm. +This repo contains Go implementation of the dBFT 2.0 consensus algorithm and its models +written in [TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) language. ## Design and structure 1. All control flow is done in main package. Most of the code which communicates with external @@ -23,6 +24,9 @@ own payloads in order to sign and verify messages. 5. `timer` contains default time provider. It should make it easier to write tests concerning dBFT's time depending behaviour. 6. `simulation` contains an example of dBFT's usage with 6-node consensus. +7. `formal-models` contains the set of dBFT's models written in [TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) + language and instructions on how to run and check them. Please, refer to the [README](./formal-models/README.md) + for more details. ## Usage A client of the library must implement its own event loop. diff --git a/formal-models/.github/dbft.png b/formal-models/.github/dbft.png new file mode 100644 index 00000000..5d9f94e0 Binary files /dev/null and b/formal-models/.github/dbft.png differ diff --git a/formal-models/README.md b/formal-models/README.md new file mode 100644 index 00000000..9c700e0d --- /dev/null +++ b/formal-models/README.md @@ -0,0 +1,141 @@ +## dBFT formal models + +This section contains a set of dBFT's formal specifications written in +[TLA⁺](https://lamport.azurewebsites.net/tla/tla.html) language. The models +describe the core algorithm logic represented in a high-level way and can be used +to illustrate some basic dBFT concepts and to validate the algorithm in terms of +liveness and fairness. It should be noted that presented models do not precisely +follow the dBFT implementation presented in the repository and may omit some +implementation details in favor of the specification simplicity and the +fundamental philosophy of the TLA⁺. However, the presented models directly +reflect some liveness problems dBFT 2.0 has; the models can and are aimed to be +used for the dBFT 2.0 liveness evaluation and further algorithm improvements. + +Any contributions, questions and discussions on the presented models are highly +appreciated. + +## Models + +### Basic dBFT 2.0 model + +This specification is a basis that was taken for the further algorithm +investigation. We recommend to begin acquaintance with the dBFT models from this +one. + +The specification describes the process of a single block acceptance: the set of +resource managers `RM` (which is effectively a set of consensus nodes) +communicating via the shared consensus message pool `msgs` and taking the +decision in a few consensus rounds (views). Each consensus node has its own state +at each step of the behaviour. Consensus node may send a consensus message by +adding it to the `msgs` pool. To perform the transition between states the +consensus node must send a consensus message or there must be a particular set of +consensus messages in the shared message pool required for a particular +transition. + +Here's the scheme of transitions between consensus node states: + +![Basic dBFT model transitions scheme](./.github/dbft.png) + +The specification also describes two kinds of malicious nodes behaviour that can +be combined, i.e. enabled or disabled independently for each particular node: + +1. "Dead" nodes. "Dead" node is completely excluded from the consensus process + and not able to send the consensus messages and to perform state transitions. + The node may become "dead" at any step in the middle of the consensus process. + Once the node becomes "dead" there's no way for it to rejoin the consensus + process. +2. "Faulty" nodes. "Faulty" node is allowed to send consensus messages of *any* + type at *any* step and to change its view without regarding the dBFT view + changing rules. The node may become "faulty" at any step in the middle of the + consensus process. Once the node becomes "faulty" there's no way for it to + become "good" again. + +The specification contains several invariants and liveness properties that must +be checked by the TLC Model Checker. These formulas mostly describe two basic +concepts that dBFT algorithm expected to guarantee: + +1. No fork must happen. There must be no situation such that two different + blocks are accepted at two different consensus rounds (views). +2. The block must always be accepted. There must be no situation such that nodes + are stuck in the middle of consensus process and can't take any further steps. + +The specification is written and working under several assumptions: + +1. All consensus messages are valid. In real life it is guaranteed by verifiable + message signatures. In case if malicious or corrupted message is received it + won't be handled by the node. +2. The exact timeouts (e.g. t/o on waiting a particular consensus message, etc.) + are not included into the model. However, the model covers timeouts in + general, i.e. the timeout is just the possibility to perform a particular + state transition. +3. All consensus messages must eventually be delivered to all nodes, but the + exact order of delivering isn't guaranteed. +4. The maximum number of consensus rounds (views) is restricted. This constraint + was introduced to reduce the number of possible model states to be checked. + The threshold may be specified via model configuration, and it is highly + recommended to keep this setting less or equal to the number of consensus + nodes. + +Here you can find the specification file and the TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbft/dbft.tla) +* [TLC Model Checker configuration](./dbft/dbft___AllGoodModel.launch) + +### Extended dBFT 2.0 model + +This is an experimental dBFT 2.0 specification that extends the +[basic model](#basic-dbft-20-model) in the following way: besides the shared pool +of consensus messages `msgs` each consensus node has its own local pool of +received and handled messages. Decisions on transmission between the node states +are taken by the node based on the state of the local message pool. This approach +allows to create more accurate low-leveled model which is extremely close to the +dBFT implementation presented in this repository. At the same time such approach +*significantly* increases the number of considered model states which leads to +abnormally long TLC Model Checker runs. Thus, we do not recommend to use this +model in development and place it here as an example of alternative (and more +detailed) dBFT specification. These two models are expected to be equivalent in +terms of the liveness locks that can be discovered by both of them, and, speaking +the TLA⁺ language, the Extended dBFT specification implements the +[basic one](#basic-dbft-20-model) (which can be proven and written in TLA⁺, but +stays out of the task scope). + +Except for this remark and a couple of minor differences all the +[basic model](#basic-dbft-20-model) description, constraints and assumptions are +valid for the Extended specification as far. Thus, we highly recommend to +consider the [basic model](#basic-dbft-20-model) before going to the Extended +one. + +Here you can find the specification file and the TLC Model Checker launch +configuration: + +* [TLA⁺ specification](./dbftMultipool/dbftMultipool.tla) +* [TLC Model Checker configuration](./dbftMultipool/dbftMultipool___AllGoodModel.launch) + +## How to run/check the TLA⁺ specification + +### Prerequirements + +1. Download and install the TLA⁺ Toolbox following the + [official guide](http://lamport.azurewebsites.net/tla/toolbox.html). +2. Read the brief introduction to the TLA⁺ language and TLC Model Checker at the + [official site](http://lamport.azurewebsites.net/tla/high-level-view.html). +3. Download and take a look at the + [TLA⁺ cheat sheet](https://lamport.azurewebsites.net/tla/summary-standalone.pdf). +4. For a proficient learning watch the + [TLA⁺ Video Course](https://lamport.azurewebsites.net/video/videos.html) and + read the [Specifying Systems book](http://lamport.azurewebsites.net/tla/book.html?back-link=tools.html#documentation). + +### Running the TLC model checker + +1. Clone the [repository](https://github.com/nspcc-dev/dbft.git). +2. Open the TLA⁺ Toolbox, open new specification and provide path to the desired + `*.tla` file that contains the specification description. +3. Create the model named `AllGoodModel` in the TLA⁺ Toolbox. +4. Copy the corresponding `*___AllGoodModel.launch` file to the `*.toolbox` + folder. +5. Open the `Model Overview` window in the TLA⁺ Toolbox and check that behaviour + specification, declared constants, invariants and properties of the model are + filled in with some values. +6. Press `Run TLC on the model` bottom to start the model checking process and + explore the progress in the `Model Checkng Results` window. \ No newline at end of file diff --git a/formal-models/dbft/dbft.tla b/formal-models/dbft/dbft.tla new file mode 100644 index 00000000..e291ebcf --- /dev/null +++ b/formal-models/dbft/dbft.tla @@ -0,0 +1,379 @@ +-------------------------------- MODULE dbft -------------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + +\* RMStates is a set of records where each record holds the node state and +\* the node current view. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "cv", "blockAccepted", "bad", "dead"}, + view : Nat + ] + +\* Messages is a set of records where each record holds the message type, +\* the message sender and sender's view by the moment when message was sent. +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView"}, rm : RM, view : Nat] + +\* -------------- Useful operators -------------- + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == rmState[r].view % N = r + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* CountCommitted returns the number of nodes that have sent the Commit message +\* in the current round (as the node r sees it). +CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit" /\ msg.view = rmState[r].view}) /= 0}) + +\* MoreThanFNodesCommitted returns whether more than F nodes have been committed +\* in the current round (as the node r sees it). +MoreThanFNodesCommitted(r) == CountCommitted(r) > F + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in msgs + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]] + /\ msgs = {} + +\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from +\* the primary node of the current round (view) and broadcasting PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMSendPrepareResponse(r) == + /\ \/ rmState[r].type = "initialized" + \* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage + \* as it is done in the code-level dBFT implementation by checking the NotAcceptingPayloadsDueToViewChanging + \* condition (see + \* https://github.com/nspcc-dev/dbft/blob/31c1bbdc74f2faa32ec9025062e3a4e2ccfd4214/dbft.go#L419 + \* and + \* https://github.com/neo-project/neo-modules/blob/d00d90b9c27b3d0c3c57e9ca1f560a09975df241/src/DBFTPlugin/Consensus/ConsensusService.OnMessage.cs#L79). + \* However, we can't easily count the number of "lost" nodes in this specification to match precisely + \* the implementation. Moreover, we don't need it to be counted as the RMSendPrepareResponse enabling + \* condition specifies only the thing that may happen given some particular set of enabling conditions. + \* Thus, we've extended the NotAcceptingPayloadsDueToViewChanging condition to consider only MoreThanFNodesCommitted. + \* It should be noted that the logic of MoreThanFNodesCommittedOrLost can't be reliable in detecting lost nodes + \* (even with neo-project/neo#2057), because real nodes can go down at any time. + \/ /\ rmState[r].type = "cv" + /\ MoreThanFNodesCommitted(r) + /\ \neg IsPrimary(r) + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"] + /\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMSendCommit describes node r sending Commit if there's enough PrepareResponse +\* messages. +RMSendCommit(r) == + /\ \/ rmState[r].type = "prepareSent" + \* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage, + \* see the related comment inside the RMSendPrepareResponse definition. + \/ /\ rmState[r].type = "cv" + /\ MoreThanFNodesCommitted(r) + /\ Cardinality({ + msg \in msgs : /\ (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest") + /\ msg.view = rmState[r].view + }) >= M + /\ PrepareRequestSentOrReceived(r) + /\ rmState' = [rmState EXCEPT ![r].type = "commitSent"] + /\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view]} + /\ UNCHANGED <<>> + +\* RMAcceptBlock describes node r collecting enough Commit messages and accepting +\* the block. +RMAcceptBlock(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ PrepareRequestSentOrReceived(r) + /\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"] + /\ UNCHANGED <> + +\* RMSendChangeView describes node r sending ChangeView message on timeout. +RMSendChangeView(r) == + /\ \/ rmState[r].type = "initialized" + \/ rmState[r].type = "prepareSent" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ rmState' = [rmState EXCEPT ![r].type = "cv"] + /\ msgs' = msgs \cup {[type |-> "ChangeView", rm |-> r, view |-> rmState[r].view]} + +\* RMReceiveChangeView describes node r receiving enough ChangeView messages for +\* view changing. +RMReceiveChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ rmState[r].type /= "commitSent" + /\ Cardinality({ + rm \in RM : Cardinality({ + msg \in msgs : /\ msg.type = "ChangeView" + /\ msg.rm = rm + /\ GetNewView(msg.view) >= GetNewView(rmState[r].view) + }) /= 0 + }) >= M + /\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV describes sending CV message by the faulty node r. +RMFaultySendCV(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* has the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M + /\ UNCHANGED <> + +\* Next is the next-state action describing the transition from the current state +\* to the next state of the behaviour. +Next == + \/ Terminating + \/ \E r \in RM: + RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) + \/ RMAcceptBlock(r) \/ RMSendChangeView(r) \/ RMReceiveChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == TerminationRequirement + +\* -------------- ModelConstraints -------------- + +\* MaxViewConstraint is a state predicate restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. This formulae must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.view <= MaxView + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + +\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in +\* the two different views, i.e. dBFT must not allow forks. +InvTwoBlocksAccepted == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ rmState[r1].view = rmState[r2].view + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount) + +============================================================================= +\* Modification History +\* Last modified Fri Feb 17 15:47:41 MSK 2023 by anna +\* Last modified Sat Jan 21 01:26:16 MSK 2023 by rik +\* Created Thu Dec 15 16:06:17 MSK 2022 by anna diff --git a/formal-models/dbft/dbft___AllGoodModel.launch b/formal-models/dbft/dbft___AllGoodModel.launch new file mode 100644 index 00000000..eb14599a --- /dev/null +++ b/formal-models/dbft/dbft___AllGoodModel.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/formal-models/dbftMultipool/dbftMultipool.tla b/formal-models/dbftMultipool/dbftMultipool.tla new file mode 100644 index 00000000..3eb395ec --- /dev/null +++ b/formal-models/dbftMultipool/dbftMultipool.tla @@ -0,0 +1,466 @@ +---------------------------- MODULE dbftMultipool ---------------------------- + +EXTENDS + Integers, + FiniteSets + +CONSTANTS + \* RM is the set of consensus node indexes starting from 0. + \* Example: {0, 1, 2, 3} + RM, + + \* RMFault is a set of consensus node indexes that are allowed to become + \* FAULT in the middle of every considered behavior and to send any + \* consensus message afterwards. RMFault must be a subset of RM. An empty + \* set means that all nodes are good in every possible behaviour. + \* Examples: {0} + \* {1, 3} + \* {} + RMFault, + + \* RMDead is a set of consensus node indexes that are allowed to die in the + \* middle of every behaviour and do not send any message afterwards. RMDead + \* must be a subset of RM. An empty set means that all nodes are alive and + \* responding in in every possible behaviour. RMDead may intersect the + \* RMFault set which means that node which is in both RMDead and RMFault + \* may become FAULT and send any message starting from some step of the + \* particular behaviour and may also die in the same behaviour which will + \* prevent it from sending any message. + \* Examples: {0} + \* {3, 2} + \* {} + RMDead, + + \* MaxView is the maximum allowed view to be considered (starting from 0, + \* including the MaxView itself). This constraint was introduced to reduce + \* the number of possible model states to be checked. It is recommended to + \* keep this setting not too high (< N is highly recommended). + \* Example: 2 + MaxView, + + \* MaxUndeliveredMessages is the maximum number of messages in the common + \* messages pool (msgs) that were not received and handled by all consensus + \* nodes. It must not be too small (>= 3) in order to allow model taking + \* at least any steps. At the same time it must not be too high (<= 6 is + \* recommended) in order to avoid states graph size explosion. + MaxUndeliveredMessages + +VARIABLES + \* rmState is a set of consensus node states. It is represented by the + \* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is + \* the state of the r-th consensus node at the current step. + rmState, + + \* msgs is the shared pool of messages sent to the network by consensus nodes. + \* It is represented by a subset of Messages set. + msgs + +\* vars is a tuple of all variables used in the specification. It is needed to +\* simplify fairness conditions definition. +vars == <> + +\* N is the number of validators. +N == Cardinality(RM) + +\* F is the number of validators that are allowed to be malicious. +F == (N - 1) \div 3 + +\* M is the number of validators that must function correctly. +M == N - F + +\* These assumptions are checked by the TLC model checker once at the start of +\* the model checking process. All the input data (declared constants) specified +\* in the "Model Overview" section must satisfy these constraints. +ASSUME + /\ RM \subseteq Nat + /\ N >= 4 + /\ 0 \in RM + /\ RMFault \subseteq RM + /\ RMDead \subseteq RM + /\ Cardinality(RMFault) <= F + /\ Cardinality(RMDead) <= F + /\ Cardinality(RMFault \cup RMDead) <= F + /\ MaxView \in Nat + /\ MaxView <= 2 + /\ MaxUndeliveredMessages \in Nat + /\ MaxUndeliveredMessages >= 3 \* First value when block can be accepted in some behaviours. + +\* Messages is a set of records where each record holds the message type, +\* the message sender and sender's view by the moment when message was sent. +Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "ChangeView"}, rm : RM, view : Nat] + +\* RMStates is a set of records where each record holds the node state, the node current view +\* and the pool of messages the nde has been sent or received and handled. +RMStates == [ + type: {"initialized", "prepareSent", "commitSent", "blockAccepted", "bad", "dead"}, + view : Nat, + pool : SUBSET Messages + ] + +\* -------------- Useful operators -------------- + +\* IsPrimary is an operator defining whether provided node r is primary +\* for the current round from the r's point of view. It is a mapping +\* from RM to the set of {TRUE, FALSE}. +IsPrimary(r) == rmState[r].view % N = r + +\* GetPrimary is an operator defining mapping from round index to the RM that +\* is primary in this round. +GetPrimary(view) == CHOOSE r \in RM : view % N = r + +\* GetNewView returns new view number based on the previous node view value. +\* Current specifications only allows to increment view. +GetNewView(oldView) == oldView + 1 + +\* IsViewChanging denotes whether node r have sent ChangeView message for the +\* current (or later) round. +IsViewChanging(r) == Cardinality({msg \in rmState[r].pool : msg.type = "ChangeView" /\ msg.view >= rmState[r].view /\ msg.rm = r}) /= 0 + +\* CountCommitted returns the number of nodes that have sent the Commit message +\* in the current round (as the node r sees it). +CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in rmState[r].pool : msg.rm = rm /\ msg.type = "Commit"}) /= 0}) + +\* CountFailed returns the number of nodes that haven't sent any message since +\* the last round (as the node r sees it from the point of its pool). +CountFailed(r) == Cardinality({rm \in RM : Cardinality({msg \in rmState[r].pool : msg.rm = rm /\ msg.view >= rmState[r].view}) = 0 }) + +\* MoreThanFNodesCommittedOrLost denotes whether more than F nodes committed or +\* failed to communicate in the current round. +MoreThanFNodesCommittedOrLost(r) == CountCommitted(r) + CountFailed(r) > F + +\* NotAcceptingPayloadsDueToViewChanging returns whether the node doesn't accept +\* payloads in the current step. +NotAcceptingPayloadsDueToViewChanging(r) == + /\ IsViewChanging(r) + /\ \neg MoreThanFNodesCommittedOrLost(r) + +\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest +\* message received from the current round's speaker (as the node r sees it). +PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in rmState[r].pool + +\* CommitSent returns whether the node has its commit sent for the current block. +CommitSent(r) == Cardinality({msg \in rmState[r].pool : msg.rm = r /\ msg.type = "Commit"}) > 0 + +\* -------------- Safety temporal formula -------------- + +\* Init is the initial predicate initializing values at the start of every +\* behaviour. +Init == + /\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 1, pool |-> {}]] + /\ msgs = {} + +\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest. +RMSendPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ IF Cardinality({m \in rmState[r].pool : m.type = "PrepareResponse" /\ m.view = rmState[r].view}) < M - 1 \* -1 is for the current PrepareRequest. + THEN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].pool = rmState[r].pool \cup {pReq}] + /\ msgs' = msgs \cup {pReq} + ELSE /\ msgs' = msgs \cup {pReq, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {pReq, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {pReq, commit}] + /\ UNCHANGED <<>> + +\* RMSendChangeView describes node r sending ChangeView message on timeout. +RMSendChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \/ (IsPrimary(r) /\ PrepareRequestSentOrReceived(r)) + \/ (\neg IsPrimary(r) /\ \neg CommitSent(r)) + /\ LET msg == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ msg \notin msgs + /\ msgs' = msgs \cup {msg} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ GetNewView(m.view) >= GetNewView(msg.view)}) >= M-1 \* -1 is for the currently sent CV + THEN rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(msg.view), ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + +\* OnTimeout describes two actions the node can take on timeout for waiting any event. +OnTimeout(r) == + \/ RMSendPrepareRequest(r) + \/ RMSendChangeView(r) + +\* RMOnPrepareRequest describes non-primary node r receiving PrepareRequest from the +\* primary node of the current round (view) and broadcasts PrepareResponse. +\* This step assumes that PrepareRequest always contains valid transactions and +\* signatures. +RMOnPrepareRequest(r) == + /\ rmState[r].type = "initialized" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "PrepareRequest" + /\ msg.view = rmState[r].view + /\ \neg IsPrimary(r) + /\ \neg NotAcceptingPayloadsDueToViewChanging(r) \* dbft.go -L296, in C# node, but not in ours + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN IF Cardinality({m \in rmState[r].pool : m.type = "PrepareResponse" /\ m.view = rmState[r].view}) < M - 1 - 1 \* -1 is for reveived PrepareRequest; -1 is for current PrepareResponse + THEN /\ rmState' = [rmState EXCEPT ![r].type = "prepareSent", ![r].pool = rmState[r].pool \cup {msg, pResp}] + /\ msgs' = msgs \cup {pResp} + ELSE /\ msgs' = msgs \cup {msg, pResp, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {msg, pResp, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg, pResp, commit}] + /\ UNCHANGED <<>> + +\* RMOnPrepareResponse describes node r accepting PrepareResponse message and handling it. +\* If there's enough PrepareResponses collected it will send the Commit; in case if there's +\* enough Commits it will accept the block. +RMOnPrepareResponse(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "PrepareResponse" + /\ msg.view = rmState[r].view + /\ \neg NotAcceptingPayloadsDueToViewChanging(r) + /\ IF \/ Cardinality({m \in rmState[r].pool : (m.type = "PrepareRequest" \/ m.type = "PrepareResponse") /\ m.view = rmState[r].view}) < M - 1 \* -1 is for the currently received PrepareResponse. + \/ CommitSent(r) + \/ \neg PrepareRequestSentOrReceived(r) + THEN /\ rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + ELSE LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ msgs' = msgs \cup {msg, commit} + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the current Commit + THEN rmState' = [rmState EXCEPT ![r].type = "commitSent", ![r].pool = rmState[r].pool \cup {msg, commit}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg, commit}] + +\* RMOnCommit describes node r accepting Commit message and (in case if there's enough Commits) +\* accepting the block. +RMOnCommit(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "Commit" + /\ msg.view = rmState[r].view + /\ IF Cardinality({m \in rmState[r].pool : m.type = "Commit" /\ m.view = rmState[r].view}) < M-1 \* -1 is for the currently accepting commit + THEN rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].type = "blockAccepted", ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + +\* RMOnChangeView describes node r receiving ChangeView message and (in case if enough ChangeViews +\* is collected) changing its view. +RMOnChangeView(r) == + /\ rmState[r].type /= "bad" + /\ rmState[r].type /= "dead" + /\ rmState[r].type /= "blockAccepted" + /\ \E msg \in msgs \ rmState[r].pool: + /\ msg.rm /= r + /\ msg.type = "ChangeView" + /\ msg.view = rmState[r].view + /\ \neg CommitSent(r) + /\ Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ m.rm = msg.rm /\ m.view > msg.view}) = 0 + /\ IF Cardinality({m \in rmState[r].pool : m.type = "ChangeView" /\ GetNewView(m.view) >= GetNewView(msg.view)}) < M-1 \* -1 is for the currently accepting CV + THEN rmState' = [rmState EXCEPT ![r].pool = rmState[r].pool \cup {msg}] + ELSE rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(msg.view), ![r].pool = rmState[r].pool \cup {msg}] + /\ UNCHANGED <> + +\* RMBeBad describes the faulty node r that will send any kind of consensus message starting +\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set. +RMBeBad(r) == + /\ r \in RMFault + /\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "bad"] + /\ UNCHANGED <> + +\* RMFaultySendCV describes sending CV message by the faulty node r. +RMFaultySendCV(r) == + /\ rmState[r].type = "bad" + /\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view] + IN /\ cv \notin msgs + /\ msgs' = msgs \cup {cv} + /\ UNCHANGED <> + +\* RMFaultyDoCV describes view changing by the faulty node r. +RMFaultyDoCV(r) == + /\ rmState[r].type = "bad" + /\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)] + /\ UNCHANGED <> + +\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r. +RMFaultySendPReq(r) == + /\ rmState[r].type = "bad" + /\ IsPrimary(r) + /\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view] + IN /\ pReq \notin msgs + /\ msgs' = msgs \cup {pReq} + /\ UNCHANGED <> + +\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r. +RMFaultySendPResp(r) == + /\ rmState[r].type = "bad" + /\ \neg IsPrimary(r) + /\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view] + IN /\ pResp \notin msgs + /\ msgs' = msgs \cup {pResp} + /\ UNCHANGED <> + +\* RMFaultySendCommit describes sending Commit message by the faulty node r. +RMFaultySendCommit(r) == + /\ rmState[r].type = "bad" + /\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view] + IN /\ commit \notin msgs + /\ msgs' = msgs \cup {commit} + /\ UNCHANGED <> + +\* RMDie describes node r that was removed from the network at the particular step +\* of the behaviour. After this node r can't change its state and accept/send messages. +RMDie(r) == + /\ r \in RMDead + /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F + /\ rmState' = [rmState EXCEPT ![r].type = "dead"] + /\ UNCHANGED <> + +\* Terminating is an action that allows infinite stuttering to prevent deadlock on +\* behaviour termination. We consider termination to be valid if at least M nodes +\* has the block being accepted. +Terminating == + /\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >=1 + /\ UNCHANGED <> + +\* Next is the next-state action describing the transition from the current state +\* to the next state of the behaviour. +Next == + \/ Terminating + \/ \E r \in RM : + \/ OnTimeout(r) + \/ RMOnPrepareRequest(r) \/ RMOnPrepareResponse(r) \/ RMOnCommit(r) \/ RMOnChangeView(r) + \/ RMDie(r) \/ RMBeBad(r) + \/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r) + +\* Safety is a temporal formula that describes the whole set of allowed +\* behaviours. It specifies only what the system MAY do (i.e. the set of +\* possible allowed behaviours for the system). It asserts only what may +\* happen; any behaviour that violates it does so at some point and +\* nothing past that point makes difference. +\* +\* E.g. this safety formula (applied standalone) allows the behaviour to end +\* with an infinite set of stuttering steps (those steps that DO NOT change +\* neither msgs nor rmState) and never reach the state where at least one +\* node is committed or accepted the block. +\* +\* To forbid such behaviours we must specify what the system MUST +\* do. It will be specified below with the help of fairness conditions in +\* the Fairness formula. +Safety == Init /\ [][Next]_vars + +\* -------------- Fairness temporal formula -------------- + +\* Fairness is a temporal assumptions under which the model is working. +\* Usually it specifies different kind of assumptions for each/some +\* subactions of the Next's state action, but the only think that bothers +\* us is preventing infinite stuttering at those steps where some of Next's +\* subactions are enabled. Thus, the only thing that we require from the +\* system is to keep take the steps until it's impossible to take them. +\* That's exactly how the weak fairness condition works: if some action +\* remains continuously enabled, it must eventually happen. +Fairness == WF_vars(Next) + +\* -------------- Specification -------------- + +\* The complete specification of the protocol written as a temporal formula. +Spec == Safety /\ Fairness + +\* -------------- Liveness temporal formula -------------- + +\* For every possible behaviour it's true that there's at least one PrepareRequest +\* message from the speaker, there's at lest one PrepareResponse message and at +\* least one Commit message. +PrepareRequestSentRequirement == <>(\E msg \in msgs : msg.type = "PrepareRequest") +PrepareResponseSentRequirement == <>(\E msg \in msgs : msg.type = "PrepareResponse") +CommitSentRequirement == <>(\E msg \in msgs : msg.type = "Commit") + +\* For every possible behaviour it's true that eventually (i.e. at least once +\* through the behaviour) block will be accepted. It is something that dBFT +\* must guarantee (an in practice this condition is violated). +TerminationRequirement == <>(Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M) + +\* A liveness temporal formula asserts only what must happen (i.e. specifies +\* what the system MUST do). Any behaviour can NOT violate it at ANY point; +\* there's always the rest of the behaviour that can always make the liveness +\* formula true; if there's no such behaviour than the liveness formula is +\* violated. The liveness formula is supposed to be checked as a property +\* by the TLC model checker. +Liveness == /\ PrepareRequestSentRequirement + /\ PrepareResponseSentRequirement + /\ CommitSentRequirement + /\ TerminationRequirement + +\* -------------- Model constraints -------------- + +\* Model constraints are a set of state predicates restricting the number of possible +\* behaviour states. It is needed to reduce model checking time and prevent +\* the model graph size explosion. These formulaes must be specified at the +\* "State constraint" section of the "Additional Spec Options" section inside +\* the model overview. + +\* MaxViewConstraint is a state predicate restricting the maximum view of messages +\* and consensus nodes state. +MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView + /\ \A msg \in msgs : msg.view <= MaxView + +\* MaxUndeliveredMessageConstraint is a state predicate restricting the maximum +\* number of messages undelivered to any of the consensus nodes. +MaxUndeliveredMessageConstraint == Cardinality({msg \in msgs : \E rm \in RM : msg \notin rmState[rm].pool}) <= MaxUndeliveredMessages + +\* ModelConstraint is overall model constraint rule. +ModelConstraint == MaxViewConstraint /\ MaxUndeliveredMessageConstraint + +\* -------------- Invariants of the specification -------------- + +\* Model invariant is a state predicate (statement) that must be true for +\* every step of every reachable behaviour. Model invariant is supposed to +\* be checked as an Invariant by the TLC Model Checker. + +\* TypeOK is a type-correctness invariant. It states that all elements of +\* specification variables must have the proper type throughout the behaviour. +TypeOK == + /\ rmState \in [RM -> RMStates] + /\ msgs \subseteq Messages + +\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in +\* the two different views, i.e. dBFT must not allow forks. +InvTwoBlocksAccepted == \A r1 \in RM: + \A r2 \in RM \ {r1}: + \/ rmState[r1].type /= "blockAccepted" + \/ rmState[r2].type /= "blockAccepted" + \/ rmState[r1].view = rmState[r2].view + +\* InvDeadlock is a deadlock invariant, it states that the following situation expected +\* never to happen: one node is committed in a single view, two others are committed in +\* a larger view, and the last one has its view changing. +InvDeadlock == \A r1 \in RM : + \A r2 \in RM \ {r1} : + \A r3 \in RM \ {r1, r2} : + \A r4 \in RM \ {r1, r2, r3} : + \/ rmState[r1].type /= "commitSent" + \/ rmState[r2].type /= "commitSent" + \/ rmState[r3].type /= "commitSent" + \/ \neg IsViewChanging(r4) + \/ rmState[r1].view >= rmState[r2].view + \/ rmState[r2].view /= rmState[r3].view + \/ rmState[r3].view /= rmState[r4].view + +\* InvFaultNodesCount states that there can be F faulty or dead nodes at max. +InvFaultNodesCount == Cardinality({ + r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead" + }) <= F + +\* This theorem asserts the truth of the temporal formula whose meaning is that +\* the state predicates TypeOK, InvTwoBlocksAccepted, InvDeadlock and InvFaultNodesCount are +\* the invariants of the specification Spec. This theorem is not supposed to be +\* checked by the TLC model checker, it's here for the reader's understanding of +\* the purpose of TypeOK, InvTwoBlocksAccepted, InvDeadlock and InvFaultNodesCount. +THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvDeadlock /\ InvFaultNodesCount) + +============================================================================= +\* Modification History +\* Last modified Fri Feb 17 15:51:19 MSK 2023 by anna +\* Created Tue Jan 10 12:28:45 MSK 2023 by anna diff --git a/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch new file mode 100644 index 00000000..e522df66 --- /dev/null +++ b/formal-models/dbftMultipool/dbftMultipool___AllGoodModel.launch @@ -0,0 +1,44 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +