/**
 * Dermot Cochran, 2010, IT University of Copenhagen
 * 
 * This class generates ballot boxes that fulfull a given scenario, by using
 * the Alloy Analayser API with a pre-defined model of PR-STV voting
 */

package ie.lero.evoting.test.data;

import ie.votail.model.Scenario;

import java.util.Map;
import java.util.logging.Logger;

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.SafeList;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Expr;
import edu.mit.csail.sdg.alloy4compiler.ast.ExprVar;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;
import edu.mit.csail.sdg.alloy4viz.VizGUI;
import election.tally.BallotBox;

public class BallotBoxGenerator {

  private static final int MAX_SCOPE = 0;
  protected Logger logger;
  protected A4Reporter reporter;
  protected Map<String, String> loaded;
  protected A4Options options;
  protected Module world;
  
  /**
   * Start the generation of ballot boxes and load the Alloy model
   * 
   * @param model_filename The name of the Alloy model file
   * @param log_filename The name of the log file
   */
  BallotBoxGenerator(String model_filename, String  log_filename) {
    reporter = new A4Reporter();
    loaded = null;
    options = new A4Options();
    options.solver = A4Options.SatSolver.SAT4J;
    logger = Logger.getLogger(log_filename);
    
    try {
      world = CompUtil.parseEverything_fromFile(reporter, loaded, 
        model_filename);
    } catch (Err e) {
      world = null;
      logger.severe("Unable to find model " + model_filename 
        + "because of " + e.msg);
    }
  }
    
  /**
   * Generate a ballot box from a scenario description, using Alloy model
   * 
   * @param scenario The scenario which will be tested by this ballot box
   * @param scope The scope for model finding in Alloy Analyser
   * 
   * @return The Ballot Box (or null if generation fails)
   */
  /*@
   * require loaded != null;
   */
  public BallotBox generateBallotBox (/*@ non_null @*/ Scenario scenario, 
    int scope) {

    Expr predicate;
    Command command;
    A4Solution solution;
    BallotBox ballotBox = null;
    
    // Find a ballot box which fulfills this scenario
    try {
        predicate = CompUtil.parseOneExpression_fromString(world, 
          scenario.toPredicate());
        command = new Command(false,scope,scope/2,scope,predicate);
        solution = TranslateAlloyToKodkod.execute_command(reporter, 
          world.getAllReachableSigs(), command, options);
        
        if (solution.satisfiable()) {
          ballotBox = extractBallotBox (solution);
          logger.info("Scenario " + scenario.toString() + " has ballot box " 
            + ballotBox.toString());
        }
        else if (scope < MAX_SCOPE) {
          ballotBox = generateBallotBox(scenario,scope+1);
        }
        else {
          ballotBox = new BallotBox();
          logger.severe("No ballot box found with scope " + MAX_SCOPE 
            + "for scenario " + scenario.toString());
        }
        
      } catch (Err e) {
        // Log failure to find scenario
        logger.severe("Unable to find ballot box for this scenario " 
          + scenario.toString() + " with scope " + scope + " because of "
          + e.msg);
      }
      return ballotBox;
    }

  /**
   * Extract ballots from the Alloy Analyser solution
   * 
   * @param solution The Alloy solution for a scenario
   * @return The Ballot Box
   */
  
  public BallotBox extractBallotBox(A4Solution solution) {
    BallotBox ballotBox = new BallotBox();
    
    SafeList<Sig> signatures = solution.getAllReachableSigs();
    // Iterate through the solution and add each ballot to the ballot box
    
    
    return ballotBox;
  }

    
}

@@ -711,16 +711,73 @@
 st.Sig;%0A
+import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig;%0A
 import e
@@ -1029,51 +1029,8 @@
 od;%0A
-import edu.mit.csail.sdg.alloy4viz.VizGUI;%0A
 impo
@@ -3972,14 +3972,8 @@
  sig
-nature
 s = 
@@ -4000,24 +4000,24 @@
 ableSigs();%0A
+
     // Itera
@@ -4078,20 +4078,171 @@
 lot box%0A
-
     
+for (Sig sig : sigs) %7B%0A      %0A      // Extract ballot preferences and assignees%0A      if (sig.label.equals(%22Ballot%22)) %7B%0A        %0A        %0A      %7D%0A    %7D
 %0A    %0A  

Identify ballot signatures in the solution