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.

archetype voting_process
variable chairperson : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
variable chairperson_tmp : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
(* vote start *)
variable startDate : date = 2019-11-12T00:00:00
(* vote deadline *)
variable deadline : date = 2020-11-12T00:00:00
asset voter identified by addr {
addr : role;
hasVoted : bool
}
asset ballot identified by value {
value : string;
nbvotes : int;
}
asset winner {
winvalue : string
}
(* state machine *)
states =
| Created initial with { s1 : winner.isempty(); }
| Voting with { s2 : winner.isempty(); }
| Buried
entry register (v : role) {
called by chairperson
require {
c1 : state = Created;
}
effect {
voter.add({ addr = v; hasVoted = false })
}
}
transition start () {
from Created
to Voting when { now > startDate }
}
entry vote (val : pkey of ballot) {
require {
c2 : voter.contains(caller);
c3 : state = Voting;
c4 : voter[caller].hasVoted = false;
}
effect {
voter.update (caller, { hasVoted = true });
if ballot.contains(val) then
ballot.update(val,{ nbvotes += 1})
else
ballot.add({ value = val; nbvotes = 1})
}
}
transition bury () {
require {
c5 : now > deadline;
}
from Voting
to Buried
with effect {
var nbvotesMax = 0;
for b in ballot do
nbvotesMax := max(nbvotesMax, ballot[b].nbvotes)
done;
for b in ballot do
if (ballot[b].nbvotes = nbvotesMax)
then winner.add({ winvalue = ballot[b].value })
done
}
}
specification {
contract invariant s3 {
startDate < deadline
}
contract invariant s4 {
(voter.select(the.hasVoted = true)).count() = ballot.sum(the.nbvotes)
}
contract invariant s5 {
forall w in winner,
forall b in ballot,
let some wb = ballot[w.winvalue] in
b.nbvotes <= wb.nbvotes
otherwise false
}
}
entry assign_new_chairperson (newrole : role) {
called by chairperson
effect {
chairperson_tmp := newrole;
}
}
entry confirm_chairperson () {
called by chairperson_tmp
effect {
chairperson := chairperson_tmp;
}
}
entry set_startDate (newstartDate : date) {
called by chairperson
require {
set_startDate_c1 : state = Created;
}
effect {
startDate := newstartDate
}
}
entry set_deadline (newdeadline : date) {
called by chairperson
require {
set_deadline_c1 : state = Created;
}
effect {
deadline := newdeadline
}
}
Edit on GitHub