Add -excel option

.classpath

@@ -4,5 +4,6 @@
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
 	<classpathentry kind="lib" path="dependencies/commons-cli-1.2.jar"/>
 	<classpathentry kind="lib" path="dependencies/antlr-runtime-4.0.jar"/>
+	<classpathentry kind="lib" path="dependencies/jxl.jar"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

src/jkind/ArgumentParser.java

@@ -8,6 +8,7 @@
 
 public class ArgumentParser {
 	final private static String BMC = "bmc";
+	final private static String EXCEL = "excel";
 	final private static String INDUCT_CEX = "induct_cex";
 	final private static String N = "n";
 	final private static String NO_INV_GEN = "no_inv_gen";
@@ -22,6 +23,7 @@ public class ArgumentParser {
 	private static Options getOptions() {
 		Options options = new Options();
 		options.addOption(BMC, false, "bounded model checking only (implies -" + NO_INV_GEN + ")");
+		options.addOption(EXCEL, false, "generate results in Excel format");
 		options.addOption(INDUCT_CEX, false, "generate inductive counterexamples");
 		options.addOption(N, true, "number of iterations (default 200)");
 		options.addOption(NO_INV_GEN, false, "disable invariant generation");
@@ -69,11 +71,20 @@ private static void setSettings(CommandLine line) {
 			System.exit(0);
 		}
 
+		if (line.hasOption(EXCEL) && line.hasOption(XML)) {
+			System.out.println("Error: only one output format may be selected");
+			System.exit(-1);
+		}
+
 		if (line.hasOption(BMC)) {
 			Settings.useInductiveProcess = false;
 			Settings.useInvariantProcess = false;
 		}
 
+		if (line.hasOption(EXCEL)) {
+			Settings.excel = true;
+		}
+
 		if (line.hasOption(INDUCT_CEX)) {
 			Settings.inductiveCounterexamples = true;
 		}

src/jkind/Settings.java

@@ -3,6 +3,7 @@
 public class Settings {
 	public static int n = 200;
 	public static int timeout = 100;
+	public static boolean excel = false;
 	public static boolean xml = false;
 	public static boolean scratch = false;
 	public static boolean useInductiveProcess = true;

src/jkind/processes/Director.java

@@ -1,6 +1,6 @@
 package jkind.processes;
 
-import java.io.FileNotFoundException;
+import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.HashMap;
@@ -20,6 +20,7 @@
 import jkind.solvers.Model;
 import jkind.translation.Specification;
 import jkind.writers.ConsoleWriter;
+import jkind.writers.ExcelWriter;
 import jkind.writers.Writer;
 import jkind.writers.XmlWriter;
 
@@ -49,14 +50,16 @@ public Director(Specification spec) {
 	}
 
 	private Writer getWriter(Specification spec) {
-		if (Settings.xml) {
-			try {
+		try {
+			if (Settings.excel) {
+				return new ExcelWriter(spec.filename + ".xls", spec.node);
+			} else if (Settings.xml) {
 				return new XmlWriter(spec.filename + ".xml", spec.typeMap);
-			} catch (FileNotFoundException e) {
-				throw new JKindException("Unable to open XML output file", e);
+			} else {
+				return new ConsoleWriter();
 			}
-		} else {
-			return new ConsoleWriter();
+		} catch (IOException e) {
+			throw new JKindException("Unable to open output file", e);
 		}
 	}
 

src/jkind/solvers/BoolValue.java

@@ -19,4 +19,26 @@ public boolean getBool() {
 	public String toString() {
 		return Boolean.toString(val);
 	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + (val ? 1231 : 1237);
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		BoolValue other = (BoolValue) obj;
+		if (val != other.val)
+			return false;
+		return true;
+	}
 }

src/jkind/solvers/NumericValue.java

@@ -12,4 +12,29 @@ public NumericValue(String val) {
 	public String toString() {
 		return val;
 	}
+
+	@Override
+	public int hashCode() {
+		final int prime = 31;
+		int result = 1;
+		result = prime * result + ((val == null) ? 0 : val.hashCode());
+		return result;
+	}
+
+	@Override
+	public boolean equals(Object obj) {
+		if (this == obj)
+			return true;
+		if (obj == null)
+			return false;
+		if (getClass() != obj.getClass())
+			return false;
+		NumericValue other = (NumericValue) obj;
+		if (val == null) {
+			if (other.val != null)
+				return false;
+		} else if (!val.equals(other.val))
+			return false;
+		return true;
+	}
 }