fixed bug where viz was still trace for static models

haslab · Apr 21, 2021 · 965c284 · 965c284
1 parent a85c1a8
commit 965c284
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java
@@ -118,7 +118,7 @@ public void bound(String msg) {
 
         @Override
         public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
-            debug("Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
+            debug("Solver=" + solver + (maxtrace < 1 ? "" : " Steps=" + mintrace + ".." + maxtrace) + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
         }
 
         @Override

diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleMain.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleMain.java
@@ -93,7 +93,7 @@ public void bound(String msg) {
 
         @Override
         public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
-            info("Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
+            info("Solver=" + solver + (maxtrace < 1 ? "" : " Steps=" + mintrace + ".." + maxtrace) + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
         }
 
         int totalVars = 0, totalPvars = 0, totalClauses = 0, lastStep = 0;

diff --git a/...oytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java b/...oytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
@@ -382,7 +382,7 @@ public void debug(final String msg) {
     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");
+        cb("translate", "Solver=" + solver + (maxtrace < 1 ? "" : " Steps=" + mintrace + ".." + maxtrace) + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + (skolemDepth == 0 ? "" : " SkolemDepth=" + skolemDepth) + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n");
     }
 
     /** {@inheritDoc} */

diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4SolutionReader.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4SolutionReader.java
@@ -432,7 +432,7 @@ private A4SolutionReader(Iterable<Sig> sigs, XMLNode xml) throws IOException, Er
                 A4Options opt = new A4Options();
                 opt.originalFilename = inst.getAttribute("filename");
                 // [electrum] do not use actual max trace, solution would identify unbounded solving but no unbounded solver
-                sol = new A4Solution(inst.getAttribute("command"), bitwidth, mintrace, tracelength, maxseq, strings, atoms, null, opt, 1);
+                sol = new A4Solution(inst.getAttribute("command"), bitwidth, Math.min(tracelength, mintrace), Math.min(tracelength, maxtrace), maxseq, strings, atoms, null, opt, 1);
                 factory = sol.getFactory();
                 // parse all the sigs, fields, and skolems
                 for (Map.Entry<String,XMLNode> e : nmap.entrySet())