Difference between revisions of "Offline Team2 Benchmark2"
(Created page with "'''Candidate Selection'''. This property is about voters ranking candidates for a party. Primarily it demonstrates the use of existential quantification in the QEA formalism....") |
(→The Trace Part) |
||
| Line 5: | Line 5: | ||
=== The Trace Part === | === The Trace Part === | ||
| − | + | There are three traces in marq/offline/bench2 | |
| + | * cand_sel_valid | ||
| + | * cand_sel_invalid1 | ||
| + | * cand_sel_invalid2 | ||
| + | cand_sel_valid consists of 977,998 events. The breakdown is | ||
| + | * member: 343,133 | ||
| + | * candidate: 6,761 | ||
| + | * rank: 628,335 | ||
| + | it satisfies the property. | ||
| + | |||
| + | cand_sel_invalid1 and cand_sel_invalid2 do not satisfy the property. They both remove an event from cand_sel_valid. The first removes a member event, meaning that a voter is not a member of any party. The second removes a rank event, meaning that a voter does not rank all candidates for their party. | ||
| + | |||
| + | The cand_sel_invalid2 trace is the one that is supposed to be used for the competition, the others are for testing. | ||
=== The Property Part === | === The Property Part === | ||
Latest revision as of 15:56, 7 June 2016
Candidate Selection. This property is about voters ranking candidates for a party. Primarily it demonstrates the use of existential quantification in the QEA formalism.
Contents
Benchmark Data
The Trace Part
There are three traces in marq/offline/bench2
- cand_sel_valid
- cand_sel_invalid1
- cand_sel_invalid2
cand_sel_valid consists of 977,998 events. The breakdown is
- member: 343,133
- candidate: 6,761
- rank: 628,335
it satisfies the property.
cand_sel_invalid1 and cand_sel_invalid2 do not satisfy the property. They both remove an event from cand_sel_valid. The first removes a member event, meaning that a voter is not a member of any party. The second removes a rank event, meaning that a voter does not rank all candidates for their party.
The cand_sel_invalid2 trace is the one that is supposed to be used for the competition, the others are for testing.
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 }
}
A FO-LTL Specification
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.
