diff --git a/cnf/central.mvn b/cnf/central.mvn index a735f3bd5..faf868b96 100644 --- a/cnf/central.mvn +++ b/cnf/central.mvn @@ -1,4 +1,5 @@ biz.aQute.bnd:aQute.libg:6.0.0 +biz.aQute.bnd:biz.aQute.bnd.annotation:6.0.0 biz.aQute:biz.aQute.wrapper.hamcrest:1.3 biz.aQute:biz.aQute.wrapper.junit:4.13.1 com.google.code.gson:gson:2.8.9 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 501044cf3..c679900fd 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 @@ -194,7 +194,7 @@ public void _exec(ExecOptions options) throws Exception { info.command = c; info.sequence = sequence++; info.durationInMs = TimeUnit.NANOSECONDS.toMillis(finish - start); - if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK) + if (opt.solver.isTransformer()) info.cnf = rep.output; answers.put(info, s); System.out.println("answers " + answers.size()); @@ -205,7 +205,7 @@ public void _exec(ExecOptions options) throws Exception { stdout.println("no commands found " + cmd); } - if (opt.solver == SATFactory.CNF || opt.solver == SATFactory.KK) { + if (opt.solver.isTransformer()) { for (CommandInfo c : answers.keySet()) { IO.copy(c.cnf, out); } diff --git a/org.alloytools.alloy.core/bnd.bnd b/org.alloytools.alloy.core/bnd.bnd index 1714378ce..f6b5a63c2 100644 --- a/org.alloytools.alloy.core/bnd.bnd +++ b/org.alloytools.alloy.core/bnd.bnd @@ -9,7 +9,8 @@ aQute.libg,\ org.alloytools.api,\ slf4j.api,\ - org.alloytools.pardinus.core + org.alloytools.pardinus.core,\ + biz.aQute.bnd.annotation -testpath: \ biz.aQute.wrapper.junit,\ diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java index 98d4a41b8..3937f9662 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Options.java @@ -15,7 +15,10 @@ package edu.mit.csail.sdg.translator; +import java.io.File; +import java.io.IOException; import java.io.Serializable; +import java.nio.file.Files; import kodkod.engine.satlab.SATFactory; @@ -163,4 +166,9 @@ public A4Options dup() { return x; } + public File tempFile(String extension) throws IOException { + File f = new File(tempDirectory); + return Files.createTempFile(f.toPath(), "alloy", extension).toFile(); + } + } 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 d781efc1d..6dee79c60 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 @@ -1156,6 +1156,8 @@ void kr2typeCLEAR() throws Err { /** Caches a constant pair of Type.EMPTY and Pos.UNKNOWN */ private Pair cachedPAIR = null; + private Formula fgoal; + /** * Maps a Kodkod variable to an Alloy Type and Alloy Pos (if no association * exists, it will return (Type.EMPTY , Pos.UNKNOWN) @@ -1553,10 +1555,9 @@ A4Solution solve(final A4Reporter rep, Command cmd, Simplifier simp, boolean try if (opt.inferPartialInstance && simp != null && formulas.size() > 0 && !simp.simplify(rep, this, formulas)) addFormula(Formula.FALSE, Pos.UNKNOWN); rep.translate(opt.solver.id(), bitwidth, maxseq, mintrace, maxtrace, solver.options().skolemDepth(), solver.options().symmetryBreaking(), A4Preferences.Decompose.values()[opt.decompose_mode].toString()); - Formula fgoal = Formula.and(formulas); + fgoal = Formula.and(formulas); rep.debug("Generating the solution...\n"); kEnumerator = null; - Solution sol = null; final Reporter oldReporter = solver.options().reporter(); final boolean solved[] = new boolean[] { true @@ -1595,56 +1596,34 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla } }); - if (!opt.solver.equals(SATFactory.CNF) && !opt.solver.equals(SATFactory.KK) && tryBookExamples) { // try book examples - A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null; - try { - sol = BookExamples.trial(r, this, fgoal, (AbstractKodkodSolver) solver.solver, cmd.check); - } catch (Throwable ex) { - sol = null; - } - } solved[0] = false; // this allows the reporter to report the # of - // vars/clauses + // vars/clauses for (Relation r : bounds.relations()) { formulas.add(r.eq(r)); } // Without this, kodkod refuses to grow unmentioned relations + fgoal = Formula.and(formulas); - // Now pick the solver and solve it! - if (opt.solver.equals(SATFactory.KK)) { - File tmpCNF = File.createTempFile("tmp", ".java", new File(opt.tempDirectory)); - String out = tmpCNF.getAbsolutePath(); - Util.writeAll(out, debugExtractKInput()); - rep.resultCNF(out); - return null; - } - if (opt.solver.equals(SATFactory.CNF)) { - File tmpCNF = File.createTempFile("tmp", ".cnf", new File(opt.tempDirectory)); - String out = tmpCNF.getAbsolutePath(); - solver.options().setSolver(WriteCNF.factory(out)); - try { - sol = solver.solve(fgoal, bounds); - } catch (WriteCNF.WriteCNFCompleted ex) { - rep.resultCNF(out); - return null; - } - // The formula is trivial (otherwise, it would have thrown an - // exception) - // Since the user wants it in CNF format, we manually generate a - // trivially satisfiable (or unsatisfiable) CNF file. - Util.writeAll(out, sol.instance() != null ? "p cnf 1 1\n1 0\n" : "p cnf 1 2\n1 0\n-1 0\n"); - rep.resultCNF(out); - return null; - } - if (/* solver.options().solver()==SATFactory.ZChaffMincost || */ !solver.options().solver().incremental()) { + + Solution sol; + if (opt.solver instanceof KKTransformer) { + sol = doKK(rep, opt); + } else if (opt.solver instanceof CNFTransformer) { + sol = doCNF(rep, opt); + } else if (tryBookExamples && solver.solver instanceof AbstractKodkodSolver) { + sol = tryBook(rep, cmd); + } else if (!solver.options().solver().incremental()) { sol = solver.solve(fgoal, bounds); - } else { + } else + sol = null; + + if (sol == null) { PardinusBounds b; if (solver.options().decomposed()) - b = PardinusBounds.splitAtTemporal(bounds); // [electrum] split bounds on temporal + b = PardinusBounds.splitAtTemporal(bounds); else b = bounds; - // [electrum] better handling of solving runtime errors + try { kEnumerator = new Peeker(solver.solveAll(fgoal, b)); } catch (InvalidMutableExpressionException e) { @@ -1656,11 +1635,17 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla Pos p = ((Expr) k2pos(e.node())).pos; throw new ErrorAPI(p, "Invalid specification for complete backend.\n" + e.getMessage()); } - if (sol == null) - sol = kEnumerator.next(); + sol = kEnumerator.next(); } + + if (sol.getOutput().isPresent()) { + rep.resultCNF(sol.getOutput().get().getAbsolutePath()); + return null; + } + if (!solved[0]) rep.solve(0, 0, 0, 0); + Instance inst = sol.instance(); if (inst != null && !(inst instanceof TemporalInstance)) inst = new TemporalInstance(Arrays.asList(inst), 0, 1); @@ -1715,6 +1700,39 @@ public synchronized void solvingCNF(int step, int primaryVars, int vars, int cla return this; } + @SuppressWarnings({ + "rawtypes", "unchecked" + } ) + private Solution tryBook(final A4Reporter rep, Command cmd) { + Solution sol; + A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null; + try { + sol = BookExamples.trial(r, this, fgoal, (AbstractKodkodSolver) solver.solver, cmd.check); + } catch (Throwable ex) { + rep.debug("" + ex); + sol = null; + } + return sol; + } + + private Solution doCNF(final A4Reporter rep, final A4Options opt) throws IOException { + File tmpCNF = opt.tempFile(".cnf"); + String out = tmpCNF.getAbsolutePath(); + solver.options().setSolver(WriteCNF.factory(out)); + Solution solve = solver.solve(fgoal, bounds); + solve.setOutput(tmpCNF); + return solve; + } + + private Solution doKK(final A4Reporter rep, final A4Options opt) throws IOException { + File tmpKK = opt.tempFile(".java"); + String out = tmpKK.getAbsolutePath(); + Util.writeAll(out, debugExtractKInput()); + Solution s = Solution.unsatisfiable(null, null); + s.setOutput(tmpKK); + return s; + } + // ===================================================================================================// /** This caches the toString() output. */ @@ -2167,4 +2185,18 @@ public InstanceDTO toDTO(int state) { return dto; } + public A4Reporter getReporter() { + return null; + } + + /** + * Add default transformers + * + * @param extensions + */ + public static void addTransformers(List extensions) { + extensions.add(new KKTransformer()); + extensions.add(new CNFTransformer()); + } + } diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/CNFTransformer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/CNFTransformer.java new file mode 100644 index 000000000..1d577be79 --- /dev/null +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/CNFTransformer.java @@ -0,0 +1,40 @@ +package edu.mit.csail.sdg.translator; + +import java.util.Optional; + +import kodkod.engine.satlab.SATFactory; + +public class CNFTransformer extends SATFactory { + + private static final long serialVersionUID = 1L; + + @Override + 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."); + } + + @Override + public String type() { + return "transformer"; + } + + @Override + public boolean isTransformer() { + return true; + } + + @Override + public boolean isPresent() { + return true; + } +} diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/KKTransformer.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/KKTransformer.java new file mode 100644 index 000000000..92f414bd7 --- /dev/null +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/KKTransformer.java @@ -0,0 +1,42 @@ +package edu.mit.csail.sdg.translator; + +import java.util.Optional; + +import kodkod.engine.satlab.SATFactory; + +public class KKTransformer extends SATFactory { + + private static final long serialVersionUID = 1L; + + @Override + public String id() { + return "KK"; + } + + + @Override + public String type() { + return "transformer"; + } + + @Override + public String name() { + return "KodKod output"; + } + + @Override + public Optional getDescription() { + return Optional.of("KK is the KodKod debug output format"); + } + + @Override + public boolean isTransformer() { + return true; + } + + @Override + public boolean isPresent() { + return true; + } + +} diff --git a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java index 437dd9020..aeec4b77e 100644 --- a/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java +++ b/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/WriteCNF.java @@ -27,7 +27,7 @@ * an exception (this code is adapted from ExternalSolver from Kodkod). */ -final class WriteCNF implements SATSolver { +final public class WriteCNF implements SATSolver { /** * This runtime exception is thrown when the CNF file has been written @@ -131,6 +131,7 @@ public void free() { Util.close(cnf); } + /** {@inheritDoc} */ @Override public void addVariables(int numVars) { @@ -173,10 +174,10 @@ public boolean solve() { cnf.seek(0); cnf.writeBytes("p cnf " + vars + " " + clauses); cnf.close(); + return false; } catch (Exception ex) { throw new RuntimeException("WriteCNF failed.", ex); } - throw new WriteCNFCompleted(); } /** {@inheritDoc} */ diff --git a/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java b/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java index f93f06944..2391a27d5 100644 --- a/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java +++ b/org.alloytools.alloy.core/src/main/java/org/alloytools/alloy/core/infra/AlloyDispatcher.java @@ -42,6 +42,7 @@ import aQute.service.reporter.Reporter; import edu.mit.csail.sdg.alloy4.A4Preferences; import edu.mit.csail.sdg.alloy4.A4Preferences.Pref; +import edu.mit.csail.sdg.translator.A4Solution; import kodkod.engine.satlab.ExternalSolver; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.SATSolver; @@ -533,6 +534,7 @@ public void setslf4j(Levels deflt, String... targets) { */ void loadExtensions(File extensions) { + A4Solution.addTransformers(SATFactory.extensions); if (!extensions.isDirectory()) return; diff --git a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/Solution.java b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/Solution.java index 31d7622fa..e3bb16b6f 100644 --- a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/Solution.java +++ b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/Solution.java @@ -21,12 +21,14 @@ */ package kodkod.engine; +import java.io.File; +import java.util.Optional; import kodkod.instance.Instance; + /** - * Represents the full solution to a formula: an - * instance if the formula is satisfiable or a - * proof of unsatisfiability if not. + * Represents the full solution to a formula: an instance if the formula is + * satisfiable or a proof of unsatisfiability if not. * * @specfield formula: Formula // the formula being solved * @specfield bounds: Bounds // the bounds on the formula @@ -37,9 +39,11 @@ public final class Solution { private final Statistics stats; private final Instance instance; private final Proof proof; - + private File output; + /** * Constructs a Solution from the given values. + * * @requires outcome != null && stats != null * @requires outcome = SATISFIABLE || TRIVIALLY_SATISFIABLE => instance != null */ @@ -50,80 +54,92 @@ private Solution(Outcome outcome, Statistics stats, Instance instance, Proof pro this.instance = instance; this.proof = proof; } - + /** * Returns a new Solution with a SATISFIABLE outcome, given stats and instance. - * @return {s: Solution | s.outcome() = SATISFIABLE && s.stats() = stats && s.instance() = instance } + * + * @return {s: Solution | s.outcome() = SATISFIABLE && s.stats() = stats && + * s.instance() = instance } */ public static Solution satisfiable(Statistics stats, Instance instance) { return new Solution(Outcome.SATISFIABLE, stats, instance, null); } - + /** - * Returns a new Solution with a TRIVIALLY_SATISFIABLE outcome, given stats and instance. - * @return {s: Solution | s.outcome() = TRIVIALLY_SATISFIABLE && s.stats() = stats && s.instance() = instance } + * Returns a new Solution with a TRIVIALLY_SATISFIABLE outcome, given stats and + * instance. + * + * @return {s: Solution | s.outcome() = TRIVIALLY_SATISFIABLE && s.stats() = + * stats && s.instance() = instance } */ static Solution triviallySatisfiable(Statistics stats, Instance instance) { return new Solution(Outcome.TRIVIALLY_SATISFIABLE, stats, instance, null); } - + /** * Returns a new Solution with a UNSATISFIABLE outcome, given stats and proof. - * @return {s: Solution | s.outcome() = UNSATISFIABLE && s.stats() = stats && s.proof() = proof } + * + * @return {s: Solution | s.outcome() = UNSATISFIABLE && s.stats() = stats && + * s.proof() = proof } */ public static Solution unsatisfiable(Statistics stats, Proof proof) { return new Solution(Outcome.UNSATISFIABLE, stats, null, proof); } - + /** - * Returns a new Solution with a TRIVIALLY_UNSATISFIABLE outcome, given stats and proof. - * @return {s: Solution | s.outcome() = TRIVIALLY_UNSATISFIABLE && s.stats() = stats && s.proof() = proof } + * Returns a new Solution with a TRIVIALLY_UNSATISFIABLE outcome, given stats + * and proof. + * + * @return {s: Solution | s.outcome() = TRIVIALLY_UNSATISFIABLE && s.stats() = + * stats && s.proof() = proof } */ static Solution triviallyUnsatisfiable(Statistics stats, Proof proof) { return new Solution(Outcome.TRIVIALLY_UNSATISFIABLE, stats, null, proof); } - + /** - * Returns the outcome of the attempt to find - * a model for this.formula. If the outcome is - * SATISFIABLE or TRIVIALLY_SATISFIABLE, a satisfying - * instance can be obtained by calling {@link #instance()}. - * If the formula is UNSATISFIABLE, a proof of unsatisfiability - * can be obtained by calling {@link #proof()} provided that - * translation logging was enabled and the unsatisfiability was - * determined using a core extracting - * {@link kodkod.engine.satlab.SATSolver sat solver}. - * Lastly, if the returned Outcome is - * or TRIVIALLY_UNSATISFIABLE, a proof of unsatisfiability can - * be obtained by calling {@link #proof()} provided that - * translation logging was enabled. - * @return an Outcome instance designating the - * satisfiability of this.formula with respect to this.bounds + * Returns the outcome of the attempt to find a model for this.formula. If the + * outcome is SATISFIABLE or TRIVIALLY_SATISFIABLE, a satisfying instance can be + * obtained by calling {@link #instance()}. If the formula is UNSATISFIABLE, a + * proof of unsatisfiability can be obtained by calling {@link #proof()} + * provided that translation logging was enabled and the unsatisfiability was + * determined using a core extracting {@link kodkod.engine.satlab.SATSolver sat + * solver}. Lastly, if the returned Outcome is or TRIVIALLY_UNSATISFIABLE, a + * proof of unsatisfiability can be obtained by calling {@link #proof()} + * provided that translation logging was enabled. + * + * @return an Outcome instance designating the satisfiability of this.formula + * with respect to this.bounds */ public Outcome outcome() { return outcome; } - + /** * Returns true iff this solution has a (trivially) satisfiable outcome. - * @return this.outcome = Outcome.SATISFIABLE || this.outcome = Outcome.TRIVIALLY_SATISFIABLE + * + * @return this.outcome = Outcome.SATISFIABLE || this.outcome = + * Outcome.TRIVIALLY_SATISFIABLE */ public final boolean sat() { - return outcome==Outcome.SATISFIABLE || outcome==Outcome.TRIVIALLY_SATISFIABLE; + return outcome == Outcome.SATISFIABLE || outcome == Outcome.TRIVIALLY_SATISFIABLE; } - + /** * Returns true iff this solution has a (trivially) unsatisfiable outcome. - * @return this.outcome = Outcome.UNSATISFIABLE || this.outcome = Outcome.TRIVIALLY_UNSATISFIABLE + * + * @return this.outcome = Outcome.UNSATISFIABLE || this.outcome = + * Outcome.TRIVIALLY_UNSATISFIABLE */ public final boolean unsat() { - return outcome==Outcome.UNSATISFIABLE || outcome==Outcome.TRIVIALLY_UNSATISFIABLE; + return outcome == Outcome.UNSATISFIABLE || outcome == Outcome.TRIVIALLY_UNSATISFIABLE; } - + /** - * Returns a satisfiying instance for this.formula, if the - * value returned by {@link #outcome() this.outcome()} is either - * SATISFIABLE or TRIVIALLY_SATISFIABLE. Otherwise returns null. + * Returns a satisfiying instance for this.formula, if the value returned by + * {@link #outcome() this.outcome()} is either SATISFIABLE or + * TRIVIALLY_SATISFIABLE. Otherwise returns null. + * * @return a satisfying instance for this.formula, if one exists. */ public Instance instance() { @@ -131,30 +147,30 @@ public Instance instance() { } /** - * Returns a proof of this.formula's unsatisfiability if the value - * returned by {@link #outcome() this.outcome()} is UNSATISFIABLE or - * TRIVIALLY_UNSATISFIABLE, translation logging was enabled during solving, - * and a core extracting {@link kodkod.engine.satlab.SATProver sat solver} (if any) - * was used to determine unsatisfiability. - * Otherwise, null is returned. - * @return a proof of this.formula's unsatisfiability, if one is available. + * Returns a proof of this.formula's unsatisfiability if the value returned by + * {@link #outcome() this.outcome()} is UNSATISFIABLE or + * TRIVIALLY_UNSATISFIABLE, translation logging was enabled during solving, and + * a core extracting {@link kodkod.engine.satlab.SATProver sat solver} (if any) + * was used to determine unsatisfiability. Otherwise, null is returned. + * + * @return a proof of this.formula's unsatisfiability, if one is available. */ public Proof proof() { return proof; } - + /** - * Returns the statistics gathered while solving - * this.formula. - * @return the statistics gathered while solving - * this.formula. + * Returns the statistics gathered while solving this.formula. + * + * @return the statistics gathered while solving this.formula. */ public Statistics stats() { return stats; } - + /** * Returns a string representation of this Solution. + * * @return a string representation of this Solution. */ public String toString() { @@ -162,12 +178,12 @@ public String toString() { b.append("---OUTCOME---\n"); b.append(outcome); b.append("\n"); - if (instance!=null) { + if (instance != null) { b.append("\n---INSTANCE---\n"); b.append(instance); b.append("\n"); } - if (proof!=null) { + if (proof != null) { b.append("\n---PROOF---\n"); b.append(proof); b.append("\n"); @@ -177,27 +193,40 @@ public String toString() { b.append("\n"); return b.toString(); } - + /** - * Enumerates the possible outcomes of an attempt - * to find a model for a FOL formula. + * Enumerates the possible outcomes of an attempt to find a model for a FOL + * formula. */ public static enum Outcome { /** The formula is satisfiable with respect to the specified bounds. */ SATISFIABLE, /** The formula is unsatisfiable with respect to the specified bounds. */ UNSATISFIABLE, - /** - * The formula is trivially satisfiable with respect to the specified bounds: - * a series of simple transformations reduces the formula to the constant TRUE. + /** + * The formula is trivially satisfiable with respect to the specified bounds: a + * series of simple transformations reduces the formula to the constant TRUE. **/ TRIVIALLY_SATISFIABLE, /** * The formula is trivially unsatisfiable with respect to the specified bounds: - * a series of simple transformations reduces the formula to the constant FALSE. + * a series of simple transformations reduces the formula to the constant FALSE. */ TRIVIALLY_UNSATISFIABLE; - + } - + + /** + * Set the output. This file is logged in the message window + * + * @param f a file or null + */ + public void setOutput(File f) { + this.output = f; + } + + public Optional getOutput() { + return Optional.ofNullable(this.output); + } + } diff --git a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/TemporalPardinusSolver.java b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/TemporalPardinusSolver.java index f83fe35b2..f8226a39b 100644 --- a/org.alloytools.pardinus.core/src/main/java/kodkod/engine/TemporalPardinusSolver.java +++ b/org.alloytools.pardinus.core/src/main/java/kodkod/engine/TemporalPardinusSolver.java @@ -184,7 +184,7 @@ public Solution solve(Formula formula, PardinusBounds bounds) throws HigherOrder stats.update(translation, transTime, solveTime); } - return isSat ? sat(translation, stats, bounds) : unsat(translation, stats); + return isSat? sat(translation, stats, bounds) : unsat(translation, stats); } catch (SATAbortedException sae) { throw new AbortedException(sae); } @@ -209,12 +209,11 @@ public Explorer solveAll(Formula formula, PardinusBounds bounds) throw private void flushFormula(Formula formula, Bounds bounds) { try { File f = new File(System.getProperty("java.io.tmpdir"), "kk.txt"); - OutputStream os = new BufferedOutputStream(new FileOutputStream(f)); - os.write(PrettyPrinter.print(formula, 2).getBytes()); - os.write("\n================\n".getBytes()); - os.write(bounds.toString().getBytes()); - os.flush(); - os.close(); + try (OutputStream os = new BufferedOutputStream(new FileOutputStream(f))) { + os.write(PrettyPrinter.print(formula, 2).getBytes()); + os.write("\n================\n".getBytes()); + os.write(bounds.toString().getBytes()); + } } catch (Exception e) { } } 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 b3c10d5dd..43a7d6b5b 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 @@ -82,76 +82,8 @@ public abstract class SATFactory implements Serializable, Comparable public static List extensions = new ArrayList<>(); public static final SATFactory DEFAULT = SAT4JRef.INSTANCE; - /** - * A special SATFactory, will indicate output of the KodKod/Pardinus code to a - * file - */ - public final static SATFactory KK = new SAT4JRef() { - private static final long serialVersionUID = 1L; - - @Override - public String id() { - return "KK"; - } - - @Override - public String name() { - return "KodKod output"; - } - - @Override - public Optional getDescription() { - return Optional.of("KK is the KodKod debug output format"); - } - - public String type() { - return "synthetic"; - } - - @Override - public boolean incremental() { - return false; - } - - }; - - /** - * A special SATFactory, will indicate output of the CNF DIMACS file - */ - public final static SATFactory CNF = new SAT4JRef() { - private static final long serialVersionUID = 1L; - - @Override - 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 type() { - return "synthetic"; - } - - @Override - public boolean incremental() { - return false; - } - - }; - static { extensions.add(DEFAULT); - extensions.add(KK); - extensions.add(CNF); extensions.add(LightSat4JRef.INSTANCE); extensions.add(PMaxSAT4JRef.INSTANCE); } @@ -174,6 +106,9 @@ public String check() { if (!isPresent()) return "cannot be found"; + if ( isTransformer()) + return ""; + SATSolver solver = null; try { solver = instance(); @@ -200,7 +135,9 @@ public String check() { * * @return a SATSolver instance */ - public abstract SATSolver instance(); + public SATSolver instance() { + throw new UnsupportedOperationException(this + " is not a SATFactory that can create instances"); + } /** * Returns true if the solvers returned by this.instance() are {@link SATProver @@ -288,6 +225,9 @@ public static List getAllSolvers() { * Check if the SATFactory is present */ public boolean isPresent() { + if ( isTransformer()) + return true; + try { instance(); for (String library : getLibraries()) { @@ -400,4 +340,9 @@ public String name() { return id(); } + public boolean isTransformer() { + return false; + } + + } diff --git a/org.alloytools.pardinus.native/bnd.bnd b/org.alloytools.pardinus.native/bnd.bnd index 68ceb1205..e21cd377e 100644 --- a/org.alloytools.pardinus.native/bnd.bnd +++ b/org.alloytools.pardinus.native/bnd.bnd @@ -1,5 +1,6 @@ -includeresource \ native=native, \ - LICENSES=LICENSES, \ - META-INF/services=services --buildpath: org.alloytools.pardinus.core \ No newline at end of file + LICENSES=LICENSES +-buildpath: \ + org.alloytools.pardinus.core,\ + biz.aQute.bnd.annotation \ No newline at end of file diff --git a/org.alloytools.pardinus.native/services/kodkod.engine.satlab.SATFactory b/org.alloytools.pardinus.native/services/kodkod.engine.satlab.SATFactory deleted file mode 100644 index dc3c64ba1..000000000 --- a/org.alloytools.pardinus.native/services/kodkod.engine.satlab.SATFactory +++ /dev/null @@ -1,8 +0,0 @@ -org.alloytools.solvers.natv.glucose.GlucoseRef -org.alloytools.solvers.natv.lingeling.PlingelingRef -org.alloytools.solvers.natv.minisat.MiniSatRef -org.alloytools.solvers.natv.minisatprover.MiniSatProverRef -org.alloytools.solvers.natv.yices.YicesRef -org.alloytools.solvers.natv.yices.YicesExternalRef -org.alloytools.solvers.natv.electrod.ElectrodNuSMVRef -org.alloytools.solvers.natv.electrod.ElectrodNuXmvRef diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuSMVRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuSMVRef.java index 8965d555b..2f01a9d0e 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuSMVRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuSMVRef.java @@ -2,6 +2,10 @@ import java.util.Optional; +import aQute.bnd.annotation.spi.ServiceProvider; +import kodkod.engine.satlab.SATFactory; + +@ServiceProvider(SATFactory.class ) public class ElectrodNuSMVRef extends ElectrodRef { private static final long serialVersionUID = 1L; @@ -21,4 +25,9 @@ public String id() { public Optional getDescription() { return Optional.ofNullable("`nuSMV` is a reimplementation and extension of `SMV`, the original Symbolic Model Verifier developed at Carnegie Mellon University. It is a software tool for the formal verification of finite state systems, which can be used to check specifications of hardware and software systems. `nuSMV` allows users to describe systems in a high-level input language and to specify properties to be verified using temporal logics such as CTL (Computation Tree Logic) and LTL (Linear Temporal Logic). The tool uses symbolic model checking techniques, including Binary Decision Diagrams (BDDs), to efficiently verify complex systems against the given specifications. It supports various analysis modes, including model checking, interactive simulation, and counterexample generation, facilitating the detection and diagnosis of design errors."); } + + @Override + public String check() { + return "todo: need to check electrod/NuSMV combination in some way"; + } } diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuXmvRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuXmvRef.java index 05aeee5d3..f65450ab2 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuXmvRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodNuXmvRef.java @@ -2,6 +2,10 @@ import java.util.Optional; +import aQute.bnd.annotation.spi.ServiceProvider; +import kodkod.engine.satlab.SATFactory; + +@ServiceProvider(SATFactory.class ) public class ElectrodNuXmvRef extends ElectrodRef { private static final long serialVersionUID = 1L; @@ -22,4 +26,9 @@ public Optional getDescription() { return Optional.of("nuXmv is a symbolic model checker for formal verification of finite state and infinite state systems. It extends and replaces the nuSMV tool, inheriting its features while introducing new functionalities and improvements. nuXmv can analyze both hardware designs and software specifications, supporting temporal logics like CTL (Computation Tree Logic) and LTL (Linear Temporal Logic) for specification of properties. It employs advanced techniques such as SAT-based and BDD-based symbolic model checking, making it effective for verifying complex systems."); } + @Override + public String check() { + return "todo: need to check electrod/nuXmv combination in some way"; + } + } diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodReader.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodReader.java index 679579695..f93cd98f3 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodReader.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodReader.java @@ -23,8 +23,12 @@ package org.alloytools.solvers.natv.electrod; import java.io.IOException; +import java.io.Reader; +import java.io.StringReader; import java.util.ArrayList; import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; import javax.xml.parsers.DocumentBuilder; import javax.xml.parsers.DocumentBuilderFactory; @@ -34,6 +38,7 @@ import org.w3c.dom.Element; import org.w3c.dom.Node; import org.w3c.dom.NodeList; +import org.xml.sax.InputSource; import org.xml.sax.SAXException; import kodkod.ast.Relation; @@ -62,7 +67,7 @@ public class ElectrodReader { /** * Initializes the Electrod solution reader with the original problem bounds. - * + * * @param bounds the original bounds of the solved problem. */ public ElectrodReader(PardinusBounds bounds) { @@ -75,22 +80,30 @@ public ElectrodReader(PardinusBounds bounds) { * Reads an Electrod solution from an XML file, creating a temporal instance * that can be processed by Kodkod/Pardinus. Returns null if the problem is * unsatisfiable. - * - * @param file the XML Electrod solution to be parsed. + * + * @param string the XML Electrod solution to be parsed. * @return the parsed temporal instance or null if unsat. * @throws InvalidUnboundedSolution if the parsing fails. */ - public TemporalInstance read(String file) throws InvalidUnboundedSolution { + public TemporalInstance read(String string) throws InvalidUnboundedSolution { + return read(new StringReader(string)); + } + + public TemporalInstance read(Reader reader) throws InvalidUnboundedSolution { + return read(new InputSource(reader)); + } + + public TemporalInstance read(InputSource source) throws InvalidUnboundedSolution { DocumentBuilderFactory factory = DocumentBuilderFactory.newInstance(); factory.setValidating(false); factory.setIgnoringElementContentWhitespace(true); try { DocumentBuilder builder = factory.newDocumentBuilder(); - Document doc = builder.parse(file); + Document doc = builder.parse(source); Element root = doc.getDocumentElement(); nbvars = Integer.valueOf(root.getAttributes().getNamedItem("nbvars").getNodeValue()); - ctime = Integer.valueOf(root.getAttributes().getNamedItem("conversion-time").getNodeValue()); - atime = Integer.valueOf(root.getAttributes().getNamedItem("analysis-time").getNodeValue()); + ctime = getMillis(root.getAttributes().getNamedItem("conversion-time").getNodeValue()); + atime = getMillis(root.getAttributes().getNamedItem("analysis-time").getNodeValue()); NodeList elems = root.getChildNodes(); int c = 0; for (int i = 0; i < elems.getLength(); i++) { @@ -110,11 +123,38 @@ public TemporalInstance read(String file) throws InvalidUnboundedSolution { return new TemporalInstance(insts, loop, 1); } + final static Pattern DURATION_P = Pattern.compile("(?\\d+(\\.\\d+)?)(?.*)?"); + + private int getMillis(String nodeValue) { + try { + return Integer.valueOf(nodeValue); + } catch (NumberFormatException e) { + Matcher m = DURATION_P.matcher(nodeValue); + if (m.matches()) { + double val = Double.valueOf(m.group("val")); + String unit = m.group("unit"); + if (unit == null) + return (int) val; + switch (unit) { + default : + case "ms" : + return (int) val; + case "s" : + return (int) (val * 1000); + case "m" : + return (int) (val * 60_000); + } + } else { + return Integer.MAX_VALUE; + } + } + } + /** * Parses a single state of the trace as a static regular Kodkod {@link Instance * instance}. Atoms and relations may have been renamed by * {@link ElectrodPrinter#normRel(String)}, which must be reverted. - * + * * @param node the XML node containing the state. * @return the static instance corresponding to the state. */ diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodRef.java index 508afb024..59b55e0ea 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodRef.java @@ -4,6 +4,7 @@ import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.util.List; +import java.util.Map; import java.util.stream.Collectors; import kodkod.ast.Formula; @@ -28,8 +29,8 @@ abstract class ElectrodRef extends SATFactory implements TemporalSolverFactory { private static final long serialVersionUID = 1L; - final String electrod; - final String solver; + final File electrod; + final File solver; final String solverId; class ElectrodSolver implements UnboundedSolver, TemporalSolver { @@ -65,19 +66,33 @@ public Solution solve(Formula formula, PardinusBounds bounds) throws InvalidUnbo options.reporter().solvingCNF(-1, -1, -1, -1); String electrod = ElectrodPrinter.print(formula, bounds, rep); - String xml = execute(this, electrod, bounds); - ElectrodReader rd = new ElectrodReader(bounds); - TemporalInstance temporalInstance = rd.read(xml); - Statistics stats = new Statistics(rd.nbvars, 0, 0, rd.ctime, rd.atime); - return temporalInstance == null ? Solution.unsatisfiable(stats, null) : Solution.satisfiable(stats, temporalInstance); + Solution solution; + if (solverId == null) { + try { + solution = Solution.unsatisfiable(null, null); + File f = Files.createTempFile(options.uniqueName(), ".elo").toFile(); + write(f, electrod); + solution.setOutput(f); + return solution; + } catch (Exception e) { + throw new RuntimeException(e); + } + } else { + String xml = execute(this, electrod, bounds); + ElectrodReader rd = new ElectrodReader(bounds); + TemporalInstance temporalInstance = rd.read(xml); + Statistics stats = new Statistics(rd.nbvars, 0, 0, rd.ctime, rd.atime); + solution = temporalInstance == null ? Solution.unsatisfiable(stats, null) : Solution.satisfiable(stats, temporalInstance); + } + return solution; } } ElectrodRef(String solver) { solverId = solver; - this.electrod = NativeCode.platform.getExecutable("electrod").map(File::getAbsolutePath).orElse(null); - this.solver = NativeCode.platform.getExecutable(solver).map(File::getAbsolutePath).orElse(null); + this.electrod = NativeCode.platform.getExecutable("electrod").orElse(null); + this.solver = solverId == null ? null : NativeCode.platform.getExecutable(solver).orElse(null); } @Override @@ -130,10 +145,12 @@ String execute(ElectrodSolver electrodSolver, String elo, PardinusBounds bounds) Exception exception = null; int exitCode = Integer.MAX_VALUE; ProcessBuilder processBuilder = new ProcessBuilder(); + Map environment = processBuilder.environment(); + environment.put("PATH", addSolverToPath(environment.get("PATH"), solver)); List args = processBuilder.command(); - args.add(electrod); + args.add(electrod.getAbsolutePath()); args.add("-t"); - args.add(solver); + args.add(solverId); ExtendedOptions options = electrodSolver.options(); if (!options.unbounded()) { @@ -144,8 +161,9 @@ String execute(ElectrodSolver electrodSolver, String elo, PardinusBounds bounds) try { File tempDir = Files.createTempDirectory(options.uniqueName()).toFile(); File eloFile = new File(tempDir, "output.elo"); + write(eloFile, elo); File out = new File(tempDir, ".out"); - args.add(elo); + args.add(eloFile.getAbsolutePath()); processBuilder.redirectError(out); processBuilder.redirectOutput(out); reporter.debug("starting electrod process with : " + args); @@ -175,7 +193,15 @@ String execute(ElectrodSolver electrodSolver, String elo, PardinusBounds bounds) throw new AbortedException(report); } - private String read(File file) { + private String addSolverToPath(String PATH, File solverPath) { + String dir = solverPath.getParent(); + if (PATH == null) { + return dir; + } else + return dir + File.pathSeparator + PATH; + } + + private String read(File file) throws Exception { try { if (file != null && file.isFile()) { byte[] allBytes = Files.readAllBytes(file.toPath()); @@ -187,5 +213,8 @@ private String read(File file) { return "no file " + file; } + private void write(File file, String contents) throws Exception { + Files.write(file.toPath(), contents.getBytes(StandardCharsets.UTF_8)); + } } diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodTransformerRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodTransformerRef.java new file mode 100644 index 000000000..9b65c681b --- /dev/null +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/electrod/ElectrodTransformerRef.java @@ -0,0 +1,51 @@ +package org.alloytools.solvers.natv.electrod; + +import java.util.Optional; + +import aQute.bnd.annotation.spi.ServiceProvider; +import kodkod.engine.satlab.SATFactory; + +@ServiceProvider(SATFactory.class ) +public class ElectrodTransformerRef extends ElectrodRef { + + private static final long serialVersionUID = 1L; + + + public ElectrodTransformerRef() { + super(null); + } + + @Override + public String id() { + return "electrod.elo"; + } + + + @Override + public Optional getDescription() { + return Optional.ofNullable("outputs the elo file generated for electrod"); + } + + @Override + public boolean isPresent() { + return electrod != null; + } + + @Override + public String[] getExecutables() { + return new String[] { + "electrod" + }; + } + + @Override + public boolean isTransformer() { + return true; + } + + @Override + public String type() { + return "transformer"; + } + +} diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/glucose/GlucoseRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/glucose/GlucoseRef.java index 4fe4e801c..e050d5330 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/glucose/GlucoseRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/glucose/GlucoseRef.java @@ -2,9 +2,11 @@ import java.util.Optional; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.SATSolver; +@ServiceProvider(SATFactory.class ) public class GlucoseRef extends SATFactory { private static final long serialVersionUID = 1L; diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/lingeling/PlingelingRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/lingeling/PlingelingRef.java index bddce2392..963c5589c 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/lingeling/PlingelingRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/lingeling/PlingelingRef.java @@ -2,10 +2,12 @@ import java.util.Optional; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.satlab.ExternalSolver; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.SATSolver; +@ServiceProvider(SATFactory.class ) public class PlingelingRef extends SATFactory { private static final long serialVersionUID = 1L; diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisat/MiniSatRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisat/MiniSatRef.java index a6b755389..dc8820727 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisat/MiniSatRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisat/MiniSatRef.java @@ -2,9 +2,11 @@ import java.util.Optional; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.SATSolver; +@ServiceProvider(SATFactory.class ) public class MiniSatRef extends SATFactory { private static final long serialVersionUID = 1L; diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisatprover/MiniSatProverRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisatprover/MiniSatProverRef.java index 280f64291..e310ca78f 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisatprover/MiniSatProverRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/minisatprover/MiniSatProverRef.java @@ -1,9 +1,11 @@ package org.alloytools.solvers.natv.minisatprover; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.config.ExtendedOptions; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.SATSolver; +@ServiceProvider(SATFactory.class ) public class MiniSatProverRef extends SATFactory { private static final long serialVersionUID = 1L; diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesExternalRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesExternalRef.java index 0609ba13e..f2161ccb4 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesExternalRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesExternalRef.java @@ -1,8 +1,10 @@ package org.alloytools.solvers.natv.yices; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.satlab.SATFactory; import kodkod.engine.satlab.WTargetSATSolver; +@ServiceProvider(SATFactory.class ) public class YicesExternalRef extends SATFactory { private static final long serialVersionUID = 1L; diff --git a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesRef.java b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesRef.java index b560d589d..def029b40 100644 --- a/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesRef.java +++ b/org.alloytools.pardinus.native/src/main/java/org/alloytools/solvers/natv/yices/YicesRef.java @@ -1,7 +1,9 @@ package org.alloytools.solvers.natv.yices; +import aQute.bnd.annotation.spi.ServiceProvider; import kodkod.engine.satlab.SATFactory; +@ServiceProvider(SATFactory.class ) public class YicesRef extends SATFactory { private static final long serialVersionUID = 1L;