forked from tlaplus/Examples
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMCVoting.tla
More file actions
39 lines (33 loc) · 821 Bytes
/
Copy pathMCVoting.tla
File metadata and controls
39 lines (33 loc) · 821 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
---- MODULE MCVoting ----
EXTENDS Voting, TLC
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
a1, a2, a3
----
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
v1, v2
----
\* MV CONSTANT definitions Acceptor
const_156180051387243000 ==
{a1, a2, a3}
----
\* MV CONSTANT definitions Value
const_156180051387244000 ==
{v1, v2}
----
\* CONSTANT definitions @modelParameterConstants:2Quorum
const_156180051387245000 ==
{{a1, a2}, {a1, a3}, {a2, a3}}
----
\* CONSTANT definition @modelParameterDefinitions:0
def_ov_156180051387246000 ==
0..2
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_156180051387248000 ==
C!Spec
----
=============================================================================
\* Modification History
\* Created Sat Jun 29 02:28:33 PDT 2019 by lamport