Merge branch 'heads/v2.1'

Author: nmacedo

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java

@@ -96,6 +96,8 @@ public class PreferencesDialog extends JFrame {
     // private JPanel solverPane;
     // private JPanel miscPane;
 
+    final static boolean isDebug = "yes".equals(System.getProperty("debug"));
+
     private static class MyIntSpinnerModel extends AbstractSpinnerModel {
 
         private final IntPref pref;
@@ -338,7 +340,7 @@ private static boolean staticLibrary(String name) {
         for (int i = dirs.length - 1; i >= 0; i--) {
             final File file = new File(dirs[i] + File.separator + name);
             if (file.canExecute()) {
-                if ("yes".equals(System.getProperty("debug")))
+                if (isDebug)
                     System.out.println("Loaded: " + name + " at " + file);
                 return true;
             }
@@ -347,13 +349,13 @@ private static boolean staticLibrary(String name) {
         for (String str : (System.getenv("PATH")).split(Pattern.quote(File.pathSeparator))) {
             Path pth = Paths.get(str);
             if (Files.exists(pth.resolve(name))) {
-                if ("yes".equals(System.getProperty("debug")))
+                if (isDebug)
                     System.out.println("Loaded: " + name + " at " + pth);
                 return true;
             }
         }
 
-        if ("yes".equals(System.getProperty("debug")))
+        if (isDebug)
             System.out.println("Failed to load: " + name);
         return false;
     }
@@ -362,7 +364,7 @@ private static boolean staticLibrary(String name) {
     private static boolean loadLibrary(String library) {
         boolean loaded = _loadLibrary(library);
         String libName = System.mapLibraryName(library);
-        if ("yes".equals(System.getProperty("debug")))
+        if (isDebug)
             if (loaded)
                 System.out.println("Loaded: " + libName);
             else

org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java

@@ -381,6 +381,7 @@ public void debug(final String msg) {
     @Override
     public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
         startTime = System.currentTimeMillis();
+        startCount = 0;
         cb("translate", "Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + (skolemDepth == 0 ? "" : " SkolemDepth=" + skolemDepth) + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
     }
 

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

@@ -28,8 +28,6 @@
 import java.io.PrintStream;
 import java.io.Serializable;
 import java.lang.Thread.UncaughtExceptionHandler;
-import java.lang.reflect.Field;
-import java.util.Locale;
 
 import org.alloytools.alloy.core.AlloyCore;
 
@@ -185,16 +183,22 @@ public static void stop() {
         synchronized (WorkerEngine.class) {
             try {
                 if (latest_sub != null) {
-                    if (!System.getProperty("os.name").toLowerCase(Locale.US).startsWith("windows"))
-                        try {  // [electrod] needed to stop all child processes (electrod)
-                            Field f = latest_sub.getClass().getDeclaredField("pid");
-                            f.setAccessible(true);
-                            Runtime.getRuntime().exec("kill -SIGTERM " + f.get(latest_sub));
-                        } catch (NoSuchFieldException | SecurityException | IllegalArgumentException | IllegalAccessException | IOException e) {
-                            e.printStackTrace();
-                        }
-                    else
-                        latest_sub.destroy();
+                    // [electrum] this replaces the currently WorkerTask so that it exits gracefully
+                    try {
+                        ObjectOutputStream main2sub = new ObjectOutputStream(wrap(latest_sub.getOutputStream()));
+                        main2sub.writeObject(new WorkerTask() {
+
+                            private static final long serialVersionUID = 1L;
+
+                            @Override
+                            public void run(WorkerCallback out) throws Exception {
+                            }
+                        });
+                        main2sub.close();
+                    } catch (IOException e) {
+                    }
+
+                    latest_sub.destroy();
                 }
             } finally {
                 latest_manager = null;

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

@@ -90,6 +90,7 @@
 import kodkod.engine.PardinusSolver;
 import kodkod.engine.Proof;
 import kodkod.engine.Solution;
+import kodkod.engine.config.AbstractReporter;
 import kodkod.engine.config.DecomposedOptions.DMode;
 import kodkod.engine.config.ExtendedOptions;
 import kodkod.engine.config.Options;
@@ -863,7 +864,10 @@ Expression a2k(Expr expr) throws ErrorFatal {
      * given expression.
      */
     TupleSet approximate(Expression expression) {
-        return factory.setOf(expression.arity(), Translator.approximate(expression, bounds, solver.options()).denseIndices());
+        PardinusBounds b = bounds.clone();
+        b.resolve(new AbstractReporter() {
+        });
+        return factory.setOf(expression.arity(), Translator.approximate(expression, b, solver.options()).denseIndices());
     }
 
     /**
@@ -880,6 +884,8 @@ TupleSet query(boolean findUpper, Expression expr, boolean makeMutable) throws E
         if (expr == KK_STRING)
             return makeMutable ? stringBounds.clone() : stringBounds;
         if (expr instanceof Relation) {
+            if (bounds.lowerSymbBound((Relation) expr) != null)
+                return query(findUpper, findUpper ? bounds.upperSymbBound((Relation) expr) : bounds.lowerSymbBound((Relation) expr), makeMutable);
             TupleSet ans = findUpper ? bounds.upperBound((Relation) expr) : bounds.lowerBound((Relation) expr);
             if (ans != null)
                 return makeMutable ? ans.clone() : ans;