package election.tally;

/**
 * Decisions taken during the counting of ballots.
 * 
 * @design It is necessary to be able to record any decision which might
 *         influence the order in which votes are counted or transfered.
 * @author Dermot Cochran
 * @copyright 2005-2009 Dermot Cochran
 */
public class Decision extends DecisionStatus {

  /**
   * Maximum number of decision points
   */
  public static final int MAX_DECISIONS = 100;

  /** Type of decision taken */
  /*@ public invariant (decisionTaken == DecisionStatus.EXCLUDE)
    @   || (decisionTaken == DecisionStatus.NO_DECISION)
    @   || (decisionTaken == DecisionStatus.DEEM_ELECTED);
    @ public constraint (\old(decisionTaken) != DecisionStatus.NO_DECISION) ==>
    @   decisionTaken == \old(decisionTaken);
    @*/
  public byte             decisionTaken;

  /** Candidate to which the decision applied */
  /*@ public invariant (candidateID != Ballot.NONTRANSFERABLE) 
    @   || (candidateID == Candidate.NO_CANDIDATE);
    @ public constraint (decisionTaken != DecisionStatus.NO_DECISION) ==>
    @   candidateID == \old(candidateID);
    @*/
  public long             candidateID;

  /** Round of counting at which decision was taken */
  //@ public invariant 0 <= atCountNumber;
  /*@ public constraint (decisionTaken != DecisionStatus.NO_DECISION) ==>
    @   atCountNumber == \old(atCountNumber);
    @*/
  public long             atCountNumber;

  /**
   * Create a new decision event.
   * 
   * @param decisionType
   *        Type of decision made e.g. elect or eliminate
   * @param candidateIDValue
   *        ID of the candidate in question
   * @param countNumberValue
   *        Count number in which the decision was made
   */
  /*@ public normal_behavior
    @   requires (decisionType == DecisionStatus.EXCLUDE) ||
    @            (decisionType == DecisionStatus.DEEM_ELECTED);
    @   requires 0 <= countNumberValue;
    @   requires candidateID != Candidate.NO_CANDIDATE;
    @   requires candidateID != Ballot.NONTRANSFERABLE;
    @   assignable decisionTaken, atCountNumber, candidateID;
    @   ensures decisionTaken == decisionType;
    @   ensures atCountNumber == countNumberValue;
    @   ensures candidateID == candidateIDValue;
    @*/
  public Decision(final int countNumberValue, final int candidateIDValue,
      final byte decisionType) {
    super();
    decisionTaken = decisionType;
    atCountNumber = countNumberValue;
    candidateID = candidateIDValue;
    /*@ assert (decisionTaken == DecisionStatus.EXCLUDE) ||
      @        (decisionTaken == DecisionStatus.DEEM_ELECTED);
      @*/
  }

  /*@ assignable decisionTaken, atCountNumber, candidateID;
    @*/
  public Decision() {
    super();
    atCountNumber = 0;
    candidateID = Candidate.NO_CANDIDATE;
    decisionTaken = DecisionStatus.NO_DECISION;
  }
}

@@ -792,32 +792,43 @@
 /%0A  
+protected /*@ spec_
 public
+ @*/
  byte 
-            
 deci
@@ -1131,38 +1131,49 @@
  @*/%0A  p
-ublic long            
+rotected/*@ spec_public @*/  long
  candida
@@ -1276,25 +1276,25 @@
 tNumber;%0A  /
-*
+/
 @ public con
@@ -1305,66 +1305,13 @@
 int 
-(decisionTaken != DecisionStatus.NO_DECISION) ==%3E%0A    @   
+%5Cold(
 atCo
@@ -1319,25 +1319,21 @@
 ntNumber
- == %5Cold(
+) %3C= 
 atCountN
@@ -1341,44 +1341,47 @@
 mber
-)
 ;%0A  
-  @*/%0A  public long            
+protected /*@ spec_public @*/  long
  atC
@@ -2631,24 +2631,170 @@
 andidateID;%0A
+    @ ensures atCountNumber == 0;%0A    @ ensures candidateID == Candidate.NO_CANDIDATE;%0A    @ ensures decisionTaken == DecisionStatus.NO_DECISION;%0A
     @*/%0A  pu

Clean up decision class, by making all fields protected and weakening one invariant.