Merge branch 'simulator' into v2.1

haslab · Sep 25, 2020 · f73c3ce · f73c3ce
2 parents a2cf68e + 228d43e
commit f73c3ce
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java
@@ -1443,6 +1443,7 @@ private Runner doExportXml() {
     }
 
     // [HASLab]
+    // reuses the Pardinus instance to formula translation, so needs some tweaks to the Alloy level
     private Runner doExportLTL() {
         if (wrap)
             return wrapMe();
@@ -1455,7 +1456,7 @@ private Runner doExportLTL() {
                 rels = rels.and(r.eq(r));
         Formula form = null;
         Map<Object,Expression> reifs = new HashMap<Object,Expression>();
-        form = inst.formulate(new HashMap<Object,Expression>(), rels, true, new PardinusBounds(inst.state(0).universe()));
+        form = inst.formulate(reifs, rels, true, new PardinusBounds(inst.state(0).universe()), false);
         Expression unvs = Expression.UNIV;
         for (int i = 1; i < inst.prefixLength(); i++)
             unvs = Expression.UNIV.union(unvs.prime());
@@ -1481,7 +1482,7 @@ public Expression visit(Variable v) {
 
         };
         form = form.accept(repls);
-        OurDialog.showtext("Text Viewer", PrettyPrinter.print(form, 4).replaceFirst("some", "some disj"));
+        OurDialog.showtext("Text Viewer", PrettyPrinter.print(form, 4).replaceAll("Int\\[(-?\\d*)\\]", "$1").replaceFirst("some", "some disj"));
         return null;
     }