Modeling Test Cases for Voting

The ballot counting process for Proportional Representation by Single Transferable Vote (PR-STV) elections can be modeled formally using the Alloy model checker so as to cover all possible branches through the ballot counting algorithm. We use the Alloy model finder to describe the elections in terms of scenarios, consisting of equivalence classes of possible outcomes for each candidate in the election, where each outcome represents one branch through the algorithm. We show how test data is generated from a first order logic representation of the counting algorithm using the Alloy model finder. This process guarantees that we find the minimal number of ballots needed to test each scenario.