Skip to content

Commit

Permalink
Diverse fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@pkriens
pkriens committed Mar 6, 2024
1 parent fb76920 commit 73892e9
Show file tree
Hide file tree
Showing 8 changed files with 80 additions and 47 deletions.
2 changes: 1 addition & 1 deletion 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 @@ -1133,7 +1133,7 @@ private void addThemeHistory(String filename) {
* Helper method returns a JTextArea containing the given text.
*/
private JComponent getTextComponent(String text) {
final JTextArea ta = OurUtil.textarea(text, 10, 10, false, true);
final JTextArea ta = OurUtil.textarea(text, 10, 10, false, false);
final JScrollPane ans = new JScrollPane(ta, ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_AS_NEEDED) {

private static final long serialVersionUID = 0;
Expand Down
31 changes: 18 additions & 13 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 @@ -180,6 +180,7 @@
import edu.mit.csail.sdg.translator.A4Tuple;
import edu.mit.csail.sdg.translator.A4TupleSet;
import kodkod.engine.fol2sat.HigherOrderDeclException;
import kodkod.engine.satlab.SATFactory;

/**
* Simple graphical interface for accessing various features of the analyzer.
Expand Down Expand Up @@ -1427,7 +1428,7 @@ private Runner doOptRefreshFont() {
}

private Runner doOptRefreshLineNumbers() {
if ( wrap ) {
if (wrap) {
return wrapMe();
}
text.enableLineNumbers(LineNumbers.get());
Expand Down Expand Up @@ -1690,25 +1691,24 @@ Runner doVisualize(String arg) {
Pos p = new Pos(Util.canon(f), x1, y1, x2, y2);
text.shade(p);
}
if (arg.startsWith("CNF: ")) { // CNF: filename
if (arg.startsWith("CNF: ") || arg.startsWith("file:")) { // CNF: filename
String filename = Util.canon(arg.substring(5));
try {
String text = Util.readAll(filename);
OurDialog.showtext("Text Viewer", text);
} catch (IOException ex) {
log.logRed("Error reading the file \"" + filename + "\"\n");
}
}
if (arg.startsWith("XML: ")) { // XML: filename
} else if (arg.startsWith("XML: ")) { // XML: filename
viz.loadXML(Util.canon(arg.substring(5)), false, 0);
}
try {
Desktop desktop = java.awt.Desktop.getDesktop();
URI oURL = new URI(arg);
desktop.browse(oURL);
} catch (Exception e) {
// ignore
}
} else
try {
Desktop desktop = java.awt.Desktop.getDesktop();
URI oURL = new URI(arg);
desktop.browse(oURL);
} catch (Exception e) {
// ignore
}
return null;
}

Expand Down Expand Up @@ -2354,7 +2354,12 @@ private void addSubmenuItems(JMenu parent, ChoicePref pref) {
Object selected = pref.get();
for (Object item : pref.validChoices()) {
Action action = pref.getAction(item);
menuItem(parent, pref.renderValueLong(item).toString(), action, item == selected ? iconYes : iconNo);
JMenuItem submenu = menuItem(parent, pref.renderValueLong(item).toString(), action, item == selected ? iconYes : iconNo);

if (item instanceof SATFactory) {
SATFactory i = (SATFactory) item;
i.getDescription().ifPresent(d -> submenu.setToolTipText(d));
}
}
}

Expand Down
5 changes: 3 additions & 2 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 @@ -217,7 +217,9 @@ else if (ex instanceof ErrorType)
if (array[0].equals("resultCNF")) {
results.add(null);
span.setLength(len3);
span.log(" File written to " + array[1] + "\n\n");
span.log(" File written to ");
span.logLink(array[1].toString(), "file://" + array[1]);
span.log("\n\n");
}
if (array[0].equals("debug") && verbosity > 2) {
span.log(" " + array[1] + "\n");
Expand Down Expand Up @@ -759,7 +761,6 @@ else if (ai.highLevelCore().a.size() > 0)
for (int i = 0; i < result.size(); i++) {
Command r = world.getAllCommands().get(i);
if (result.get(i) == null) {
rep.cb("", " #" + (i + 1) + ": Unknown.\n");
continue;
}
StringBuilder sb = new StringBuilder();
Expand Down
61 changes: 37 additions & 24 deletions org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,16 +53,16 @@ public enum OutputType {
none, plain, json, xml;
}

InputStream stdin = new FilterInputStream(System.in) {
@Override
public void close() throws IOException {
}
};
PrintStream stdout = new PrintStream(new FilterOutputStream(System.out)) {
public void close() {
System.out.flush();
};
};
InputStream stdin = new FilterInputStream(System.in) {
@Override
public void close() throws IOException {
}
};
PrintStream stdout = new PrintStream(new FilterOutputStream(System.out)) {
public void close() {
System.out.flush();
};
};

/**
* Show the list of solvers
Expand Down Expand Up @@ -104,16 +104,20 @@ interface ExecOptions extends Options {

@Description("After resolving each command, start an evaluator")
boolean evaluator();

@Description("Find multiple solutions, up to this number. Use 0 for as many as can be found.")
int repeat(int deflt);

}

/**
* Execute a Alloy program
*
* @param options
* the options to use
* @param options the options to use
*/
@Description("Execute an Alloy program")
public void _exec(ExecOptions options) throws Exception {

SimpleReporter rep = new SimpleReporter(this);
A4Options opt = this.options.dup();
opt.noOverflow = options.nooverflow();
Expand Down Expand Up @@ -175,17 +179,27 @@ public void _exec(ExecOptions options) throws Exception {
stdout.println("solving command " + c);

long start = System.nanoTime();
A4Solution s = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), c,
opt);
A4Solution s = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), c, opt);
long finish = System.nanoTime();

CommandInfo info = new CommandInfo();
info.command = c;
info.durationInMs = TimeUnit.NANOSECONDS.toMillis(finish - start);
if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK)
info.cnf = rep.output;
answers.put(info, s);

int repeat = options.repeat(-1);
if (repeat == 0) {
repeat = Integer.MAX_VALUE;
}
if (s.satisfiable()) {
int sequence = 0;
do {
repeat--;
System.out.println("repeat " + repeat);
CommandInfo info = new CommandInfo();
info.command = c;
info.sequence = sequence++;
info.durationInMs = TimeUnit.NANOSECONDS.toMillis(finish - start);
if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK)
info.cnf = rep.output;
answers.put(info, s);
System.out.println("answers " + answers.size());
} while (repeat >= 0 && s.isIncremental() && (s = s.next()).satisfiable());
}
}
if (!options.quiet() && answers.isEmpty()) {
stdout.println("no commands found " + cmd);
Expand Down Expand Up @@ -229,8 +243,7 @@ interface CommandsOptions extends Options {
/**
* Execute a Alloy program
*
* @param options
* the options to use
* @param options the options to use
*/
@Description("Show all commands in an Alloy program")
public void _commands(CommandsOptions options) throws Exception {
Expand Down
6 changes: 5 additions & 1 deletion org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CommandInfo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,12 @@ public class CommandInfo implements Comparable<CommandInfo>{
public long durationInMs;
public File cnf;
public File kodkod;
public int sequence;
@Override
public int compareTo(CommandInfo o) {
return command.label.compareTo(o.command.label);
int n = command.label.compareTo(o.command.label);
if ( n != 0)
return n;
return Integer.compare(sequence, o.sequence);
}
}
2 changes: 1 addition & 1 deletion org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurDialog.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -382,7 +382,7 @@ public static JFrame showtext(String title, String text) {
JFrame window = new JFrame(title);
JButton done = new JButton("Close");
done.addActionListener(Runner.createDispose(window));
JScrollPane scrollPane = OurUtil.scrollpane(OurUtil.textarea(text, 20, 60, false, false));
JScrollPane scrollPane = OurUtil.scrollpane(OurUtil.textarea(text, 40, 90, false, false));
window.setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE);
window.getContentPane().setLayout(new BorderLayout());
window.getContentPane().add(scrollPane, BorderLayout.CENTER);
Expand Down
1 change: 1 addition & 0 deletions org.alloytools.alloy.dist/bnd.bnd
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ JPM-Command: alloy
@${repo;org.alloytools.alloy.cli}, \
@${repo;org.alloytools.pardinus.core}, \
@${repo;org.alloytools.pardinus.native}, \
@${repo;jline}, \
@${repo;org.sat4j.core}, \
@${repo;org.sat4j.maxsat}, \
@${repo;org.sat4j.pb}, \
Expand Down
19 changes: 14 additions & 5 deletions org.alloytools.pardinus.core/src/main/java/kodkod/engine/satlab/SATFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,11 @@ public String id() {
return "KK";
}

@Override
public String name() {
return "KodKod output";
}

@Override
public Optional<String> getDescription() {
return Optional.of(
Expand Down Expand Up @@ -121,16 +126,16 @@ public String id() {
return "CNF";
}

@Override
public String name() {
return "CNF output";
}
@Override
public Optional<String> getDescription() {
return Optional.of(
"CNF stands for Conjunctive Normal Form. It is specified by DIMACS. This is a standardized way of representing Boolean algebra expressions for processing by SAT solvers.");
}

public String toString() {
return id();
}

public String type() {
return "synthetic";
}
Expand Down Expand Up @@ -373,7 +378,7 @@ public int hashCode() {
}

public String toString() {
return id();
return name();
}

public abstract String type();
Expand All @@ -389,4 +394,8 @@ public String attributes() {

return attrs.stream().collect(Collectors.joining(","));
}

public String name() {
return id();
}
}

0 comments on commit 73892e9

Please sign in to comment.