Merge branch 'electrod-ints'

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/DotColor.java

@@ -34,29 +34,29 @@
 public enum DotColor {
 
                       MAGIC("Magic", "magic"),
-                      YELLOW("Yellow", "gold", "yellow", "lightgoldenrod", "yellow", "bright_yellow"),
+                      YELLOW("Yellow", "gold", "yellow", "lightgoldenrod", "yellow", "tol_light_yellow"),
                       GREEN(
                             "Green",
                             "limegreen",
                             "green2",
                             "darkolivegreen2",
                             "chartreuse2",
-                            "bright_green"),
+                            "tol_light_green"),
                       BLUE(
                            "Blue",
                            "cornflowerblue",
                            "blue",
                            "cadetblue",
                            "cyan",
-                           "bright_blue"),
+                           "tol_light_blue"),
                       RED(
                           "Red",
                           "palevioletred",
                           "red",
                           "salmon",
                           "magenta",
-                          "bright_red"),
-                      GRAY("Gray", "lightgray", "lightgray", "lightgray", "lightgray", "bright_gray"),
+                          "tol_light_red"),
+                      GRAY("Gray", "lightgray", "lightgray", "lightgray", "lightgray", "tol_light_gray"),
                       WHITE("White", "white"),
                       BLACK("Black", "black");
 
@@ -131,8 +131,8 @@ else if (name.equals("palevioletred"))
             ans = new Color(222, 113, 148);
         else if (name.equals("red"))
             ans = new Color(255, 0, 0);
-        else if (name.equals("bright_red"))
-            ans = new Color(238, 102, 119);
+        else if (name.equals("tol_light_red"))
+            ans = new Color(204, 102, 119);
         else if (name.equals("salmon"))
             ans = new Color(255, 130, 115);
         else if (name.equals("magenta"))
@@ -141,8 +141,8 @@ else if (name.equals("limegreen"))
             ans = new Color(49, 207, 49);
         else if (name.equals("green2"))
             ans = new Color(0, 239, 0);
-        else if (name.equals("bright_green"))
-            ans = new Color(34, 136, 51);
+        else if (name.equals("tol_light_green"))
+            ans = new Color(170, 170, 0);
         else if (name.equals("darkolivegreen2"))
             ans = new Color(189, 239, 107);
         else if (name.equals("chartreuse2"))
@@ -151,24 +151,24 @@ else if (name.equals("gold"))
             ans = new Color(255, 215, 0);
         else if (name.equals("yellow"))
             ans = new Color(255, 255, 0);
-        else if (name.equals("bright_yellow"))
-            ans = new Color(204, 187, 68);
+        else if (name.equals("tol_light_yellow"))
+            ans = new Color(238, 221, 136);
         else if (name.equals("lightgoldenrod"))
             ans = new Color(239, 223, 132);
         else if (name.equals("cornflowerblue"))
             ans = new Color(99, 150, 239);
         else if (name.equals("blue"))
             ans = new Color(0, 0, 255);
-        else if (name.equals("bright_blue"))
-            ans = new Color(68, 119, 170);
+        else if (name.equals("tol_light_blue"))
+            ans = new Color(119, 170, 221);
         else if (name.equals("cadetblue"))
             ans = new Color(90, 158, 165);
         else if (name.equals("cyan"))
             ans = new Color(0, 255, 255);
         else if (name.equals("lightgray"))
             ans = new Color(214, 214, 214);
-        else if (name.equals("bright_gray"))
-            ans = new Color(187, 187, 187);
+        else if (name.equals("tol_light_gray"))
+            ans = new Color(221, 221, 221);
         else if (name.equals("white"))
             ans = Color.WHITE;
         else

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4graph/DotPalette.java

@@ -34,7 +34,7 @@ public enum DotPalette {
                         /** Neon palette. */
                         NEON("Neon"),
                         /** Color-blind palette. */
-                        BRIGHT("Bright");
+                        TOL_LIGHT("Tol");
 
     /** The text to display. */
     private final String displayText;

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticGraphMaker.java

@@ -115,7 +115,7 @@ public static JPanel produceGraph(JFrame parent, AlloyInstance instance, VizStat
     private static final List<Color> colorsNeon     = Util.asList(new Color(231, 41, 138), new Color(217, 95, 2), new Color(166, 118, 29), new Color(102, 166, 30), new Color(27, 158, 119), new Color(117, 112, 179));
 
     /** The list of colors, in order, to assign each legend. */
-    private static final List<Color> colorsColorBlind = Util.asList(new Color(68, 119, 170), new Color(102, 204, 238), new Color(34, 136, 51), new Color(204, 187, 68), new Color(238, 102, 119), new Color(170, 51, 119), new Color(187, 187, 187));
+    private static final List<Color> colorsColorBlind = Util.asList(new Color(119, 170, 221), new Color(153, 221, 255), new Color(187, 204, 51), new Color(170, 170, 0), new Color(238, 136, 102), new Color(255, 170, 187), new Color(221, 221, 221));
 
     private List<Color> getColors(DotPalette palette) {
         List<Color> colors;
@@ -125,7 +125,7 @@ else if (palette == DotPalette.STANDARD)
             colors = colorsStandard;
         else if (palette == DotPalette.MARTHA)
             colors = colorsMartha;
-        else if (palette == DotPalette.BRIGHT)
+        else if (palette == DotPalette.TOL_LIGHT)
             colors = colorsColorBlind;
         else
             colors = colorsNeon;

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java

@@ -156,6 +156,7 @@ private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, boolea
      * Create a new AlloyRelation whose label is unambiguous with any existing one.
      */
     private AlloyRelation makeRel(String label, boolean isPrivate, boolean isMeta, boolean isVar, boolean isSkolem, List<AlloyType> types) {
+        label = Util.tail(label);
         while (label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label))
             label = label + "'";
         while (true) {

org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/Util.java

@@ -821,7 +821,13 @@ public static boolean onMac() {
     /** Returns the substring after the last "/" */
     public static String tail(String string) {
         int i = string.lastIndexOf('/');
-        return (i < 0) ? string : string.substring(i + 1);
+        String label = (i < 0) ? string : string.substring(i + 1);
+        return string.charAt(0) == '$' && label.charAt(0) != '$' ? "$" + label : label;
+    }
+
+    /** Returns the substring without "this/". May not start with "this/" in skolems. */
+    public static String tailThis(String string) {
+        return string.replace("this/","");
     }
 
     /** Returns the substring without "this/". May not start with "this/" in skolems. */

org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java

@@ -419,7 +419,7 @@ public final class A4Solution {
         solver_opts.setCoreGranularity(opt.coreGranularity);
         solver_opts.setSymmetryBreaking(sym);
         solver_opts.setSkolemDepth(opt.skolemDepth);
-        solver_opts.setBitwidth(bitwidth > 0 ? bitwidth : (int) Math.ceil(Math.log(atoms.size())) + 1);
+        solver_opts.setBitwidth(bitwidth > 0 ? bitwidth : (int) Math.ceil(Math.log(atoms.size()+1) / Math.log(2)) + 1);
         solver_opts.setIntEncoding(Options.IntEncoding.TWOSCOMPLEMENT);
 
         solver_opts.setSolver(opt.solver.doOptions(solver_opts));
@@ -1556,7 +1556,7 @@ A4Solution solve(final A4Reporter rep, Command cmd, Simplifier simp, boolean try
         rep.debug("Simplifying the bounds...\n");
         if (opt.inferPartialInstance && simp != null && formulas.size() > 0 && !simp.simplify(rep, this, formulas))
             addFormula(Formula.FALSE, Pos.UNKNOWN);
-        rep.translate(opt.solver.id(), bitwidth, maxseq, mintrace, maxtrace, solver.options().skolemDepth(), solver.options().symmetryBreaking(), A4Preferences.Decompose.values()[opt.decompose_mode].toString());
+        rep.translate(opt.solver.id(), solver.options().bitwidth(), maxseq, mintrace, maxtrace, solver.options().skolemDepth(), solver.options().symmetryBreaking(), A4Preferences.Decompose.values()[opt.decompose_mode].toString());
         fgoal = Formula.and(formulas);
         rep.debug("Generating the solution...\n");
         kEnumerator = null;

org.alloytools.pardinus.core/bnd.bnd

@@ -5,4 +5,8 @@
 	org.sat4j.core,\
 	aQute.libg
 
+-testpath: \
+	biz.aQute.wrapper.junit,\
+	biz.aQute.wrapper.hamcrest
+
 Export-Package kodkod.*

org.alloytools.pardinus.core/src/main/java/kodkod/engine/PardinusSolver.java

@@ -134,9 +134,6 @@ private AbstractSolver<PardinusBounds,ExtendedOptions> solver() {
 		if (options.unbounded() && !options.solver().unbounded())
 			throw new InvalidSolverParamException("Bounded engines do not support complete model checking.");
 
-		if (!options.temporal() && options.solver().unbounded())
-			throw new InvalidSolverParamException("Unbounded engines do not support static models.");
-
 		if (options.decomposed()) {
 
 			if (options.temporal()) {
@@ -154,8 +151,8 @@ private AbstractSolver<PardinusBounds,ExtendedOptions> solver() {
 			if (options.temporal()) {
 				return getTemporalSolver(options);
 			} else {
-				ExtendedSolver solver = new ExtendedSolver(options);
-				return solver;				
+				return getStaticSolver(options);
+
 			}
 
 		}
@@ -164,12 +161,20 @@ private AbstractSolver<PardinusBounds,ExtendedOptions> solver() {
 
 	private TemporalSolver<ExtendedOptions> getTemporalSolver(ExtendedOptions options) {
 		SATFactory s = options.solver();
-		if ( s instanceof TemporalSolverFactory) {
+		if (s instanceof TemporalSolverFactory) {
 			return ((TemporalSolverFactory)s).getTemporalSolver(options);
 		} else
 			return new TemporalPardinusSolver(options);
 	}
 
+	private AbstractSolver<PardinusBounds,ExtendedOptions> getStaticSolver(ExtendedOptions options) {
+		SATFactory s = options.solver();
+		if (s instanceof TemporalSolverFactory) {
+			return StaticWrapper.wrap((TemporalSolverFactory) s, options);
+		} else
+			return new ExtendedSolver(options);
+	}
+
 	/**
 	 * {@inheritDoc}
 	 */

org.alloytools.pardinus.core/src/main/java/kodkod/engine/StaticWrapper.java

@@ -0,0 +1,27 @@
+package kodkod.engine;
+
+import kodkod.ast.Formula;
+import kodkod.engine.config.ExtendedOptions;
+import kodkod.engine.satlab.SATFactory;
+import kodkod.instance.PardinusBounds;
+import kodkod.solvers.api.TemporalSolverFactory;
+
+public class StaticWrapper {
+    public static AbstractSolver wrap(TemporalSolverFactory temporalFactory, ExtendedOptions options) {
+        options.setMinTraceLength(1);
+        options.setMaxTraceLength(1);
+        options.setRunTemporal(true);
+        TemporalSolver<ExtendedOptions> temporalSolver = temporalFactory.getTemporalSolver(options);
+        return new AbstractSolver<PardinusBounds, ExtendedOptions>() {
+            @Override
+            public ExtendedOptions options() {
+                return temporalSolver.options();
+            }
+
+            @Override
+            public Solution solve(Formula formula, PardinusBounds bounds) {
+                return temporalSolver.solve(formula, bounds);
+            }
+        };
+    }
+}

org.alloytools.pardinus.native/bnd.bnd

@@ -1,6 +1,11 @@
 -includeresource \
     native=native, \
     LICENSES=LICENSES
+
 -buildpath: \
 	org.alloytools.pardinus.core,\
-	biz.aQute.bnd.annotation
+	biz.aQute.bnd.annotation
+
+-testpath: \
+	biz.aQute.wrapper.junit,\
+	biz.aQute.wrapper.hamcrest