Voting process
Basic voting process
This archetype defines a basic voting process. The chairman is responsible for registering voters.
The result of the vote is computed with the bury action: winners are ballots with the highest number of votes.
1
archetype voting_process
2
3
variable chairperson : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
4
5
variable chairperson_tmp : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
6
7
(* vote start *)
8
variable startDate : date = 2019-11-12T00:00:00
9
10
(* vote deadline *)
11
variable deadline : date = 2020-11-12T00:00:00
12
13
asset voter identified by addr {
14
addr : role;
15
hasVoted : bool
16
}
17
18
asset ballot identified by value {
19
value : string;
20
nbvotes : int;
21
}
22
23
asset winner {
24
winvalue : string
25
}
26
27
(* state machine *)
28
states =
29
| Created initial with { s1 : winner.isempty(); }
30
| Voting with { s2 : winner.isempty(); }
31
| Buried
32
33
entry register (v : role) {
34
called by chairperson
35
require {
36
c1 : state = Created;
37
}
38
effect {
39
voter.add({ addr = v; hasVoted = false })
40
}
41
}
42
43
transition start () {
44
from Created
45
to Voting when { now > startDate }
46
}
47
48
entry vote (val : pkey<ballot>) {
49
require {
50
c2 : voter.contains(caller);
51
c3 : state = Voting;
52
c4 : voter[caller].hasVoted = false;
53
}
54
55
effect {
56
voter.update (caller, { hasVoted = true });
57
if ballot.contains(val) then
58
ballot.update(val,{ nbvotes += 1})
59
else
60
ballot.add({ value = val; nbvotes = 1})
61
}
62
}
63
64
transition bury () {
65
require {
66
c5 : now > deadline;
67
}
68
from Voting
69
to Buried
70
with effect {
71
var nbvotesMax : int = 0;
72
for b in ballot do
73
nbvotesMax := max(nbvotesMax, ballot[b].nbvotes)
74
done;
75
for b in ballot do
76
if (ballot[b].nbvotes = nbvotesMax)
77
then winner.add({ winvalue = ballot[b].value })
78
done
79
}
80
}
81
82
specification {
83
contract invariant s3 {
84
startDate < deadline
85
}
86
contract invariant s4 {
87
(voter.select(the.hasVoted = true)).count() = ballot.sum(the.nbvotes)
88
}
89
contract invariant s5 {
90
forall w in winner,
91
forall b in ballot,
92
let some wb = ballot[w.winvalue] in
93
b.nbvotes <= wb.nbvotes
94
otherwise false
95
}
96
}
97
98
entry assign_new_chairperson (newrole : role) {
99
called by chairperson
100
effect {
101
chairperson_tmp := newrole;
102
}
103
}
104
105
entry confirm_chairperson () {
106
called by chairperson_tmp
107
effect {
108
chairperson := chairperson_tmp;
109
}
110
}
111
112
entry set_startDate (newstartDate : date) {
113
called by chairperson
114
require {
115
set_startDate_c1 : state = Created;
116
}
117
effect {
118
startDate := newstartDate
119
}
120
}
121
122
entry set_deadline (newdeadline : date) {
123
called by chairperson
124
require {
125
set_deadline_c1 : state = Created;
126
}
127
effect {
128
deadline := newdeadline
129
}
130
}
131
Copied!
Last modified 1yr ago
Export as PDF
Copy link