Voting process
Basic voting process
This archetype defines a basic voting process. The chairman is responsible for registering voters. The use of the mutable extension gives the chairman the extra right to modify the voting agenda, in Created state only.
The result of the vote is computed with the bury action: winners are ballots with the highest number of votes.
voting:process.arl
1
archetype voting_process
2
3
variable[%transferable%] chairperson : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
4
5
(* vote start *)
6
variable[%mutable (chairperson, (instate (Created)))%] startDate : date = 2019-11-12T00:00:00
7
8
(* vote deadline *)
9
variable[%mutable (chairperson, (instate (Created)))%] deadline : date = 2020-11-12T00:00:00
10
11
asset voter identified by addr {
12
addr : role;
13
hasVoted : bool
14
}
15
16
asset ballot identified by value {
17
value : string;
18
nbvotes : int;
19
}
20
21
asset winner {
22
winvalue : string
23
}
24
25
(* state machine *)
26
states =
27
| Created initial with { s1 : winner.isempty(); }
28
| Voting with { s2 : winner.isempty(); }
29
| Buried
30
31
action register (v : role) {
32
called by chairperson
33
require {
34
c1 : state = Created;
35
}
36
effect {
37
voter.add({ addr = v; hasVoted = false })
38
}
39
}
40
41
transition start () {
42
from Created
43
to Voting when { now > startDate }
44
}
45
46
action vote (val : pkey of ballot) {
47
require {
48
c2 : voter.contains(caller);
49
c3 : state = Voting;
50
c4 : voter.get(caller).hasVoted = false;
51
}
52
53
effect {
54
voter.update (caller, { hasVoted = true });
55
if ballot.contains(val) then
56
ballot.update(val,{ nbvotes += 1})
57
else
58
ballot.add({ value = val; nbvotes = 1})
59
}
60
}
61
62
transition bury () {
63
require {
64
c5 : now > deadline;
65
}
66
from Voting
67
to Buried
68
with effect {
69
let nbvotesMax = ballot.max(the.nbvotes) in
70
for b in ballot do
71
if (b.nbvotes = nbvotesMax)
72
then winner.add({ winvalue = b.value })
73
done
74
}
75
}
76
77
specification {
78
contract invariant s3 {
79
startDate < deadline
80
}
81
contract invariant s4 {
82
(voter.select(the.hasVoted = true)).count() = ballot.sum(the.nbvotes)
83
}
84
contract invariant s5 {
85
forall w in winner,
86
forall b in ballot,
87
let some wb = ballot.get(w.winvalue) in
88
b.nbvotes <= wb.nbvotes
89
otherwise false
90
}
91
}
Copied!
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub