Skip to content

Commit ac6b4a4

Browse files
nmacedonmacedo
committed
Merge branch 'heads/v2.1'
2 parents 9fa0aec + 965fc71 commit ac6b4a4

File tree

16 files changed

+168
-157
lines changed

16 files changed

+168
-157
lines changed

‎org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java

+10-10
Original file line numberDiff line numberDiff line change
@@ -650,11 +650,11 @@ else if (height < 100)
650650
else
651651
menuItem(fileMenu, "Close All", 'A', doCloseAll());
652652
JMenu instanceMenu = menu(mb, "&Instance", null);
653-
enumerateMenu = menuItem(instanceMenu, "Show Fresh Solution", 'N', 'N', doNext());
654-
cnfgMenu = menuItem(instanceMenu, "Show Fresh Configuration", 'C', 'C', doConfig()); // [HASLab]
655-
pathMenu = menuItem(instanceMenu, "Show Fresh Path", 'P', 'P', doPath()); // [HASLab]
656-
initMenu = menuItem(instanceMenu, "Show Fresh Initial State", 'I', 'I', doInit()); // [HASLab]
657-
forkMenu = menuItem(instanceMenu, "Show Different Post-state", 'F', 'F', doFork()); // [HASLab]
653+
enumerateMenu = menuItem(instanceMenu, "Show New Solution", 'N', 'N', doNext());
654+
cnfgMenu = menuItem(instanceMenu, "Show New Configuration", 'C', 'C', doConfig()); // [HASLab]
655+
pathMenu = menuItem(instanceMenu, "Show New Path", 'P', 'P', doPath()); // [HASLab]
656+
initMenu = menuItem(instanceMenu, "Show New Initial State", 'I', 'I', doInit()); // [HASLab]
657+
forkMenu = menuItem(instanceMenu, "Show New Fork", 'F', 'F', doFork()); // [HASLab]
658658
leftNavMenu = menuItem(instanceMenu, "Show Previous State", KeyEvent.VK_LEFT, KeyEvent.VK_LEFT, leftNavListener); // [HASLab]
659659
rightNavMenu = menuItem(instanceMenu, "Show Next State", KeyEvent.VK_LEFT, KeyEvent.VK_RIGHT, rightNavListener); // [HASLab]
660660
thememenu = menu(mb, "&Theme", doRefreshTheme());
@@ -707,11 +707,11 @@ public void actionPerformed(ActionEvent e) {
707707
toolbar.add(magicLayout = OurUtil.button("Magic Layout", "Automatic theme customization (will reset current theme)", "images/24_settings_apply2.gif", doMagicLayout()));
708708
toolbar.add(openEvaluatorButton = OurUtil.button("Evaluator", "Open the evaluator", "images/24_settings.gif", doOpenEvalPanel()));
709709
toolbar.add(closeEvaluatorButton = OurUtil.button("Close Evaluator", "Close the evaluator", "images/24_settings_close2.gif", doCloseEvalPanel()));
710-
toolbar.add(enumerateButton = OurUtil.button("Next", "Show a fresh solution", "images/24_history.gif", doNext()));
711-
toolbar.add(cnfgButton = OurUtil.button("Fresh Config", "Show a fresh configuration", "images/24_history.gif", doConfig())); // [HASLab]
712-
toolbar.add(pathButton = OurUtil.button("Fresh Path", "Show a fresh path", "images/24_history.gif", doPath())); // [HASLab]
713-
toolbar.add(initButton = OurUtil.button("Fresh Init", "Show a fresh initial state", "images/24_history.gif", doInit())); // [HASLab]
714-
toolbar.add(forkButton = OurUtil.button("Fork", "Show a different post-state", "images/24_history.gif", doFork())); // [HASLab]
710+
toolbar.add(enumerateButton = OurUtil.button("New", "Show a new solution", "images/24_history.gif", doNext()));
711+
toolbar.add(cnfgButton = OurUtil.button("New Config", "Show a new configuration", "images/24_history.gif", doConfig())); // [HASLab]
712+
toolbar.add(pathButton = OurUtil.button("New Path", "Show a new path", "images/24_history.gif", doPath())); // [HASLab]
713+
toolbar.add(initButton = OurUtil.button("New Init", "Show a new initial state", "images/24_history.gif", doInit())); // [HASLab]
714+
toolbar.add(forkButton = OurUtil.button("New Fork", "Show a new fork", "images/24_history.gif", doFork())); // [HASLab]
715715
toolbar.add(leftNavButton = OurUtil.button(new String(Character.toChars(0x2190)), "Show the previous state", "images/24_history.gif", leftNavListener));
716716
toolbar.add(rightNavButton = OurUtil.button(new String(Character.toChars(0x2192)), "Show the next state", "images/24_history.gif", rightNavListener));
717717
toolbar.add(projectionButton);

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
import static edu.mit.csail.sdg.alloy4.A4Preferences.AutoVisualize;
55
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreGranularity;
66
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreMinimization;
7-
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposedPref;
7+
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposePref;
88
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontName;
99
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontSize;
1010
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
@@ -432,7 +432,7 @@ protected Component initEditorPane() {
432432
}
433433

434434
protected Component initSolverPane() {
435-
JPanel p = OurUtil.makeGrid(2, gbc().make(), mkCombo(Solver), mkSlider(SkolemDepth), mkCombo(Unrolls), mkCombo(CoreGranularity), mkSlider(CoreMinimization), mkSlider(DecomposedPref)); // [HASLab]);
435+
JPanel p = OurUtil.makeGrid(2, gbc().make(), mkCombo(Solver), mkSlider(SkolemDepth), mkCombo(Unrolls), mkCombo(CoreGranularity), mkSlider(CoreMinimization), mkSlider(DecomposePref)); // [HASLab]);
436436
int r = 6; // [HASLab]
437437
addToGrid(p, mkCheckBox(NoOverflow), gbc().pos(0, r++).gridwidth(2));
438438
addToGrid(p, mkCheckBox(ImplicitThis), gbc().pos(0, r++).gridwidth(2));

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -115,10 +115,10 @@ public void bound(String msg) {
115115
sb.append(msg);
116116
}
117117

118-
// [HASLab]
119118
@Override
120-
public void translate(String solver, String strat, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
121-
debug("Solver=" + solver + " Decomposed=" + strat + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + "\n"); // [HASLab]
119+
// [HASLab] trace + decompose params
120+
public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
121+
debug("Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n"); // [HASLab]
122122
}
123123

124124
@Override

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

+4-4
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424
import static edu.mit.csail.sdg.alloy4.A4Preferences.AutoVisualize;
2525
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreGranularity;
2626
import static edu.mit.csail.sdg.alloy4.A4Preferences.CoreMinimization;
27-
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposedPref;
27+
import static edu.mit.csail.sdg.alloy4.A4Preferences.DecomposePref;
2828
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontName;
2929
import static edu.mit.csail.sdg.alloy4.A4Preferences.FontSize;
3030
import static edu.mit.csail.sdg.alloy4.A4Preferences.ImplicitThis;
@@ -1132,7 +1132,7 @@ private Runner doRefreshRun() {
11321132
}
11331133
if (cp.size() > 1) {
11341134
JMenuItem menuItem = new JMenuItem("Execute All", null);
1135-
// [Electrum] cmd+u acc for mac
1135+
// [HASLab] cmd+u acc for mac
11361136
final int mnemonic = Util.onMac() ? VK_U : VK_A;
11371137
menuItem.setMnemonic(mnemonic);
11381138
menuItem.setAccelerator(KeyStroke.getKeyStroke(mnemonic, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()));
@@ -1191,7 +1191,7 @@ private Runner doRun(Integer commandIndex) {
11911191
opt.coreMinimization = CoreMinimization.get();
11921192
opt.inferPartialInstance = InferPartialInstance.get();
11931193
opt.coreGranularity = CoreGranularity.get();
1194-
opt.decomposed_mode = DecomposedPref.get().ordinal(); // [HASLab]
1194+
opt.decompose_mode = DecomposePref.get().ordinal(); // [HASLab]
11951195
opt.originalFilename = Util.canon(text.get().getFilename());
11961196
opt.solver = Solver.get();
11971197
task.bundleIndex = i;
@@ -1449,7 +1449,7 @@ private Runner doRefreshOption() {
14491449

14501450
if (Version.experimental) {
14511451
addToMenu(optmenu, Unrolls);
1452-
addToMenu(optmenu, DecomposedPref); // [HASLab]
1452+
addToMenu(optmenu, DecomposePref); // [HASLab]
14531453
addToMenu(optmenu, ImplicitThis, NoOverflow, InferPartialInstance);
14541454
}
14551455

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

+9-8
Original file line numberDiff line numberDiff line change
@@ -92,8 +92,9 @@ public void bound(String msg) {
9292
}
9393

9494
@Override
95-
public void translate(String solver, String mode, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
96-
info("Solver=" + solver + " Mode=" + mode + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + "\n");
95+
// [HASLab] trace + decompose params
96+
public void translate(String solver, int bitwidth, int maxseq, int mintrace, int maxtrace, int skolemDepth, int symmetry, String strat) {
97+
info("Solver=" + solver + " Steps=" + mintrace + ".." + maxtrace + " Bitwidth=" + bitwidth + " MaxSeq=" + maxseq + " Symmetry=" + (symmetry > 0 ? ("" + symmetry) : "OFF") + " Mode=" + strat + "\n"); // [HASLab]
9798
}
9899

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

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

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

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

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

271-
if (clargs.hasOption("decomposed"))
272-
options.decomposed_mode = 1;
273-
if (clargs.getOptionValue("decomposed") != null)
274-
options.decomposed_threads = Integer.valueOf(clargs.getOptionValue("decomposed"));
272+
if (clargs.hasOption("decompose"))
273+
options.decompose_mode = 1;
274+
if (clargs.getOptionValue("decompose") != null)
275+
options.decompose_threads = Integer.valueOf(clargs.getOptionValue("decompose"));
275276
else
276-
options.decomposed_mode = 0;
277+
options.decompose_mode = 0;
277278

278279
int i0 = 0, i1 = cmds.size();
279280
if (clargs.hasOption("command")) {

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -364,12 +364,12 @@ public void debug(final String msg) {
364364
cb("debug", msg.trim());
365365
}
366366

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

375375
/** {@inheritDoc} */

0 commit comments

Comments
 (0)