From 73892e910c4429861d21331d54edf21932b885a6 Mon Sep 17 00:00:00 2001 From: Peter Kriens Date: Mon, 4 Mar 2024 17:32:41 +0100 Subject: [PATCH] Diverse fixes --- .../edu/mit/csail/sdg/alloy4viz/VizGUI.java | 2 +- .../mit/csail/sdg/alloy4whole/SimpleGUI.java | 31 ++++++---- .../csail/sdg/alloy4whole/SimpleReporter.java | 5 +- .../java/org/alloytools/alloy/cli/CLI.java | 61 +++++++++++-------- .../org/alloytools/alloy/cli/CommandInfo.java | 6 +- .../edu/mit/csail/sdg/alloy4/OurDialog.java | 2 +- org.alloytools.alloy.dist/bnd.bnd | 1 + .../java/kodkod/engine/satlab/SATFactory.java | 19 ++++-- 8 files changed, 80 insertions(+), 47 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 index 09246ee12..81c17fe2e 100644 --- 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 @@ -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; diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java index 0c7ffa04d..2e6402d2e 100644 --- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java +++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java @@ -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. @@ -1427,7 +1428,7 @@ private Runner doOptRefreshFont() { } private Runner doOptRefreshLineNumbers() { - if ( wrap ) { + if (wrap) { return wrapMe(); } text.enableLineNumbers(LineNumbers.get()); @@ -1690,7 +1691,7 @@ 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); @@ -1698,17 +1699,16 @@ Runner doVisualize(String arg) { } 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; } @@ -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)); + } } } diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java index 9c19e83e2..5f1735426 100644 --- a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java +++ b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java @@ -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"); @@ -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(); diff --git a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java index 9f1eb75b9..501044cf3 100644 --- a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java +++ b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CLI.java @@ -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 @@ -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(); @@ -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); @@ -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 { diff --git a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CommandInfo.java b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CommandInfo.java index bf6a33741..845cae1d3 100644 --- a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CommandInfo.java +++ b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/CommandInfo.java @@ -9,8 +9,12 @@ public class CommandInfo implements Comparable{ 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); } } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurDialog.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurDialog.java index 6e92f5b82..26f6892ed 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurDialog.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/OurDialog.java @@ -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); diff --git a/org.alloytools.alloy.dist/bnd.bnd b/org.alloytools.alloy.dist/bnd.bnd index c46e38779..dceb852c8 100644 --- a/org.alloytools.alloy.dist/bnd.bnd +++ b/org.alloytools.alloy.dist/bnd.bnd @@ -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}, \ diff --git a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/satlab/SATFactory.java b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/satlab/SATFactory.java index 4165d1432..af90f9eb1 100644 --- a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/satlab/SATFactory.java +++ b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/satlab/SATFactory.java @@ -93,6 +93,11 @@ public String id() { return "KK"; } + @Override + public String name() { + return "KodKod output"; + } + @Override public Optional getDescription() { return Optional.of( @@ -121,16 +126,16 @@ public String id() { return "CNF"; } + @Override + public String name() { + return "CNF output"; + } @Override public Optional 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"; } @@ -373,7 +378,7 @@ public int hashCode() { } public String toString() { - return id(); + return name(); } public abstract String type(); @@ -389,4 +394,8 @@ public String attributes() { return attrs.stream().collect(Collectors.joining(",")); } + + public String name() { + return id(); + } }