/* Sample solution to SE304 Lab 2
** Author: Margaret McGaley
** Ammended by: Gareth Carter
** Questions 2, 3, 4 & 5 can be found within
*/
package dbcvote;

import java.util.LinkedList;
import java.util.Arrays;

public class Vote {
       private /*@ spec_public non_null @*/LinkedList prefs;
       private /*@ spec_public @*/ LinkedList clean_prefs;

       /*@ invariant (\forall int i; i>=0 && i<prefs.size();
                             prefs.get(i) instanceof Preference); @*/

       /* Question 2a */
       /* (* We assume all elements of prefs are of type Preference and
             all Preferences only contain genuine Candidate names and
             there are no duplicate names in the Preference *) */

       /* Question 2b */
       /*@   requires
         @        (\forall int i; i>=0 && i<prefs.size();
         @            prefs.get(i) instanceof Preference)
         @       &
         @        (\forall int j; j>=0 && j<prefs.size();
         @            ElectionENV.isCandidate(((Preference)prefs.get(j)).getName()))
         @       &
         @        (\forall int k; k>=0 && k<prefs.size();
         @          !(\exists int l; l>k && l<prefs.size();
         @            ((Preference)prefs.get(k)).getName().equals(((Preference)prefs.get(l)).getName())));
         @   ensures this.prefs==prefs;
         @*/
       public Vote(/*@ non_null @*/ LinkedList prefs) {
              this.prefs = prefs;
       }


       /* Question 3a */
       /* (* If prefs represents no first vote or multiple first votes
                  throws a spoiled vote exception*)*/

       /* Question 3b */
       /*@   signals (SpoiledVoteException) !(\exists int i; i>=0 && i<prefs.size();
         @                                       ((Preference)prefs.get(i)).getPref()==1)||
         @                                   (\exists int j; j>=0 && j<prefs.size();
         @                                        !(\exists int k; k>j && k<prefs.size();
         @                                            (((Preference)prefs.get(j)).getPref()==1 &&
         @                                            ((Preference)prefs.get(k)).getPref()==1)));
         @   ensures (\forall int p ; p>=0 && p<=prefs.size();
         @                 clean_prefs.contains((Preference)(prefs.get(p))));
         @*/

       public void validateVote() throws SpoiledVoteException {
              Preference[] sorted = new Preference[prefs.size()];
              sorted = (Preference[]) prefs.toArray(sorted);

              Arrays.sort(sorted);
              clean_prefs = new LinkedList();
              int i;

              if (sorted[0].getPref() != 1) {
                  throw new SpoiledVoteException("No first preference");
              }

              for (i = 1; i < sorted.length; i++) {
                  if ( (sorted[i].compareTo(sorted[i - 1]) == 0)
                    || (sorted[i].getPref() > (sorted[i - 1].getPref() + 1)) ) {
                    i -= 1;
                    break;
                  }
              }

              if (i == 0) {
                  throw new SpoiledVoteException("Multiple first preferences");
              }

              for (int j = 0; j < i; j++) {
                  clean_prefs.add(sorted[j]);
              }
       }

       public /*@ pure non_null @*/String toString() {
              LinkedList out;
              if (clean_prefs != null) {
                 out = clean_prefs;
              }
              else {
                 out = prefs;
              }

              String out_string = new String();

              for (int i = 0; i < out.size(); i++) {
                  out_string += out.get(i).toString();
              }

              return out_string;
       }
}