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 a8c10bf9b..3cd21c496 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 @@ -1,16 +1,14 @@ package org.alloytools.alloy.cli; import java.io.File; -import java.io.FileOutputStream; import java.io.FilterInputStream; import java.io.FilterOutputStream; import java.io.IOException; import java.io.InputStream; -import java.io.OutputStream; import java.io.PrintStream; import java.io.PrintWriter; -import java.util.ArrayList; import java.util.Collections; +import java.util.Formatter; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -19,21 +17,26 @@ import java.util.TreeMap; import java.util.concurrent.TimeUnit; import java.util.function.Predicate; +import java.util.stream.Collectors; -import org.alloytools.alloy.dto.SolutionDTO; import org.alloytools.alloy.infrastructure.api.AlloyMain; +import org.alloytools.util.table.Table; +import aQute.bnd.exceptions.Exceptions; import aQute.lib.env.Env; import aQute.lib.getopt.Arguments; import aQute.lib.getopt.Description; import aQute.lib.getopt.Options; import aQute.lib.io.IO; import aQute.lib.json.JSONCodec; +import aQute.lib.strings.Strings; import aQute.libg.glob.Glob; +import edu.mit.csail.sdg.alloy4.TableView; import edu.mit.csail.sdg.ast.Command; import edu.mit.csail.sdg.ast.ExprVar; import edu.mit.csail.sdg.parser.CompModule; import edu.mit.csail.sdg.parser.CompUtil; +import edu.mit.csail.sdg.sim.SimTupleset; import edu.mit.csail.sdg.translator.A4Options; import edu.mit.csail.sdg.translator.A4Solution; import edu.mit.csail.sdg.translator.A4SolutionWriter; @@ -81,7 +84,7 @@ interface ExecOptions extends Options { @Description("Specify the output type: none, text, table, json, xml") OutputType type(OutputType deflt); - @Description("Specify where the output should go. Default is the console") + @Description("Specify where the output should go. Default is the console. If a name specified, this will become a directory with the different outputs ordered as separate file with meaningful command names.") String output(); @Description("If set, the solution will include only those models in which no arithmetic overflows occur") @@ -127,7 +130,8 @@ public void _exec(ExecOptions options) throws Exception { Optional solver = SATFactory.find(options.solver("sat4j")); if (!solver.isPresent()) { - error("No such solver %s. Use the `solvers` command to see the available solvers", options.solver(null)); + error("No such solver %s: %s", options.solver(null), + SATFactory.getSolvers().stream().map(sf -> sf.id()).collect(Collectors.joining(", "))); return; } opt.solver = solver.get(); @@ -163,60 +167,86 @@ public void _exec(ExecOptions options) throws Exception { run = c -> g.matches(c.label); } - OutputStream out = output(options.output()); - if (out == null) { - return; - } - + File outdir = output(options.output(), getStem(file)); + OutputTrace trace = new OutputTrace(options.quiet() ? null : stdout); Map answers = new TreeMap<>(); + int n = 0; for (Command c : commands) { if (!run.test(c)) { trace("ignore command %s", c); continue; } - - if (!options.quiet()) - stdout.println("solving command " + c); - - long start = System.nanoTime(); - A4Solution s = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), c, opt); - long finish = System.nanoTime(); - int repeat = options.repeat(-1); + 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.isTransformer()) - info.cnf = rep.output; - answers.put(info, s); - stdout.println("answers " + answers.size()); - } while (repeat >= 0 && s.isIncremental() && (s = s.next()).satisfiable()); + int index = 0; + trace.format("%02d. %-5s %-20s %-60s ", n, c.check ? "check" : "run", c.label, c.scope); + String cname = toCName(c) + "-" + n; + + try { + A4Solution solution = TranslateAlloyToKodkod.execute_commandFromBook(rep, world.getAllReachableSigs(), + c, opt); + + if (!solution.satisfiable()) { + if (rep.output != null) { + trace.format(" %s", cname + "." + ext(rep.output)); + showTransformerFile(rep.output, outdir, cname); + } else { + trace.format("UNSAT"); + } + } else { + int back = 0; + do { + trace.back(back).format("%-5d", index); + generate(world, solution, options.type(OutputType.table), outdir, cname); + index++; + back = 5; + } while (index < repeat && solution.isIncremental() && (solution = solution.next()).satisfiable()); + + if (options.evaluator() && !answers.isEmpty()) { + evaluator(world, answers); + } + } + n++; + } catch (Exception e) { + error("command %s could not be solved: %s", cname, Exceptions.unrollCause(e)); + trace.format("!%s", Exceptions.unrollCause(e)); } + trace.format("%n"); } - if (!options.quiet() && answers.isEmpty()) { - stdout.println("no commands solved " + cmd); + } + + private void showTransformerFile(File source, File outdir, String cname) throws IOException { + if (outdir == null) + IO.copy(source, stdout); + else { + File out = new File(outdir, cname + "." + ext(source)); + IO.rename(source, out); } + IO.delete(source); + } - if (opt.solver.isTransformer()) { - for (CommandInfo c : answers.keySet()) { - IO.copy(c.cnf, out); - } + private String ext(File file) { + String parts[] = Strings.extension(file.getName()); + if (parts == null) + return ".unknown"; + else + return parts[1]; + } - } else { - generate(world, answers, options.type(OutputType.table), out); + private String toCName(Command c) { + StringBuilder sb = new StringBuilder(); + sb.append(c.label); + return sb.toString(); + } - if (options.evaluator() && !answers.isEmpty()) { - evaluator(world, answers); - } - } + private String getStem(File file) { + String parts[] = Strings.extension(file.getName()); + if (parts == null) { + return file.getName() + "-output"; + } else + return parts[0]; } private void evaluator(CompModule world, Map answers) throws Exception { @@ -257,103 +287,92 @@ public void _commands(CommandsOptions options) throws Exception { } } - private OutputStream output(String output) throws IOException { + private File output(String output, String stem) throws IOException { - if (output == null) { - return stdout; + if (output == null) + output = stem; + else if (output.equals("--")) { + return null; } - File file = IO.getFile(output); - file.getParentFile().mkdirs(); - if (!file.getParentFile().isDirectory()) { - error("Cannot create parent directory for %s", file); + File dir = IO.getFile(output); + IO.delete(dir); + IO.mkdirs(dir); + if (!dir.isDirectory()) { + error("Cannot create parent directory for %s", dir); return null; } - return new FileOutputStream(file); + return dir; + } - private void generate(CompModule world, Map s, OutputType type, OutputStream out) + private void generate(CompModule world, A4Solution solution, OutputType type, File outdir, String cname) throws Exception { - try { - switch (type) { - default: - case none: - return; - - case text: - try (PrintWriter pw = new PrintWriter(out)) { - for (Map.Entry e : s.entrySet()) { - A4Solution solution = e.getValue(); - CommandInfo cmdinfo = e.getKey(); - pw.println(cmdinfo); - pw.println(solution.toString()); - } - } - return; - - case table: - try (PrintWriter pw = new PrintWriter(out)) { - for (Map.Entry e : s.entrySet()) { - A4Solution solution = e.getValue(); - CommandInfo cmdinfo = e.getKey(); - - pw.println("---"); - pw.printf("%-40s%s%n", "Command", cmdinfo.command); - pw.printf("%-40s%s%n", "Duration (ms)", cmdinfo.durationInMs); - pw.printf("%-40s%s%n", "Sequence", cmdinfo.sequence); - - int n = 0; - if (solution.satisfiable()) { - pw.printf("%-40s%d/%d%n", "Trace", solution.getTraceLength(), solution.getLoopState()); - int max = solution.getTraceLength(); - while (solution.satisfiable() && n < max) { - for (ExprVar expr : solution.getAllSkolems()) { - Object eval = solution.eval(expr); - pw.printf("%-40s%s%n", expr.label, eval); - - } - pw.println(solution.toTable(n)); - solution = solution.next(); - n++; - } - } - } - } - break; + switch (type) { + default: + case none: + return; + + case text: + try (PrintWriter pw = getPrintWriter(outdir, cname, ".txt")) { + pw.println(solution.toString()); + } + return; - case json: - List trace = new ArrayList<>(); + case table: + try (PrintWriter pw = getPrintWriter(outdir, cname, ".md")) { + int n = solution.getLoopState(); + if (solution.getTraceLength() < 2) + n = -1; - for (Map.Entry e : s.entrySet()) { - A4Solution a4s = e.getValue(); - a4s.setModule(world); - trace.add(a4s.toDTO()); - } - JSONCodec codec = new JSONCodec(); - codec.enc().writeDefaults().indent(" ").to(out).put(trace); - break; - - case xml: - try (PrintWriter pw = new PrintWriter(out)) { - if (s.size() > 1) { - pw.println(""); - } - for (Map.Entry e : s.entrySet()) { - A4SolutionWriter.writeInstance(null, e.getValue(), pw, Collections.emptyList(), - Collections.emptyMap()); + for (int i = 0; i < solution.getTraceLength(); i++) { + Table t = solution.toTable(i); + if (n == i) { + pw.println("--loopstate->"); } - if (s.size() > 1) { - pw.println(""); + pw.println(t); + List skolems = solution.getAllSkolems(); + if (!skolems.isEmpty()) { + Table skolemsTable = new Table(skolems.size() + 1, 2, 1); + skolemsTable.set(0, 0, "skolem"); + skolemsTable.set(0, 1, "value"); + for (int j = 0; i < skolems.size(); j++) { + ExprVar var = skolems.get(j); + Object eval = solution.eval(var, i); + if (eval instanceof SimTupleset) { + Table tt = TableView.toTable((SimTupleset) eval); + skolemsTable.set(j + 1, 1, tt); + } else + skolemsTable.set(j + 1, 1, eval); + skolemsTable.set(j + 1, 0, var.label); + } + pw.println(skolemsTable); } } - break; + } + break; + case json: + JSONCodec codec = new JSONCodec(); + codec.enc().writeDefaults().indent(" ").to(getPrintWriter(outdir, cname, ".json")).put(solution.toDTO()); + break; + + case xml: + try (PrintWriter pw = getPrintWriter(outdir, cname, ".xml")) { + A4SolutionWriter.writeInstance(null, solution, pw, Collections.emptyList(), Collections.emptyMap()); } - } finally { - IO.close(out); + break; } } + private PrintWriter getPrintWriter(File outdir, String cname, String extension) throws IOException { + if (outdir == null) + return new PrintWriter(stdout); + + File file = new File(outdir, cname + extension); + return new PrintWriter(IO.writer(file)); + } + @Override public String toString() { return "CLI"; 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 845cae1d3..8860223b0 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,12 +9,12 @@ public class CommandInfo implements Comparable{ public long durationInMs; public File cnf; public File kodkod; - public int sequence; + public int trace; @Override public int compareTo(CommandInfo o) { int n = command.label.compareTo(o.command.label); if ( n != 0) return n; - return Integer.compare(sequence, o.sequence); + return Integer.compare(trace, o.trace); } } diff --git a/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/OutputTrace.java b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/OutputTrace.java new file mode 100644 index 000000000..190f6b76d --- /dev/null +++ b/org.alloytools.alloy.cli/src/main/java/org/alloytools/alloy/cli/OutputTrace.java @@ -0,0 +1,36 @@ +package org.alloytools.alloy.cli; + +import java.io.IOException; +import java.io.PrintStream; +import java.io.Writer; + +public class OutputTrace { + final Appendable writer; + + public OutputTrace(Appendable writer) { + this.writer = writer; + } + + public OutputTrace format(String format, Object... args) throws IOException { + if (writer != null) { + writer.append(String.format(format, args)); + if (writer instanceof Writer) { + ((Writer) writer).flush(); + } else if (writer instanceof PrintStream) { + ((PrintStream) writer).flush(); + } + } + return this; + } + + public OutputTrace back(int i) throws IOException { + if (writer != null) { + + while (i-- > 0) + this.writer.append('\u0008'); + + } + return this; + } + +} diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/SafeList.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/SafeList.java index d9dfc9ce2..7fb12d72c 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/SafeList.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/SafeList.java @@ -302,4 +302,12 @@ public String toString() { } return sb.append(']').toString(); } + + public List toList() { + List result = new ArrayList<>(); + for (T t : this) { + result.add(t); + } + return result; + } } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java index 5af0da882..3d5c47f31 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java @@ -924,8 +924,8 @@ public boolean hasConfigs() { * Returns an unmodifiable copy of the list of all skolems if the problem is * solved and is satisfiable; else returns an empty list. */ - public Iterable getAllSkolems() { - return skolems.dup(); + public List getAllSkolems() { + return skolems.toList(); } /** diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java index b1cad7bda..e21e7e085 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/TranslateAlloyToKodkod.java @@ -25,6 +25,7 @@ import java.util.Map; import java.util.Set; +import aQute.bnd.exceptions.Exceptions; import edu.mit.csail.sdg.alloy4.A4Reporter; import edu.mit.csail.sdg.alloy4.ConstList; import edu.mit.csail.sdg.alloy4.ConstMap; @@ -618,10 +619,7 @@ public static A4Solution execute_commandFromBook(A4Reporter rep, Iterable s Pos p = tr != null ? tr.frame.kv2typepos(ex.decl().variable()).b : Pos.UNKNOWN; throw new ErrorType(p, "Analysis cannot be performed since it requires higher-order quantification that could not be skolemized."); } catch (Throwable ex) { - if (ex instanceof Err) - throw (Err) ex; - else - throw new ErrorFatal("Unknown exception occurred: " + ex, ex); + throw Exceptions.duck(ex); } } diff --git a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/PardinusSolver.java b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/PardinusSolver.java index 69007095b..a32edf6ec 100644 --- a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/PardinusSolver.java +++ b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/PardinusSolver.java @@ -24,6 +24,7 @@ import java.io.File; import java.util.Iterator; +import java.util.Optional; import java.util.Set; import kodkod.ast.Formula; @@ -114,6 +115,7 @@ public void free() { } + /** * Calculates the solver that will be used, given the specified options. * This may be a regular {@link Solver regular Kodkod solver}, a