Skip to content

Commit

Permalink
Merge branch 'simulator' into v2.1
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmacedo
nmacedo committed Oct 1, 2020
2 parents f73c3ce + 16be7ec commit dca5028
Show file tree
Hide file tree
Showing 3 changed files with 158 additions and 47 deletions.
198 changes: 151 additions & 47 deletions org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,11 @@
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.StringJoiner;
import java.util.prefs.Preferences;

import javax.swing.Box;
Expand Down Expand Up @@ -85,17 +85,13 @@
import edu.mit.csail.sdg.alloy4.Util;
import edu.mit.csail.sdg.alloy4.Version;
import edu.mit.csail.sdg.alloy4graph.GraphViewer;
import kodkod.ast.Decls;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.Node;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.ast.visitor.AbstractReplacer;
import kodkod.instance.PardinusBounds;
import kodkod.instance.TemporalInstance;
import kodkod.util.nodes.PrettyPrinter;
import edu.mit.csail.sdg.ast.Expr;
import edu.mit.csail.sdg.ast.ExprConstant;
import edu.mit.csail.sdg.ast.ExprVar;
import edu.mit.csail.sdg.ast.Sig;
import edu.mit.csail.sdg.translator.A4Solution;
import edu.mit.csail.sdg.translator.A4Tuple;
import edu.mit.csail.sdg.translator.A4TupleSet;

/**
* GUI main window for the visualizer.
Expand Down Expand Up @@ -141,7 +137,10 @@ public final class VizGUI implements ComponentListener {
private final JButton projectionButton, openSettingsButton, closeSettingsButton, magicLayout,
loadSettingsButton, saveSettingsButton, saveAsSettingsButton, resetSettingsButton, updateSettingsButton,
openEvaluatorButton, closeEvaluatorButton, enumerateButton, vizButton, treeButton,
txtButton, tableButton, leftNavButton, rightNavButton, cnfgButton, forkButton, initButton/* , dotButton, xmlButton */; // [HASLab]
txtButton, tableButton, leftNavButton, rightNavButton, cnfgButton, forkButton, initButton, pathButton/*
* , dotButton,
* xmlButton
*/; // [HASLab]

/**
* This list must contain all the display mode buttons (that is, vizButton,
Expand All @@ -158,15 +157,19 @@ public final class VizGUI implements ComponentListener {
/** The "show next" menu item. */
private final JMenuItem enumerateMenu;

/** The "fork next" menu item. */
/** The "fresh config" menu item. */
// [HASLab]
private final JMenuItem cnfgMenu;

/** The "fresh path" menu item. */
// [HASLab]
private final JMenuItem pathMenu;

/** The "fork next" menu item. */
// [HASLab]
private final JMenuItem forkMenu;

/** The "fork next" menu item. */
/** The "fork init" menu item. */
// [HASLab]
private final JMenuItem initMenu;

Expand All @@ -183,6 +186,9 @@ public final class VizGUI implements ComponentListener {
*/
private int settingsOpen = 0;

// [HASLab]
private boolean seg_iteration = false;

/**
* The current states and visualization settings; null if none is loaded.
*/
Expand Down Expand Up @@ -645,6 +651,7 @@ else if (height < 100)
JMenu instanceMenu = menu(mb, "&Instance", null);
enumerateMenu = menuItem(instanceMenu, "Show Next Solution", 'N', 'N', doNext());
cnfgMenu = menuItem(instanceMenu, "Show Fresh Configuration", 'C', 'C', doConfig()); // [HASLab]
pathMenu = menuItem(instanceMenu, "Show Fresh Path", 'P', 'P', doPath()); // [HASLab]
initMenu = menuItem(instanceMenu, "Show Fresh Initial State", 'I', 'I', doInit()); // [HASLab]
forkMenu = menuItem(instanceMenu, "Show Different Post-state", 'F', 'F', doFork()); // [HASLab]
leftNavMenu = menuItem(instanceMenu, "Show Previous State", KeyEvent.VK_LEFT, KeyEvent.VK_LEFT, leftNavListener); // [HASLab]
Expand Down Expand Up @@ -701,6 +708,7 @@ public void actionPerformed(ActionEvent e) {
toolbar.add(closeEvaluatorButton = OurUtil.button("Close Evaluator", "Close the evaluator", "images/24_settings_close2.gif", doCloseEvalPanel()));
toolbar.add(enumerateButton = OurUtil.button("Next", "Show a fresh solution", "images/24_history.gif", doNext()));
toolbar.add(cnfgButton = OurUtil.button("Fresh Config", "Show a fresh configuration", "images/24_history.gif", doConfig())); // [HASLab]
toolbar.add(pathButton = OurUtil.button("Fresh Path", "Show a fresh path", "images/24_history.gif", doPath())); // [HASLab]
toolbar.add(initButton = OurUtil.button("Fresh Init", "Show a fresh initial state", "images/24_history.gif", doInit())); // [HASLab]
toolbar.add(forkButton = OurUtil.button("Fork", "Show a different post-state", "images/24_history.gif", doFork())); // [HASLab]
toolbar.add(leftNavButton = OurUtil.button(new String(Character.toChars(0x2190)), "Show the previous state", "images/24_history.gif", leftNavListener));
Expand Down Expand Up @@ -876,6 +884,10 @@ private void updateDisplay() {
initMenu.setEnabled(!isMeta && settingsOpen == 0 && enumerator != null); // [HASLab]
initMenu.setVisible(isTrace); // [HASLab]
initButton.setVisible(!isMeta && settingsOpen == 0 && enumerator != null && isTrace); // [HASLab]
pathMenu.setEnabled(!isMeta && settingsOpen == 0 && enumerator != null && !seg_iteration); // [HASLab]
pathMenu.setVisible(isTrace); // [HASLab]
pathButton.setVisible(!isMeta && settingsOpen == 0 && enumerator != null && isTrace); // [HASLab]
pathButton.setEnabled(!seg_iteration); // [HASLab]
cnfgMenu.setEnabled(!isMeta && settingsOpen == 0 && enumerator != null); // [HASLab]
cnfgMenu.setVisible(isTrace); // [HASLab]
cnfgButton.setVisible(!isMeta && settingsOpen == 0 && enumerator != null && isTrace); // [HASLab]
Expand Down Expand Up @@ -1127,6 +1139,8 @@ public void loadXML(final String fileName, boolean forcefully, int state) {
current = state; // [HASLab]
final String xmlFileName = Util.canon(fileName);
File f = new File(xmlFileName);
if (!forcefully)
seg_iteration = false;
if (forcefully || !xmlFileName.equals(this.xmlFileName)) {
for (int i = 0; i < statepanes; i++) { // [HASLab]
try {
Expand Down Expand Up @@ -1443,46 +1457,107 @@ private Runner doExportXml() {
}

// [HASLab]
// reuses the Pardinus instance to formula translation, so needs some tweaks to the Alloy level
// ad hoc implementation since alloy lacks a proper pretty printer
// also, prints conjunctions as lists, which can't be parsed
private Runner doExportLTL() {
if (wrap)
return wrapMe();
if (myStates.isEmpty())
return null;
TemporalInstance inst = (TemporalInstance) myStates.get(myStates.size() - 1).getOriginalInstance().originalA4.debugExtractKInstance();
Formula rels = Formula.TRUE;
for (Relation r : inst.state(0).relations())
if (!(r.toString().startsWith("Int/") || r.toString().startsWith("seq/") || r.isAtom()))
rels = rels.and(r.eq(r));
Formula form = null;
Map<Object,Expression> reifs = new HashMap<Object,Expression>();
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());
Decls decs = null;
for (Expression rs : reifs.values()) {
if (decs == null)
decs = ((Variable) rs).oneOf(unvs);
else
decs = decs.and(((Variable) rs).oneOf(unvs));
}
form = ((QuantifiedFormula) form).formula().forSome(decs);
// [HASLab] normalize variable names
AbstractReplacer repls = new AbstractReplacer(new HashSet<Node>()) {

@Override
public Expression visit(Variable v) {
final Expression ret = lookup(v);
if (ret != null)
return ret;
String n = v.name().replace("$", "");
return cache(v, Variable.nary(n, v.arity()));
Map<String,ExprVar> reifs = new HashMap<String,ExprVar>();
A4Solution inst = myStates.get(myStates.size() - 1).getOriginalInstance().originalA4;

StringJoiner config = new StringJoiner(" and ");
for (Sig s : inst.getAllReachableSigs()) {
if (s.isPrivate != null || s.isVariable != null || s.equals(Sig.UNIV) || s.equals(Sig.NONE))
continue;
A4TupleSet ts = inst.eval(s);
Expr tupleset = null;
for (A4Tuple t : ts) {
Expr tuple = null;
for (int ai = 0; ai < t.arity(); ai++) {
Expr atom;
if (t.atom(ai).matches("-?\\d+")) {
atom = ExprConstant.makeNUMBER(Integer.valueOf(t.atom(ai)));
} else {
atom = reifs.computeIfAbsent("_" + t.atom(ai).replace("$", "").replace("/", "_"), k -> ExprVar.make(null, k));
}
tuple = tuple == null ? atom : tuple.product(tuple);
}
tupleset = tupleset == null ? tuple : tupleset.plus(tuple);
}
if (tupleset == null) {
tupleset = ExprConstant.EMPTYNESS;
for (int ai = 0; ai < ts.arity() - 1; ai++)
tupleset = tupleset.product(ExprConstant.EMPTYNESS);
}
config.add(s.equal(tupleset).toString());
}

};
form = form.accept(repls);
OurDialog.showtext("Text Viewer", PrettyPrinter.print(form, 4).replaceAll("Int\\[(-?\\d*)\\]", "$1").replaceFirst("some", "some disj"));
List<String> states = new ArrayList<String>();
for (int i = 0; i < inst.getTraceLength(); i++) {
StringJoiner state = new StringJoiner(" and ");
for (Sig s : inst.getAllReachableSigs()) {
if (s.isPrivate != null || (s.isVariable == null && !s.equals(Sig.UNIV)))
continue;
A4TupleSet ts = inst.eval(s, i);
Expr tupleset = null;
for (A4Tuple t : ts) {
Expr tuple = null;
for (int ai = 0; ai < t.arity(); ai++) {
Expr atom;
if (t.atom(ai).matches("-?\\d+")) {
atom = ExprConstant.makeNUMBER(Integer.valueOf(t.atom(ai)));
} else {
atom = reifs.computeIfAbsent("_" + t.atom(ai).replace("$", "").replace("/", "_"), k -> ExprVar.make(null, k));
}
tuple = tuple == null ? atom : tuple.product(tuple);
}
tupleset = tupleset == null ? tuple : tupleset.plus(tuple);
}
if (tupleset == null) {
tupleset = ExprConstant.EMPTYNESS;
for (int ai = 0; ai < ts.arity() - 1; ai++)
tupleset = tupleset.product(ExprConstant.EMPTYNESS);
}
state.add(s.equal(tupleset).toString());
}
states.add(state.toString());
}
StringBuilder sb = new StringBuilder();
sb.append("some disj ");
StringJoiner sj = new StringJoiner(",");
for (ExprVar v : reifs.values())
sj.add(v.toString());
sb.append(sj.toString());
sb.append(" : ");
Expr unvs = Sig.UNIV;
for (int i = 0; i < inst.getTraceLength() - 1; i++)
unvs = Sig.UNIV.plus(unvs.prime());
sb.append(unvs.toString());
sb.append(" {\n ");
sb.append(config.toString());
sb.append("\n\n ");
StringJoiner statesj = new StringJoiner(";\n ");
for (String s : states)
statesj.add(s);
sb.append(statesj.toString());
sb.append("\n\n ");
for (int i = 0; i < inst.getLoopState(); i++)
sb.append("after ");
sb.append(" {\n");
for (int i = inst.getLoopState(); i < inst.getTraceLength(); i++) {
StringBuilder sa = new StringBuilder("");
for (int j = inst.getLoopState(); j < inst.getTraceLength(); j++)
sa.append("after ");
sa.append("(");
sa.append(states.get(i));
sa.append(")");
sb.append(" (" + states.get(i) + ") implies " + sa.toString() + "\n");
}
sb.append(" }\n}\n");
OurDialog.showtext("Text Viewer", sb.toString());
return null;
}

Expand Down Expand Up @@ -1619,6 +1694,7 @@ private Runner doConfig() {
OurDialog.alert("Cannot display the next solution since the analysis engine is not loaded with the visualizer.");
} else {
try {
seg_iteration = false;
enumerator.compute(new String[] {
xmlFileName, -1 + ""
});
Expand All @@ -1629,6 +1705,32 @@ private Runner doConfig() {
return null;
}

/**
* This method attempts to derive the next satisfying instance.
*/
// [HASLab]
private Runner doPath() {
if (wrap)
return wrapMe();
if (settingsOpen != 0)
return null;
if (xmlFileName.length() == 0) {
OurDialog.alert("Cannot display the next solution since no instance is currently loaded.");
} else if (enumerator == null) {
OurDialog.alert("Cannot display the next solution since the analysis engine is not loaded with the visualizer.");
} else {
try {
seg_iteration = false;
enumerator.compute(new String[] {
xmlFileName, -2 + ""
});
} catch (Throwable ex) {
OurDialog.alert(ex.getMessage());
}
}
return null;
}

/** This method attempts to derive the next satisfying instance. */
// [HASLab] simulator
private Runner doFork() {
Expand All @@ -1642,6 +1744,7 @@ private Runner doFork() {
OurDialog.alert("Cannot display the next solution since the analysis engine is not loaded with the visualizer.");
} else {
try {
seg_iteration = true;
enumerator.compute(new String[] {
xmlFileName, current + 1 + ""
});
Expand All @@ -1665,6 +1768,7 @@ private Runner doInit() {
OurDialog.alert("Cannot display the next solution since the analysis engine is not loaded with the visualizer.");
} else {
try {
seg_iteration = true;
enumerator.compute(new String[] {
xmlFileName, 0 + ""
});
Expand Down
5 changes: 5 additions & 0 deletions org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/ExprUnary.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,11 @@ public void toString(StringBuilder out, int indent) {
sub.toString(out, -1);
out.append(']');
return;
case PRIME : // [HASLab]
out.append('(');
sub.toString(out, -1);
out.append(")'");
return;
case NOOP :
break;
default :
Expand Down
2 changes: 2 additions & 0 deletions org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -484,6 +484,8 @@ private A4Solution(A4Solution old, int state) throws Err {
try { // [HASLab] better reporting of unsupported iteration
if (state == -1) // [HASLab] simulator, this is a next config
inst = old.kEnumerator.nextC().instance();
else if (state == -2) // [HASLab] simulator, this is a next path
inst = old.kEnumerator.nextP().instance();
else if (state >= 0) { // [HASLab] simulator, this is a fork
Set<Relation> rels = ((TemporalInstance) old.eval.instance()).state(0).relations().stream().filter(r -> r.isVariable()).collect(Collectors.toSet());
inst = old.kEnumerator.nextS(state, 1, rels).instance();
Expand Down

0 comments on commit dca5028

Please sign in to comment.