United States Election Assistance Comittee

Register to Vote!

Use the National Mail Voter Registration Form to register to vote, update your registration information with a new name or address, or register with a political party.

Note: If you wish to vote absentee and are a uniformed service member or family member or a citizen living outside the U.S., contact the Federal Voting Assistance Program to register to vote.

EAC Newsletters
and Updates

Sign up to receive information about EAC activities including public meetings, webcasts, reports and grants.

Give Us Your Feedback

Share your feedback on EAC policy proposalsElection Resource Library materials, and OpenEAC activities. Give feedback on general issues, including the Web site, through our Contact Us page.

Military and Overseas Voters

EAC has several projects under way to assist states in serving military and overseas citizens who register and vote absentee under the Uniformed and Overseas Citizens Absentee Voting Act. Learn more

Chapter 8: Reference Models

8.1 Process Model (informative)

8.1.1 Introduction

This section contains 16 diagrams describing the elections and voting process. The diagrams are expressed in Unified Modeling Language (UML) version 2.1.1 [OMG07].

A brief and incomplete guide to the notation is provided in Part 1: Table 8-1. It is not possible to explain accurate and full semantics for UML without extensive discussion which would be inappropriate here. For a complete and formal introduction, please see [OMG07].

Table 8-1 Guide to UML Activity Diagram notation

Shape

Meaning

Capsule

Action

Rectangle

Object

Arrow

Control or object flow

Bar

Fork/join

Diamond

Decision/merge

Dog-eared rectangle

Note

To simplify the diagrams, the following shortcuts have been taken:

  • The expansion regions around actions that are performed for every precinct or every voter are not shown.
  • When a particular object may or may not exist depending on system and jurisdiction-specific factors (e.g., paper-based vs. DRE), that object is modeled as an optional parameter to an action. This does not capture the constraint that subsequent actions must wait on this object in those jurisdictions where it applies (i.e., in some jurisdictions it is mandatory).
  • Objects that flow downstream in an obvious manner through many actions are not shown as inputs/outputs of all of those actions.
  • The propagation of the registration database from one election cycle to the next is not shown. The database appears as an input to the Register voters activity with no indication of its origin.
  • Many actions produce reports and other objects that eventually flow into the Archive action. These flows into the archive are not shown.
 

8.1.2 Diagrams

Figure 8-1 Administer elections

Administer elections

Figure 8-2 Prepare for election

Prepare
for election

Figure 8-3 Gather in-person vote (paper-based)

Gather
in-person vote (paper-based)

Figure 8-4 Gather in-person vote (DRE)

Gather
in-person vote (DRE)

Figure 8-5 Wrap up voting (precinct)

Wrap up
voting (precinct)

Figure 8-6 Wrap up voting (central)

Wrap up
voting (central)

Figure 8-7 Miscellaneous activities (1)

Miscellaneous activities (1)

Figure 8-8 Miscellaneous activities (2)

Miscellaneous activities (2)
 

3 Comments

Comment by Brian V. Jarvis (Local Election Official)

Regarding Figures 8-1 through 8-7. For each capsule (action) that is further expanded by another figure, recommend that you reference that expanded figure by it's figure number and subscript (if applicable) adjacent to the source capsule. This will improve readability and traceability from one figure to another.

Comment by Brian V. Jarvis (Local Election Official)

In the figures defining "Gather in-person vote" -- 8-3 (paper-based) and 8-4 (DRE) -- do you want to have a decision-point following "check voter eligibility" to depict the situation where the voter is determined to be not eligible to vote? This path would branch to the exit point.

Comment by Brian V. Jarvis (Local Election Official)

Regarding Figures 8-7 and 8-8. Recommend applying a subscript (e.g., (a), (b), (c)) along with an applicable short title adjacent to each of the small diagrams so that they can be easily referenced (e.g., Figure 8-7a, Figure 8-7b).

8.1.3 Translation of diagrams

This subsection contains a rendering of the process model into text. The rendering is based on the Petri Net Linear Form [Martin07]. At the time of this writing, a full discussion of the origins and formal definition of the notation are being prepared as a NIST IR with the working title "Rendering UML Activity Diagrams as Human-Readable Text."

Although the form of the diagrams is being changed from drawings to text, the meanings of the diagram elements—actions, objects, etc.—continue to be as in UML 2.1.1 [OMG07].

Actions are represented in this translation by the action name in parenthesis. Objects are represented in this translation by the object name in square brackets. Object states are represented with annotations of the form state=x.

Sequential control and object flows are indicated with ->.

A flow may be qualified by a guard condition and/or a multiplicity such as 0..1. These notations are inserted immediately before and after the affected flow. For example, Daytime->0..1("Drink coffee") denotes an optional flow into the "drink coffee" action that can only occur if the condition Daytime is true.

A node may be assigned an identifier that may be used as the target of flows from elsewhere in the diagram. The identifier is prefixed by an asterisk and is introduced by including it after the first occurrence of the node name. For example, ("Do something" *s) denotes an action "do something" with the identifier *s. The node name may be omitted in subsequent references that include only the identifier.

The following special nodes appear with semantics as in UML 2.1.1. They are distinguished from objects and actions by being enclosed between < and >.

  • <InitialNode>
  • <ForkNode>
  • <JoinNode>
  • <DecisionNode>
  • <MergeNode>
  • <ActivityFinal>
  • <FlowFinal>

When multiple flows follow from a node, they are listed between curly braces {} and separated by commas.

A semicolon indicates that the description is about to continue at a different node. A period indicates that the description of the diagram is complete.

Translation of the diagrams follows.

// Diagram:  Administer elections

<InitialNode>
  -><MergeNode *merge>
  ->("Prepare for election")
  ->["Equipment, voter lists, ballot styles and/or ballots"]
  -><ForkNode>{
    ->("Prepare for voting (precinct)")
      -><ForkNode>{
        ->("Gather in-person vote") // Includes early voting.
          ->["Ballots and/or ballot images"]
          ->(Collect *c),
        "Precinct count"
          ->("Count (precinct count)")
          ->["Machine totals"]
          ->0..1(*c)
      },
    ->("Gather absentee / remote votes")
      ->["Ballots and/or ballot images"]
      ->(*c),
    ->("Prepare for voting (central)")
      ->("Wrap up voting (central)" *w)
  };
(*c)
  ->["Ballots, ballot images and/or machine totals"]
  ->("Wrap up voting (precinct)")
  ->["Ballots, ballot images and/or precinct totals"]
  ->("Wrap up voting (central)" *w)
  ->[Counts state=certified]
  ->("Wrap up election")
  -><*merge>.


// Diagram:  Prepare for election
// Output:  ["Equipment, voter lists, ballot styles and/or ballots"]

<InitialNode>
  -><ForkNode>{
    ->("Define precincts") // This action refers to configuring the
    // voting system to realize the precincts as defined by state law.
      ->["Precinct definitions"]
      -><ForkNode>{
        ->("Train poll workers")
          -><FlowFinal>,
        ->("Register voters")
          ->["Voter lists"]
          ->(Collect *c1),
        ->("Program election")
          ->["Election definition"]
          ->("Prepare ballots")
          ->["Ballot styles"]
          -><ForkNode>{
            ->(*c1),
            "Centrally programmed ballot styles"
              ->["Ballot styles"]
              ->0..1("Configure & calibrate precinct equipment (central)" *cc)
          }
      },
    ->("Maintain equipment in storage")
      ->[Equipment state=old]
      ->(*cc),
    "Need new equipment"
      ->("Procure equipment")
      ->[Equipment state=new]
      ->0..1(*cc)
  };
(*c1)
  ->["Voter lists, ballot styles"]
  -><ForkNode>{
    ->("Educate / notify / inform voters")
      -><FlowFinal>,
    ->(Collect *c2),
    "Paper ballots"
      ->("Produce ballots")
      ->[Ballots]
      ->0..1(*c2)
  };
(*cc)
  ->[Equipment state=configured]
  ->("Test precinct equipment (central)")
  ->[Equipment state=tested]
  ->("Transport equipment")
  ->[Equipment state=deployed]
  ->(Collect *c2)
  ->["Equipment, voter lists, ballot styles and/or ballots"].


// Diagram:  Gather in-person vote (paper-based).
//
// This diagram is divided to show which actions are done by the voter
// and which are done by the poll worker or election judge.  The action
// Spoil ballot may be done by either.  Present credentials, Mark ballot,
// Review ballot, and Present / submit ballot are done by the voter.  All
// others are done by the poll worker or election judge.
//
// Note:  This activity occurs once per voter.
//
// Input:  ["Voter lists"]
// Output:  [Ballot state=accepted]

["Voter lists"]
  ->("Check identity of voter" *check);
<InitialNode>
  ->("Present credentials")
  ->("Check identity of voter" *check)
  ->("Check voter eligibility")
  -><MergeNode *merge>
  ->("Update poll book")
  ->("Issue ballot or provisional ballot")
  ->("Provide private voting station")
  ->[Ballot state=blank]
  ->("Mark ballot")
  -><DecisionNode>{
    "Fled voter"
      ->("Handle abandoned ballot")
      -><ActivityFinal>,
    else
      ->("Review ballot")
      -><DecisionNode>{
        "Not OK"
          ->("Spoil ballot")
          -><*merge>,
        OK
          ->("Present / submit ballot")
          ->[Ballot state=completed]
          ->("Validate ballot")
          -><DecisionNode>{
            OK
              ->("Accept ballot")
              ->[Ballot state=accepted],
            "Not OK"
              ->("Spoil ballot")
              -><DecisionNode>{
                "Try again"
                  -><*merge>,
                else
                  -><ActivityFinal>
              }
          }
      }
  }.


// Diagram:  Gather in-person vote (DRE).
//
// This diagram is divided to show which actions are done by the voter
// and which are done by the poll worker or election judge.  Present
// credentials, Mark ballot, Review ballot, Correct ballot, and Cast
// ballot are done by the voter.  All others are done by the poll worker
// or election judge.
//
// Note:  This activity occurs once per voter.
//
// Input:  ["Voter lists"]
// Output:  ["Ballot image"]

["Voter lists"]
  ->("Check identity of voter" *check);
<InitialNode>
  ->("Present credentials")
  ->("Check identity of voter" *check)
  ->("Check voter eligibility")
  ->("Update poll book")
  ->("Provide private voting station")
  ->("Mark ballot")
  -><MergeNode *merge>
  -><DecisionNode>{
    "Fled voter"
      ->("Handle abandoned ballot")
      -><ActivityFinal>,
    else
      ->("Review ballot")
      -><DecisionNode>{
        "Not OK"
          ->("Correct ballot")
          -><*merge>,
        OK
          ->("Cast ballot")
          ->["Ballot image"]
      }
  }.


// Diagram:  Wrap up voting (precinct)
//
// Note:  This activity occurs once per precinct.  Absentee / remote
// ballots may be handled and processed as a separate precinct under this
// activity.
//
// Input:  ["Ballots, ballot images and/or machine totals"]
// Outputs:  [Reports], ["Ballots, ballot images and/or precinct totals" state=validated]

["Ballots, ballot images and/or machine totals"]
  ->("Close polls (including absentee / remote voting)"){
    ->[Reports],
    ->["Ballots, ballot images and/or precinct totals" state=unvalidated]
    -><MergeNode *merge>
    ->("Validate counts (precinct)")
    -><DecisionNode>{
      Invalid
        ->("Diagnose and correct problem (precinct)")
        ->["Ballots, ballot images and/or precinct totals" state="corrected, unvalidated"]
        -><*merge>,
      else
        ->["Ballots, ballot images and/or precinct totals" state=validated]
        ->("Deliver / transmit ballots, ballot images and/or precinct totals to central")
        ->["Ballots, ballot images and/or precinct totals" state=validated]
    }	
  }.


// Diagram:  Wrap up voting (central)
//
// Input:  ["Ballots, ballot images and/or precinct totals" state=validated]
// Outputs:  [Counts state=certified], [Reports state=official]

["Ballots, ballot images and/or precinct totals" state=validated]
  -><MergeNode *merge1>
  ->("Count (central)") // Including absentee and write-ins.
  ->[Counts state=unvalidated]
  -><MergeNode *merge2>
  ->("Validate counts (central)")
  -><DecisionNode>{
    Invalid
      ->("Diagnose and correct problem (central)")
      ->[Counts state="corrected, unvalidated"]
      -><*merge2>,
    else
      ->[Counts state=validated]
      ->("Generate unofficial reports")
      ->[Reports state=unofficial]
      ->("Reconcile provisional/challenged ballots and ballots with write-ins")
      ->[Counts state=adjusted]
      ->("Generate official reports")
      ->[Reports state=official]
      -><DecisionNode>{
        Recount
          ->("Retrieve original data")
          ->["Ballots, ballot images and/or precinct totals" state=validated]
          -><*merge1>,
        else
          ->("Certify final counts"){
            ->[Counts state=certified],
            ->[Reports state=official]
          }
      }
  }.


// Diagram:  Audit / observe elections

<InitialNode>{
  ->("Involve independent observers"),
  ->("Conduct official audits"),
  ->("Conduct personnel checks"),
  ->("Conduct equipment checks"),
  ->("Conduct procedural checks")
}.


// Diagram:  Prepare ballots
//
// Note:  Produce ballots is analogous.
//
// Input:  ["Election definition"]
// Output:  ["Ballot styles"]

["Election definition"]
  -><ForkNode>{
    ->("Define regular ballots")
      -><JoinNode *j>,
    ->("Define provisional ballots")
      -><*j>,
    ->("Define absentee / remote ballots")
      -><*j>
  };
<*j>
  ->["Ballot styles"].


// Diagram:  Procure equipment
//
// Output:  [Equipment]

<InitialNode>
  ->("Specify requirements")
  ->("Select manufacturers and equipment")
  ->("Conduct certification testing")
  ->("Conduct acceptance testing")
  ->[Equipment].


// Diagram:  Prepare for voting (precinct)
//
// Note:  This activity occurs once per precinct.
//
// Input:  [Equipment]
// Output:  [Reports]

[Equipment]
  ->("Set up polling place")
  ->("Set up precinct equipment (precinct)")
  ->("Configure & calibrate precinct equipment (precinct)")
  ->("Test precinct equipment (precinct)")
  ->("Open poll")
  ->[Reports].


// Diagram:  Prepare for voting (central)
//
// Input:  [Equipment]
// Output:  [Reports]

[Equipment]
  ->("Set up central equipment (central)")
  ->("Configure & calibrate central equipment (central)")
  ->("Test central equipment (central)")
  ->[Reports].


// Diagram:  Register voters
//
// Input:  ["Registration database" state=original]
// Output:  ["Voter lists"]

["Registration database" state=original]
  -><ForkNode>{
    ->("Register new voters")
      -><JoinNode *j>,
    ->("Update voter information")
      -><*j>,
    ->("Purge ineligible, inactive, or dead voters")
      -><*j>
  };
<*j>
  ->["Registration database" state=updated]
  ->("Generate voter lists")
  ->["Voter lists"].


// Diagram:  Wrap up election

<InitialNode>
  -><ForkNode>{
    ->("Deactivate equipment")
      -><JoinNode *j>,
    ->("Conduct post-mortem")
      -><*j>
  };
<*j>
  -><ActivityFinal>.


// Diagram:  Top level

<InitialNode>
  -><ForkNode>{
    ->("Administer elections"),
    ->("Audit / observe elections"),
    ->(Archive) // All of the reports that are generated by various
                // actions are archived.
  }.


// Diagram:  Deactivate equipment

<InitialNode>
  ->("Pack up equipment")
  ->("Transport equipment")
  ->("Put equipment in storage")
  -><ActivityFinal>.


// Diagram:  Conduct post-mortem

<InitialNode>
  ->("Analyze election results")
  ->["Lessons learned"]
  ->("Refine needs and requirements")
  ->("Make revisions / changes to existing hardware, software, processes, procedures, and testing")
  -><ActivityFinal>.
Leave a
Comment

8.2 Vote-Capture Device State Model (informative)

The state model shown in Part 1 :Figure 8-9 clarifies the relationship between the different equipment states that result from the opening and closing of polls and the suspension and resumption of voting in jurisdictions that allow early voting.

Figure 8-9 Vote-capture device states

Vote-capture device states

The many steps that occur prior to the opening of polls are abstracted by the Pre-voting state. The many steps that occur after the close of polls are abstracted by the Post-voting state. Between these is a composite state Open, which contains the simple state Suspended and the composite state Activated. Activated in turn contains the simple states Ready and In use.

Upon the opening of polls, the vote-capture device transitions from the Pre-voting state to the Ready state (and, consequently, also to the Open and Activated composite states that contain it). From Ready it can transition to the In use state upon the activation of a ballot and return to the Ready state when that ballot is printed, cast or spoiled (the details depend on the technology in use). From Ready it can also transition to the Suspended state when an election official suspends voting and return to the Ready state when voting is resumed. Finally, from Ready it can transition to the Post-voting state when polls are closed.

In conformance with Requirement Part 1: 7.6-B.5, there is no transition from Post-voting back to Open except by beginning an entirely new election cycle, which is not modeled here.

A voting session lasts while the device is in the In use state. An active period lasts while the device is in the Activated state.

 

8.3 Logic Model (normative)

This model defines the results that must appear in vote data reports and is used in verification of voting system logic. It does not address ranked order voting and does not attempt to define every voting variation that jurisdictions may use. It suffices for N-of-M (including 1-of-M) and cumulative voting.[10]

2 Comments

Comment by James Ronback (General Public)

The online definition link for "N-of-M" is broken in: 8.3 Logic Model (normative) This model defines the results that must appear in vote data reports and is used in verification of voting system logic. It does not address ranked order voting and does not attempt to define every voting variation that jurisdictions may use. It suffices for N-of-M (including 1-of-M) and cumulative voting.[10]

Comment by James Ronback (General Public)

It is not clear if "Approval Voting" is addressed by this standard. Approval Voting is a simple voting system with powerful benefits. Approval Voting allows you to vote for more than one candidate if you so choose. The winner is the candidate that collects the most votes. See: http://www.approvalvoting.org/

8.3.1 Domain of discourse

A noteworthy bound on the scope of the voting system, and hence the logic model, is that, as of the state of the practice in 2005, voting systems do not identify voters. Poll workers are responsible for maintaining the one voter, one ballot parity. The voting system is limited to handling ballots. Consequently, logic verification is limited to showing that those ballots are counted correctly.

Table 8-2 Terms used in logic verification

Term

Definition

A(t,v)

Boolean function, returns true if and only if ballot v conforms to jurisdiction-dependent criteria for accepting or rejecting entire ballots, such as stray marks policies and voter eligibility criteria, as of time t.  This value is false for provisional, challenged, and review-required ballots that are not [yet] validated, and for spoiled ballots.
The system may not be able to determine the value of A(t,v) without human input; however, it may assign tentative values according to local procedures and state law, to be corrected later if necessary by input from election workers.
The value of A(t,v) may change over time as a result of court decisions, registrar review of voter eligibility, etc.
In a paper-based system, A(t,v) will be false if ballot v is unprocessable. 

C(r,t)

The set of all contest choices for a contest r, including any write-ins appearing on ballots cast as of time t.  In systems conforming to the Write-ins class, each distinct write-in candidate appears separately in C(r,t).  Systems not conforming to the Write-ins class may nevertheless offer ballot positions for write-ins to be processed manually; in that case, C(r,t) contains entries corresponding to the anonymous write-in positions. 

c, cn, etc. 

Individual contest choices.

D(v)

The time at which ballot v is "done" (either cast or spoiled).  If a ballot is not "done" by the close of polls (e.g., an absentee ballot was never returned), it is effectively spoiled and called "done."

J

The set of reporting contexts (including tabulators, precincts, election districts, and system extent).

j, jn, etc.

Individual reporting contexts.

K(j,r,t)

For a given contest and reporting context, the number of read ballots for which A(t,v) is true as of time t (i.e., the number of ballots that should be counted). Ballot styles that do not include contest r do not contribute to this total.

LB

A limit on the number of ballots or ballot images that a tabulator is claimed to be capable of processing correctly. (Non-tabulating devices like EBMs have no such limit.)

LC

A limit on the number of ballot positions per contest that a voting device is claimed to be capable of processing correctly.  (See also LW)

LF

A limit on the number of ballot styles that a voting device is claimed to be capable of processing correctly.

LP

For paper-based tabulators, a limit on the ballot tabulation rate at which the device is claimed to be capable of operating correctly.

LR

A limit on the number of contests that a voting device is claimed to be capable of processing correctly.

LT

A numerical limit on vote totals that a tabulator is claimed to be capable of processing correctly.

LV

A limit on the number of provisional, challenged, or review-required ballots that a voting device is claimed to be capable of processing correctly.

LW

A limit on the total number of distinct contest choices per contest, including write-ins, that a voting device is claimed to be capable of processing correctly. LW ≥ LC. (See also LC)

N(r)

The maximum number of votes that may be cast by a given voter in contest r, pursuant to the definition of the contest. For N-of-M contests, this is the value N.

O(j,r,t)

For a given contest and reporting context, the number of overvotes in read ballots for which A(t,v) is true as of time t. Each ballot in which contest r is overvoted contributes N(r) to O(j,r,t).

R

The set of all contests.

r, rn, etc.

Individual contests in R.

S(c,r,t,v)

Ballot v's vote with respect to contest choice c in contest r as of time t. For checkboxes and the like, the value is 1 (selected) or 0 (not selected). For cumulative voting, the value is the number of votes that v gives to contest choice c in contest r. If the applicable ballot style does not include contest r, S(c,r,t,v) = 0.

S'(c,r,t,v)

Ballot v's vote with respect to contest choice c in contest r as accepted for counting purposes (i.e., valid votes only), as of time t.

S(r,t,v)

The total number of votes that ballot v has in contest r as of time t.
 total number of votes


T(c,j,r,t)

The vote total for contest choice c in contest r and reporting context j as of time t. This does not include votes that are invalid due to overvoting or votes from ballots for which A(t,v) is false.

t, tn, etc. 

Individual time points.

tO

The time at which polls are opened.

tC

The time at which polls are closed.

tE

The time at which the value of A(t,v) is frozen for all ballots, the counting is complete, and final vote totals are required ("end").

U(j,r,t)

For a given contest and reporting context, the number of undervotes in read ballots for which A(t,v) is true as of time t. A given ballot contributes at most N(r) to U(j,r,t). Ballot styles that do not include contest r do not contribute to this total.

V(j,t)

The set of all ballots that have been distributed to voters, enabled, activated or issued within reporting context j by time t, including any that are presently being voted. Absentee ballots, provisional/challenged ballots, and review-required ballots are included in V if and only if the system claims conformance to the relevant classes. Ballots containing write-in votes may be included for systems not conforming to the Write-ins class if the system reports all write-in votes as a single ballot position. For more information on this exception see C(r,t) and Part 1: 2.5.3.1 "Supported voting variations (system-level)".

v, vn, etc. 

Individual ballots in V(j,t). 

Ballot styles, which determine which contests appear on a given ballot, are factored out of this model. They impact it only indirectly—see the definitions of K(j,r,t), S(c,r,t,v), and U(j,r,t).

 

3 Comments

Comment by Carolyn Coggins, Kevin Wilson, Gail Audette (Voting System Test Laboratory)

For whom is this section effective? Based upon the introduction of section 8.1.1 this entire reference model is based on "a brief and incomplete guide". In addition for simplification "the following short cuts have been taken" those short cuts ignore the full voting process. As a result, this chapter is not useful; yet it is referred to through out the document. It adds incomplete, conflicting, and unproductive esoteric complexity to the entire VVSG. This approach is unworkable.

Comment by Kevin Wilson (Voting System Test Laboratory)

This section does not state the assumption that S(c,r,t,v) represents voter intent.

Comment by Kevin Wilson (Voting System Test Laboratory)

This section violates the previous EAC standards in that it uses variables which are not descriptive and duplicate. S and S' differ by only one character and S(r,t,v) is different from S(c,r,t,v). The use of S in S(c,r,t,v) is not understood since this does not appear to be a sum (perhaps a state?)

8.3.2 General constraints

Invariants:

invariant 1

invariant 2

invariant 3

The following formalize several basic integrity constraints. Each textual description is intended to elucidate the formal constraint(s) that follow it. In case of discrepancy or confusion, the formal constraints are normative.

No ballots will be accepted before polls are opened or after polls have closed, or during the process of opening or closing the polls (N.B., in early voting, polls are considered open when vote collection begins; see Part 1: 8.2 "Vote-Capture Device State Model (informative)".):

no
ballots accepted

No votes will be counted until after polls are opened:

no
votes counted

All tallies must remain zero until after polls are opened:

all tallies must be zero

A CVR cannot change once the voting session for that ballot has ended:

CVR cannot change

 

8.3.3 Cumulative voting

All valid votes must be counted, and only valid votes may be counted:[11]

all
votes valid

The final vote totals must accurately reflect all valid votes and only valid votes:

final tallies reflect valid votes

The overvote and undervote totals must be correct:

undervotes and overvotes must be correct 1

undervotes and overvotes must be correct 2

Every vote must be accounted for:

every vote must be accounted for

Note that all of the above constraints are predicated by every vote must be accounted for. No assertion has been made regarding the correctness of pre-final reports. Since the transmission and processing of vote data are not instantaneous, the correctness of a pre-final report can only be judged relative to some viewpoint (e.g., a central counting site, using whatever vote data they happen to have received and processed).

1 Comment

Comment by Kevin Wilson (Voting System Test Laboratory)

There are no numbers on equations making it difficult to quote them. In the first equation in 8.3.3 it is unclear what operations are grouped. Presumably it is " … if ( ( S(r,D(v),v) .lte. N(r) ) ^ A(t,v) )

8.3.4 N-of-M contests (including 1-of-M)

N-of-M is identical to cumulative voting but for the addition of the following invariant, which reflects the design of a ballot style that allows only one vote in each ballot position (equivalent to a checkbox). In systems conforming to the Write-ins class, this property must be preserved through the reconciliation of aliases and double votes (Requirement Part 1: 7.7.2-A.9).

N of M invariant