sig Candidate {} sig Voter { ballot: lone Ballot } sig Ballot { choice: lone Candidate } sig Box { cast: set Ballot } one sig Tally { ballots: set Ballot, count: Candidate -> one Int } { all c: Candidate | count[c] = #(ballots & choice.c) } fact AllVotersCastBallots { all v: Voter | some x: Box | v.ballot in x.cast } fact NoBoxStuffing { all x: Box, b: x.cast | some ballot.b } fact NoTallyStuffing { all b: Tally.ballots | some x: Box | b in x.cast } fact NoBallotsLost { all x: Box | x.cast in Tally.ballots } fact NoSharedBallots { all b: Ballot | lone ballot.b } assert CountingCorrect { all c: Candidate | Tally.count[c] = #ballot.choice.c } run { some cast } -- and some count } check CountingCorrect for 5 run {some v: Voter | no x: Box | v.ballot in x.cast } for 2 /* sig Audit {checked: set Ballot } run {some b: Ballot | no a: Audit | b in a.checked some checked } for 2 */