Skip to content

Commit

Permalink
Merge branch 'heads/v2.1'
Browse files Browse the repository at this point in the history
  • Loading branch information
@nmacedo
nmacedo committed Jan 27, 2021
2 parents 9fa0aec + 965fc71 commit ac6b4a4
Show file tree
Hide file tree
Showing 16 changed files with 168 additions and 157 deletions.
20 changes: 10 additions & 10 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 @@ -650,11 +650,11 @@ else if (height < 100)
else
menuItem(fileMenu, "Close All", 'A', doCloseAll());
JMenu instanceMenu = menu(mb, "&Instance", null);
enumerateMenu = menuItem(instanceMenu, "Show Fresh 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]
enumerateMenu = menuItem(instanceMenu, "Show New Solution", 'N', 'N', doNext());
cnfgMenu = menuItem(instanceMenu, "Show New Configuration", 'C', 'C', doConfig()); // [HASLab]
pathMenu = menuItem(instanceMenu, "Show New Path", 'P', 'P', doPath()); // [HASLab]
initMenu = menuItem(instanceMenu, "Show New Initial State", 'I', 'I', doInit()); // [HASLab]
forkMenu = menuItem(instanceMenu, "Show New Fork", 'F', 'F', doFork()); // [HASLab]
leftNavMenu = menuItem(instanceMenu, "Show Previous State", KeyEvent.VK_LEFT, KeyEvent.VK_LEFT, leftNavListener); // [HASLab]
rightNavMenu = menuItem(instanceMenu, "Show Next State", KeyEvent.VK_LEFT, KeyEvent.VK_RIGHT, rightNavListener); // [HASLab]
thememenu = menu(mb, "&Theme", doRefreshTheme());
Expand Down Expand Up @@ -707,11 +707,11 @@ public void actionPerformed(ActionEvent e) {
toolbar.add(magicLayout = OurUtil.button("Magic Layout", "Automatic theme customization (will reset current theme)", "images/24_settings_apply2.gif", doMagicLayout()));
toolbar.add(openEvaluatorButton = OurUtil.button("Evaluator", "Open the evaluator", "images/24_settings.gif", doOpenEvalPanel()));
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(enumerateButton = OurUtil.button("New", "Show a new solution", "images/24_history.gif", doNext()));
toolbar.add(cnfgButton = OurUtil.button("New Config", "Show a new configuration", "images/24_history.gif", doConfig())); // [HASLab]
toolbar.add(pathButton = OurUtil.button("New Path", "Show a new path", "images/24_history.gif", doPath())); // [HASLab]
toolbar.add(initButton = OurUtil.button("New Init", "Show a new initial state", "images/24_history.gif", doInit())); // [HASLab]
toolbar.add(forkButton = OurUtil.button("New Fork", "Show a new fork", "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));
toolbar.add(rightNavButton = OurUtil.button(new String(Character.toChars(0x2192)), "Show the next state", "images/24_history.gif", rightNavListener));
toolbar.add(projectionButton);
Expand Down
4 changes: 2 additions & 2 deletions ...ools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
import static edu.mit.csail.sdg.alloy4.A4Preferences.AutoVisualize;
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreGranularity;
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreMinimization;
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposedPref;
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposePref;
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontName;
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontSize;
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
Expand Down Expand Up @@ -432,7 +432,7 @@ protected Component initEditorPane() {
}

protected Component initSolverPane() {
JPanel p = OurUtil.makeGrid(2, gbc().make(), mkCombo(Solver), mkSlider(SkolemDepth), mkCombo(Unrolls), mkCombo(CoreGranularity), mkSlider(CoreMinimization), mkSlider(DecomposedPref)); // [HASLab]);
JPanel p = OurUtil.makeGrid(2, gbc().make(), mkCombo(Solver), mkSlider(SkolemDepth), mkCombo(Unrolls), mkCombo(CoreGranularity), mkSlider(CoreMinimization), mkSlider(DecomposePref)); // [HASLab]);
int r = 6; // [HASLab]
addToGrid(p, mkCheckBox(NoOverflow), gbc().pos(0, r++).gridwidth(2));
addToGrid(p, mkCheckBox(ImplicitThis), gbc().pos(0, r++).gridwidth(2));
Expand Down
6 changes: 3 additions & 3 deletions org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleCLI.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,10 +115,10 @@ public void bound(String msg) {
sb.append(msg);
}

// [HASLab]
@Override
public void translate(String solver, String strat, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
debug("Solver=" + solver + " Decomposed=" + strat + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + "\n"); // [HASLab]
// [HASLab] trace + decompose params
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"); // [HASLab]
}

@Override
Expand Down
8 changes: 4 additions & 4 deletions org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
import static edu.mit.csail.sdg.alloy4.A4Preferences.AutoVisualize;
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreGranularity;
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreMinimization;
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposedPref;
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposePref;
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontName;
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontSize;
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
Expand Down Expand Up @@ -1132,7 +1132,7 @@ private Runner doRefreshRun() {
}
if (cp.size() > 1) {
JMenuItem menuItem = new JMenuItem("Execute All", null);
// [Electrum] cmd+u acc for mac
// [HASLab] cmd+u acc for mac
final int mnemonic = Util.onMac() ? VK_U : VK_A;
menuItem.setMnemonic(mnemonic);
menuItem.setAccelerator(KeyStroke.getKeyStroke(mnemonic, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()));
Expand Down Expand Up @@ -1191,7 +1191,7 @@ private Runner doRun(Integer commandIndex) {
opt.coreMinimization = CoreMinimization.get();
opt.inferPartialInstance = InferPartialInstance.get();
opt.coreGranularity = CoreGranularity.get();
opt.decomposed_mode = DecomposedPref.get().ordinal(); // [HASLab]
opt.decompose_mode = DecomposePref.get().ordinal(); // [HASLab]
opt.originalFilename = Util.canon(text.get().getFilename());
opt.solver = Solver.get();
task.bundleIndex = i;
Expand Down Expand Up @@ -1449,7 +1449,7 @@ private Runner doRefreshOption() {

if (Version.experimental) {
addToMenu(optmenu, Unrolls);
addToMenu(optmenu, DecomposedPref); // [HASLab]
addToMenu(optmenu, DecomposePref); // [HASLab]
addToMenu(optmenu, ImplicitThis, NoOverflow, InferPartialInstance);
}

Expand Down
17 changes: 9 additions & 8 deletions org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleMain.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,8 +92,9 @@ public void bound(String msg) {
}

@Override
public void translate(String solver, String mode, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
info("Solver=" + solver + " Mode=" + mode + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + "\n");
// [HASLab] trace + decompose params
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"); // [HASLab]
}

int totalVars = 0, totalPvars = 0, totalClauses = 0, lastStep = 0;
Expand Down Expand Up @@ -209,7 +210,7 @@ private static Options options() {

options.addOption(Option.builder().longOpt("cli").hasArg(false).desc("force CLI mode").build());

options.addOption(Option.builder("d").longOpt("decomposed").hasArg(true).argName("threads").optionalArg(true).required(false).desc("run in decomposed mode").build());
options.addOption(Option.builder("d").longOpt("decompose").hasArg(true).argName("threads").optionalArg(true).required(false).desc("run in decompose mode").build());

options.addOption(Option.builder("so").longOpt("solver-options").hasArg(true).required(false).desc("additional solver-specific options").build());

Expand Down Expand Up @@ -268,12 +269,12 @@ else if (clargs.hasOption("NuSMV"))
else if (clargs.hasOption("nuXmv"))
options.solver = A4Options.SatSolver.electrodX(clargs.hasOption("so") ? clargs.getOptionValue("so").split(",") : new String[0]);

if (clargs.hasOption("decomposed"))
options.decomposed_mode = 1;
if (clargs.getOptionValue("decomposed") != null)
options.decomposed_threads = Integer.valueOf(clargs.getOptionValue("decomposed"));
if (clargs.hasOption("decompose"))
options.decompose_mode = 1;
if (clargs.getOptionValue("decompose") != null)
options.decompose_threads = Integer.valueOf(clargs.getOptionValue("decompose"));
else
options.decomposed_mode = 0;
options.decompose_mode = 0;

int i0 = 0, i1 = cmds.size();
if (clargs.hasOption("command")) {
Expand Down
6 changes: 3 additions & 3 deletions ...oytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -364,12 +364,12 @@ public void debug(final String msg) {
cb("debug", msg.trim());
}

// [HASLab]
/** {@inheritDoc} */
@Override
public void translate(String solver, String strat, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
// [HASLab] trace + decompose params
public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
startTime = System.currentTimeMillis();
cb("translate", "Solver=" + solver + " Decomposed=" + strat + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + (skolemDepth == 0 ? "" : " SkolemDepth=" + skolemDepth) + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + '\n'); // [HASLab]
cb("translate", "Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + (skolemDepth == 0 ? "" : " SkolemDepth=" + skolemDepth) + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n"); // [HASLab]
}

/** {@inheritDoc} */
Expand Down
Loading

0 comments on commit ac6b4a4

Please sign in to comment.