Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 37c84f9

Browse files
AnnaShalevaAnnaShaleva
committedApr 25, 2024·
formal-models: extend dBFT with additional post-commit phase
Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
1 parent 6abc124 commit 37c84f9

File tree

2 files changed

+476
-0
lines changed

2 files changed

+476
-0
lines changed
 

‎formal-models/dbft3.0/dbft.tla

+434
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,434 @@
1+
-------------------------------- MODULE dbft --------------------------------
2+
3+
EXTENDS
4+
Integers,
5+
FiniteSets
6+
7+
CONSTANTS
8+
\* RM is the set of consensus node indexes starting from 0.
9+
\* Example: {0, 1, 2, 3}
10+
RM,
11+
12+
\* RMFault is a set of consensus node indexes that are allowed to become
13+
\* FAULT in the middle of every considered behavior and to send any
14+
\* consensus message afterwards. RMFault must be a subset of RM. An empty
15+
\* set means that all nodes are good in every possible behaviour.
16+
\* Examples: {0}
17+
\* {1, 3}
18+
\* {}
19+
RMFault,
20+
21+
\* RMDead is a set of consensus node indexes that are allowed to die in the
22+
\* middle of every behaviour and do not send any message afterwards. RMDead
23+
\* must be a subset of RM. An empty set means that all nodes are alive and
24+
\* responding in in every possible behaviour. RMDead may intersect the
25+
\* RMFault set which means that node which is in both RMDead and RMFault
26+
\* may become FAULT and send any message starting from some step of the
27+
\* particular behaviour and may also die in the same behaviour which will
28+
\* prevent it from sending any message.
29+
\* Examples: {0}
30+
\* {3, 2}
31+
\* {}
32+
RMDead,
33+
34+
\* MaxView is the maximum allowed view to be considered (starting from 0,
35+
\* including the MaxView itself). This constraint was introduced to reduce
36+
\* the number of possible model states to be checked. It is recommended to
37+
\* keep this setting not too high (< N is highly recommended).
38+
\* Example: 2
39+
MaxView
40+
41+
VARIABLES
42+
\* rmState is a set of consensus node states. It is represented by the
43+
\* mapping (function) with domain RM and range RMStates. I.e. rmState[r] is
44+
\* the state of the r-th consensus node at the current step.
45+
rmState,
46+
47+
\* msgs is the shared pool of messages sent to the network by consensus nodes.
48+
\* It is represented by a subset of Messages set.
49+
msgs
50+
51+
\* vars is a tuple of all variables used in the specification. It is needed to
52+
\* simplify fairness conditions definition.
53+
vars == <<rmState, msgs>>
54+
55+
\* N is the number of validators.
56+
N == Cardinality(RM)
57+
58+
\* F is the number of validators that are allowed to be malicious.
59+
F == (N - 1) \div 3
60+
61+
\* M is the number of validators that must function correctly.
62+
M == N - F
63+
64+
\* These assumptions are checked by the TLC model checker once at the start of
65+
\* the model checking process. All the input data (declared constants) specified
66+
\* in the "Model Overview" section must satisfy these constraints.
67+
ASSUME
68+
/\ RM \subseteq Nat
69+
/\ N >= 4
70+
/\ 0 \in RM
71+
/\ RMFault \subseteq RM
72+
/\ RMDead \subseteq RM
73+
/\ Cardinality(RMFault) <= F
74+
/\ Cardinality(RMDead) <= F
75+
/\ Cardinality(RMFault \cup RMDead) <= F
76+
/\ MaxView \in Nat
77+
/\ MaxView <= 2
78+
79+
\* RMStates is a set of records where each record holds the node state and
80+
\* the node current view.
81+
RMStates == [
82+
type: {"initialized", "prepareSent", "commitSent", "cv", "ackSent", "blockAccepted", "bad", "dead"},
83+
view : Nat
84+
]
85+
86+
\* Messages is a set of records where each record holds the message type,
87+
\* the message sender and sender's view by the moment when message was sent.
88+
Messages == [type : {"PrepareRequest", "PrepareResponse", "Commit", "Ack", "ChangeView"}, rm : RM, view : Nat]
89+
90+
\* -------------- Useful operators --------------
91+
92+
\* IsPrimary is an operator defining whether provided node r is primary
93+
\* for the current round from the r's point of view. It is a mapping
94+
\* from RM to the set of {TRUE, FALSE}.
95+
IsPrimary(r) == rmState[r].view % N = r
96+
97+
\* GetPrimary is an operator defining mapping from round index to the RM that
98+
\* is primary in this round.
99+
GetPrimary(view) == CHOOSE r \in RM : view % N = r
100+
101+
\* GetNewView returns new view number based on the previous node view value.
102+
\* Current specifications only allows to increment view.
103+
GetNewView(oldView) == oldView + 1
104+
105+
\* CountCommitted returns the number of nodes that have sent the Commit message
106+
\* in the current round or in some other round.
107+
CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit"}) /= 0})
108+
109+
\* MoreThanFNodesCommitted returns whether more than F nodes have been committed
110+
\* in the current round (as the node r sees it).
111+
\*
112+
\* IMPORTANT NOTE: we intentionally do not add the "lost" nodes calculation to the specification, and here's
113+
\* the reason: from the node's point of view we can't reliably check that some neighbour is completely
114+
\* out of the network. It is possible that the node doesn't receive consensus messages from some other member
115+
\* due to network delays. On the other hand, real nodes can go down at any time. The absence of the
116+
\* member's message doesn't mean that the member is out of the network, we never can be sure about
117+
\* that, thus, this information is unreliable and can't be trusted during the consensus process.
118+
\* What can be trusted is whether there's a Commit message from some member was received by the node.
119+
MoreThanFNodesCommitted(r) == CountCommitted(r) > F
120+
121+
\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
122+
\* message received from the current round's speaker (as the node r sees it).
123+
PrepareRequestSentOrReceived(r) == [type |-> "PrepareRequest", rm |-> GetPrimary(rmState[r].view), view |-> rmState[r].view] \in msgs
124+
125+
\* -------------- Safety temporal formula --------------
126+
127+
\* Init is the initial predicate initializing values at the start of every
128+
\* behaviour.
129+
Init ==
130+
/\ rmState = [r \in RM |-> [type |-> "initialized", view |-> 0]]
131+
/\ msgs = {}
132+
133+
\* RMSendPrepareRequest describes the primary node r broadcasting PrepareRequest.
134+
RMSendPrepareRequest(r) ==
135+
/\ rmState[r].type = "initialized"
136+
/\ IsPrimary(r)
137+
/\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
138+
/\ msgs' = msgs \cup {[type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]}
139+
/\ UNCHANGED <<>>
140+
141+
\* RMSendPrepareResponse describes non-primary node r receiving PrepareRequest from
142+
\* the primary node of the current round (view) and broadcasting PrepareResponse.
143+
\* This step assumes that PrepareRequest always contains valid transactions and
144+
\* signatures.
145+
RMSendPrepareResponse(r) ==
146+
/\ \/ rmState[r].type = "initialized"
147+
\* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage
148+
\* as it is done in the code-level dBFT implementation by checking the NotAcceptingPayloadsDueToViewChanging
149+
\* condition (see
150+
\* https://github.com/nspcc-dev/dbft/blob/31c1bbdc74f2faa32ec9025062e3a4e2ccfd4214/dbft.go#L419
151+
\* and
152+
\* https://github.com/neo-project/neo-modules/blob/d00d90b9c27b3d0c3c57e9ca1f560a09975df241/src/DBFTPlugin/Consensus/ConsensusService.OnMessage.cs#L79).
153+
\* However, we can't easily count the number of "lost" nodes in this specification to match precisely
154+
\* the implementation. Moreover, we don't need it to be counted as the RMSendPrepareResponse enabling
155+
\* condition specifies only the thing that may happen given some particular set of enabling conditions.
156+
\* Thus, we've extended the NotAcceptingPayloadsDueToViewChanging condition to consider only MoreThanFNodesCommitted.
157+
\* It should be noted that the logic of MoreThanFNodesCommittedOrLost can't be reliable in detecting lost nodes
158+
\* (even with neo-project/neo#2057), because real nodes can go down at any time. See the comment above the MoreThanFNodesCommitted.
159+
\/ /\ rmState[r].type = "cv"
160+
/\ MoreThanFNodesCommitted(r)
161+
/\ \neg IsPrimary(r)
162+
/\ PrepareRequestSentOrReceived(r)
163+
/\ rmState' = [rmState EXCEPT ![r].type = "prepareSent"]
164+
/\ msgs' = msgs \cup {[type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]}
165+
/\ UNCHANGED <<>>
166+
167+
\* RMSendCommit describes node r sending Commit if there's enough PrepareResponse
168+
\* messages.
169+
RMSendCommit(r) ==
170+
/\ \/ rmState[r].type = "prepareSent"
171+
\* We do allow the transition from the "cv" state to the "prepareSent" or "commitSent" stage,
172+
\* see the related comment inside the RMSendPrepareResponse definition.
173+
\/ /\ rmState[r].type = "cv"
174+
/\ MoreThanFNodesCommitted(r)
175+
/\ Cardinality({
176+
msg \in msgs : /\ (msg.type = "PrepareResponse" \/ msg.type = "PrepareRequest")
177+
/\ msg.view = rmState[r].view
178+
}) >= M
179+
/\ PrepareRequestSentOrReceived(r)
180+
/\ rmState' = [rmState EXCEPT ![r].type = "commitSent"]
181+
/\ msgs' = msgs \cup {[type |-> "Commit", rm |-> r, view |-> rmState[r].view]}
182+
/\ UNCHANGED <<>>
183+
184+
\* RMAcceptBlock describes node r collecting enough Commit messages and sending
185+
\* the Ack message.
186+
RMSendAck(r) ==
187+
/\ rmState[r].type /= "bad"
188+
/\ rmState[r].type /= "dead"
189+
/\ rmState[r].type /= "ackSent"
190+
/\ rmState[r].type /= "blockAccepted"
191+
/\ PrepareRequestSentOrReceived(r)
192+
/\ Cardinality({msg \in msgs : msg.type = "Commit" /\ msg.view = rmState[r].view}) >= M
193+
/\ rmState' = [rmState EXCEPT ![r].type = "ackSent"]
194+
/\ msgs' = msgs \cup {[type |-> "Ack", rm |-> r, view |-> rmState[r].view]}
195+
/\ UNCHANGED <<>>
196+
197+
\* RMAcceptBlock describes node r collecting enough Ack messages and accepting
198+
\* the block.
199+
RMAcceptBlock(r) ==
200+
/\ rmState[r].type = "ackSent"
201+
/\ Cardinality({msg \in msgs : msg.type = "Ack" /\ msg.view = rmState[r].view}) >= M
202+
/\ rmState' = [rmState EXCEPT ![r].type = "blockAccepted"]
203+
/\ UNCHANGED <<msgs>>
204+
205+
\* RMSendChangeView describes node r sending ChangeView message on timeout.
206+
RMSendChangeView(r) ==
207+
/\ \/ (rmState[r].type = "initialized" /\ \neg IsPrimary(r))
208+
\/ rmState[r].type = "prepareSent"
209+
/\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view]
210+
IN /\ cv \notin msgs
211+
/\ rmState' = [rmState EXCEPT ![r].type = "cv"]
212+
/\ msgs' = msgs \cup {[type |-> "ChangeView", rm |-> r, view |-> rmState[r].view]}
213+
214+
\* RMReceiveChangeView describes node r receiving enough ChangeView messages for
215+
\* view changing.
216+
RMReceiveChangeView(r) ==
217+
/\ rmState[r].type /= "bad"
218+
/\ rmState[r].type /= "dead"
219+
/\ rmState[r].type /= "blockAccepted"
220+
/\ rmState[r].type /= "commitSent"
221+
/\ rmState[r].type /= "ackSent"
222+
/\ Cardinality({
223+
rm \in RM : Cardinality({
224+
msg \in msgs : /\ msg.type = "ChangeView"
225+
/\ msg.rm = rm
226+
/\ GetNewView(msg.view) >= GetNewView(rmState[r].view)
227+
}) /= 0
228+
}) >= M
229+
/\ rmState' = [rmState EXCEPT ![r].type = "initialized", ![r].view = GetNewView(rmState[r].view)]
230+
/\ UNCHANGED <<msgs>>
231+
232+
\* RMBeBad describes the faulty node r that will send any kind of consensus message starting
233+
\* from the step it's gone wild. This step is enabled only when RMFault is non-empty set.
234+
RMBeBad(r) ==
235+
/\ r \in RMFault
236+
/\ Cardinality({rm \in RM : rmState[rm].type = "bad"}) < F
237+
/\ rmState' = [rmState EXCEPT ![r].type = "bad"]
238+
/\ UNCHANGED <<msgs>>
239+
240+
\* RMFaultySendCV describes sending CV message by the faulty node r.
241+
RMFaultySendCV(r) ==
242+
/\ rmState[r].type = "bad"
243+
/\ LET cv == [type |-> "ChangeView", rm |-> r, view |-> rmState[r].view]
244+
IN /\ cv \notin msgs
245+
/\ msgs' = msgs \cup {cv}
246+
/\ UNCHANGED <<rmState>>
247+
248+
\* RMFaultyDoCV describes view changing by the faulty node r.
249+
RMFaultyDoCV(r) ==
250+
/\ rmState[r].type = "bad"
251+
/\ rmState' = [rmState EXCEPT ![r].view = GetNewView(rmState[r].view)]
252+
/\ UNCHANGED <<msgs>>
253+
254+
\* RMFaultySendPReq describes sending PrepareRequest message by the primary faulty node r.
255+
RMFaultySendPReq(r) ==
256+
/\ rmState[r].type = "bad"
257+
/\ IsPrimary(r)
258+
/\ LET pReq == [type |-> "PrepareRequest", rm |-> r, view |-> rmState[r].view]
259+
IN /\ pReq \notin msgs
260+
/\ msgs' = msgs \cup {pReq}
261+
/\ UNCHANGED <<rmState>>
262+
263+
\* RMFaultySendPResp describes sending PrepareResponse message by the non-primary faulty node r.
264+
RMFaultySendPResp(r) ==
265+
/\ rmState[r].type = "bad"
266+
/\ \neg IsPrimary(r)
267+
/\ LET pResp == [type |-> "PrepareResponse", rm |-> r, view |-> rmState[r].view]
268+
IN /\ pResp \notin msgs
269+
/\ msgs' = msgs \cup {pResp}
270+
/\ UNCHANGED <<rmState>>
271+
272+
\* RMFaultySendCommit describes sending Commit message by the faulty node r.
273+
RMFaultySendCommit(r) ==
274+
/\ rmState[r].type = "bad"
275+
/\ LET commit == [type |-> "Commit", rm |-> r, view |-> rmState[r].view]
276+
IN /\ commit \notin msgs
277+
/\ msgs' = msgs \cup {commit}
278+
/\ UNCHANGED <<rmState>>
279+
280+
\* RMFaultySendAck describes sending Ack message by the faulty node r.
281+
RMFaultySendAck(r) ==
282+
/\ rmState[r].type = "bad"
283+
/\ LET ack == [type |-> "Ack", rm |-> r, view |-> rmState[r].view]
284+
IN /\ ack \notin msgs
285+
/\ msgs' = msgs \cup {ack}
286+
/\ UNCHANGED <<rmState>>
287+
288+
\* RMDie describes node r that was removed from the network at the particular step
289+
\* of the behaviour. After this node r can't change its state and accept/send messages.
290+
RMDie(r) ==
291+
/\ r \in RMDead
292+
/\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) < F
293+
/\ rmState' = [rmState EXCEPT ![r].type = "dead"]
294+
/\ UNCHANGED <<msgs>>
295+
296+
\* Terminating is an action that allows infinite stuttering to prevent deadlock on
297+
\* behaviour termination. We consider termination to be valid if at least M nodes
298+
\* has the block being accepted.
299+
Terminating ==
300+
/\ Cardinality({rm \in RM : rmState[rm].type = "blockAccepted"}) >= M
301+
/\ UNCHANGED <<msgs, rmState>>
302+
303+
\* TerminatingFourNodesDeadlock describes node r that is in the state where dBFT stucks in a four
304+
\* nodes scenario. Allow infinite stuttering to prevent TLC deadlock recognition.
305+
TerminatingFourNodesDeadlockSameView(r) ==
306+
/\ Cardinality({rm \in RM : rmState[rm].type = "dead" /\ rmState[rm].view = rmState[r].view}) = 1
307+
/\ Cardinality({rm \in RM : rmState[rm].type = "cv" /\ rmState[rm].view = rmState[r].view}) = 2
308+
/\ Cardinality({rm \in RM : rmState[rm].type = "commitSent" /\ rmState[rm].view = rmState[r].view}) = 1
309+
/\ UNCHANGED <<msgs, rmState>>
310+
311+
\* TerminatingFourNodesDeadlock describes node r that is in the state where dBFT stucks in a four
312+
\* nodes scenario and the same view. Allow infinite stuttering to prevent TLC deadlock recognition.
313+
TerminatingFourNodesDeadlock ==
314+
/\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) = 1
315+
/\ Cardinality({rm \in RM : rmState[rm].type = "cv"}) = 2
316+
/\ Cardinality({rm \in RM : rmState[rm].type = "commitSent"}) = 1
317+
/\ UNCHANGED <<msgs, rmState>>
318+
319+
\* Next is the next-state action describing the transition from the current state
320+
\* to the next state of the behaviour.
321+
Next ==
322+
\/ Terminating
323+
\/ \E r \in RM:
324+
RMSendPrepareRequest(r) \/ RMSendPrepareResponse(r) \/ RMSendCommit(r) \/ RMSendAck(r)
325+
\/ RMAcceptBlock(r) \/ RMSendChangeView(r) \/ RMReceiveChangeView(r)
326+
\/ RMDie(r) \/ RMBeBad(r)
327+
\/ RMFaultySendCV(r) \/ RMFaultyDoCV(r) \/ RMFaultySendCommit(r) \/ RMFaultySendAck(r) \/ RMFaultySendPReq(r) \/ RMFaultySendPResp(r)
328+
\/ TerminatingFourNodesDeadlock
329+
\* \/ TerminatingFourNodesDeadlockSameView(r)
330+
331+
\* Safety is a temporal formula that describes the whole set of allowed
332+
\* behaviours. It specifies only what the system MAY do (i.e. the set of
333+
\* possible allowed behaviours for the system). It asserts only what may
334+
\* happen; any behaviour that violates it does so at some point and
335+
\* nothing past that point makes difference.
336+
\*
337+
\* E.g. this safety formula (applied standalone) allows the behaviour to end
338+
\* with an infinite set of stuttering steps (those steps that DO NOT change
339+
\* neither msgs nor rmState) and never reach the state where at least one
340+
\* node is committed or accepted the block.
341+
\*
342+
\* To forbid such behaviours we must specify what the system MUST
343+
\* do. It will be specified below with the help of fairness conditions in
344+
\* the Fairness formula.
345+
Safety == Init /\ [][Next]_vars
346+
347+
\* -------------- Fairness temporal formula --------------
348+
349+
\* Fairness is a temporal assumptions under which the model is working.
350+
\* Usually it specifies different kind of assumptions for each/some
351+
\* subactions of the Next's state action, but the only think that bothers
352+
\* us is preventing infinite stuttering at those steps where some of Next's
353+
\* subactions are enabled. Thus, the only thing that we require from the
354+
\* system is to keep take the steps until it's impossible to take them.
355+
\* That's exactly how the weak fairness condition works: if some action
356+
\* remains continuously enabled, it must eventually happen.
357+
Fairness == WF_vars(Next)
358+
359+
\* -------------- Specification --------------
360+
361+
\* The complete specification of the protocol written as a temporal formula.
362+
Spec == Safety /\ Fairness
363+
364+
\* -------------- Liveness temporal formula --------------
365+
366+
\* For every possible behaviour it's true that eventually (i.e. at least once
367+
\* through the behaviour) block will be accepted. It is something that dBFT
368+
\* must guarantee (an in practice this condition is violated).
369+
TerminationRequirement == <>(
370+
\/ Cardinality({r \in RM : rmState[r].type = "blockAccepted"}) >= M
371+
\/ /\ Cardinality({rm \in RM : rmState[rm].type = "dead"}) = 1
372+
/\ Cardinality({rm \in RM : rmState[rm].type = "cv"}) = 2
373+
/\ Cardinality({rm \in RM : rmState[rm].type = "commitSent"}) = 1
374+
\* \/ \E r \in RM: /\ Cardinality({rm \in RM : rmState[rm].type = "dead" /\ rmState[rm].view = rmState[r].view}) = 1
375+
\* /\ Cardinality({rm \in RM : rmState[rm].type = "cv" /\ rmState[rm].view = rmState[r].view}) = 2
376+
\* /\ Cardinality({rm \in RM : rmState[rm].type = "commitSent" /\ rmState[rm].view = rmState[r].view}) = 1
377+
)
378+
379+
\* A liveness temporal formula asserts only what must happen (i.e. specifies
380+
\* what the system MUST do). Any behaviour can NOT violate it at ANY point;
381+
\* there's always the rest of the behaviour that can always make the liveness
382+
\* formula true; if there's no such behaviour than the liveness formula is
383+
\* violated. The liveness formula is supposed to be checked as a property
384+
\* by the TLC model checker.
385+
Liveness == TerminationRequirement
386+
387+
\* -------------- ModelConstraints --------------
388+
389+
\* MaxViewConstraint is a state predicate restricting the number of possible
390+
\* behaviour states. It is needed to reduce model checking time and prevent
391+
\* the model graph size explosion. This formulae must be specified at the
392+
\* "State constraint" section of the "Additional Spec Options" section inside
393+
\* the model overview.
394+
MaxViewConstraint == /\ \A r \in RM : rmState[r].view <= MaxView
395+
/\ \A msg \in msgs : msg.view <= MaxView
396+
397+
\* -------------- Invariants of the specification --------------
398+
399+
\* Model invariant is a state predicate (statement) that must be true for
400+
\* every step of every reachable behaviour. Model invariant is supposed to
401+
\* be checked as an Invariant by the TLC Model Checker.
402+
403+
\* TypeOK is a type-correctness invariant. It states that all elements of
404+
\* specification variables must have the proper type throughout the behaviour.
405+
TypeOK ==
406+
/\ rmState \in [RM -> RMStates]
407+
/\ msgs \subseteq Messages
408+
409+
\* InvTwoBlocksAccepted states that there can't be two different blocks accepted in
410+
\* the two different views, i.e. dBFT must not allow forks.
411+
InvTwoBlocksAccepted == \A r1 \in RM:
412+
\A r2 \in RM \ {r1}:
413+
\/ rmState[r1].type /= "blockAccepted"
414+
\/ rmState[r2].type /= "blockAccepted"
415+
\/ rmState[r1].view = rmState[r2].view
416+
417+
\* InvFaultNodesCount states that there can be F faulty or dead nodes at max.
418+
InvFaultNodesCount == Cardinality({
419+
r \in RM : rmState[r].type = "bad" \/ rmState[r].type = "dead"
420+
}) <= F
421+
422+
\* This theorem asserts the truth of the temporal formula whose meaning is that
423+
\* the state predicates TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount are
424+
\* the invariants of the specification Spec. This theorem is not supposed to be
425+
\* checked by the TLC model checker, it's here for the reader's understanding of
426+
\* the purpose of TypeOK, InvTwoBlocksAccepted and InvFaultNodesCount.
427+
THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount)
428+
429+
=============================================================================
430+
\* Modification History
431+
\* Last modified Thu Apr 25 20:03:18 MSK 2024 by anna
432+
\* Last modified Mon Mar 06 15:36:57 MSK 2023 by root
433+
\* Last modified Sat Jan 21 01:26:16 MSK 2023 by rik
434+
\* Created Thu Dec 15 16:06:17 MSK 2022 by anna

‎formal-models/dbft3.0/dbft___AllGoodModel.launch

+42
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
2+
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
3+
<stringAttribute key="configurationName" value="AllGoodModel"/>
4+
<intAttribute key="distributedFPSetCount" value="0"/>
5+
<stringAttribute key="distributedNetworkInterface" value="172.200.0.254"/>
6+
<intAttribute key="distributedNodesCount" value="1"/>
7+
<stringAttribute key="distributedTLC" value="off"/>
8+
<intAttribute key="fpIndex" value="47"/>
9+
<intAttribute key="maxHeapSize" value="50"/>
10+
<stringAttribute key="modelBehaviorInit" value=""/>
11+
<stringAttribute key="modelBehaviorNext" value=""/>
12+
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
13+
<intAttribute key="modelBehaviorSpecType" value="1"/>
14+
<stringAttribute key="modelBehaviorVars" value="msgs, rmState"/>
15+
<stringAttribute key="modelComments" value=""/>
16+
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
17+
<listAttribute key="modelCorrectnessInvariants">
18+
<listEntry value="1TypeOK"/>
19+
<listEntry value="1InvTwoBlocksAccepted"/>
20+
<listEntry value="1InvFaultNodesCount"/>
21+
</listAttribute>
22+
<listAttribute key="modelCorrectnessProperties">
23+
<listEntry value="1Liveness"/>
24+
</listAttribute>
25+
<intAttribute key="modelEditorOpenTabs" value="10"/>
26+
<stringAttribute key="modelParameterActionConstraint" value=""/>
27+
<listAttribute key="modelParameterConstants">
28+
<listEntry value="RMFault;;{};0;0"/>
29+
<listEntry value="MaxView;;1;0;0"/>
30+
<listEntry value="RMDead;;{};0;0"/>
31+
<listEntry value="RM;;{0, 1, 2, 3};0;0"/>
32+
</listAttribute>
33+
<stringAttribute key="modelParameterContraint" value="MaxViewConstraint"/>
34+
<listAttribute key="modelParameterDefinitions"/>
35+
<stringAttribute key="modelParameterModelValues" value="{}"/>
36+
<stringAttribute key="modelParameterNewDefinitions" value=""/>
37+
<intAttribute key="modelVersion" value="20191005"/>
38+
<intAttribute key="numberOfWorkers" value="8"/>
39+
<stringAttribute key="result.mail.address" value=""/>
40+
<stringAttribute key="specName" value="dbft"/>
41+
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
42+
</launchConfiguration>

0 commit comments

Comments
 (0)
Please sign in to comment.