Offline Team2 Benchmark2

Candidate Selection. This property is about voters ranking candidates for a party. Primarily it demonstrates the use of existential quantification in the QEA formalism.

Benchmark Data

The Trace Part

<< Will appear shortly>

The Property Part

Informal Description

We consider three entities: voters, parties and candidates. The property states that for every voter there must exist a party that the voter is a member of, and the voter must rank all candidates for that party. More precisely, every voter v must be a member of at least one party p, recorded as member(v,p), and for every candidate c, if c is a candidate for p, recorded as candidate(c,p), then v must rank c, recorded as rank(v,c,r) where r is the rank.

Demonstration Traces

The following traces should be accepted:

   member(alice,A).candidate(bob,A).rank(alice,bob,1)
   member(alice,A).candidate(bob,A).member(alice,B).rank(alice,bob,1)
   member(alice,A).candidate(bob,A).candidate(eva,A).rank(alice,bob,2).rank(alice,eva,1)
   member(alice,A).member(bob,B).candidate(bob,A).rank(alice,bob,1)
   member(alice,A).member(alice,B).candidate(bob,A)

This last trace is valid due to a technicality... alice ranks all candidates from party B as there are no candidates for party B.

The following traces should be rejected

   member(alice,A).candidate(bob,A)
   member(alice,A).candidate(bob,A).candidate(eva,A).rank(alice,bob,1)
   member(alice,A).member(bob,A).candidate(bob,A).rank(bob,alice,1)

All of these are invalid as alice does not rank every candidate for party A (the only party she is a member of).

Formal Specification

A QEA for this property can be given as

   qea(CandidateSelection){
     Forall(v) Exists(p) Forall(c)

     skip(noparty)          {  member(v,p) -> hasparty }
     accept skip(hasparty)  {  candidate(c,p) -> shouldrank }
     skip(shouldrank)       { rank(v,c,r) -> success }
   }

Clarification Requests

This is a space where other teams can ask for clarifications and the submitting team can answer. When a team requests a clarification, the team should be mentioned in the request and the request timestamped. The team submitting the benchmark should ensure they watch this page so that they get notifications of questions.