From fdce4bea5f2df82078a25f876964ba664735e6b0 Mon Sep 17 00:00:00 2001 From: nmacedo Date: Fri, 3 Jun 2016 12:04:11 +0100 Subject: [PATCH] documentation --- .../alloy4compiler/translator/A4Solution.java | 2190 +++++++++-------- .../translator/A4SolutionReader.java | 10 +- .../translator/A4SolutionWriter.java | 20 +- .../translator/ScopeComputer.java | 16 +- .../translator/TranslateAlloyToKodkod.java | 15 +- .../mit/csail/sdg/alloy4viz/AlloyType.java | 5 +- .../sdg/alloy4viz/StaticInstanceReader.java | 12 +- .../csail/sdg/alloy4viz/VizGraphPanel.java | 8 +- .../csail/sdg/alloy4whole/SimpleReporter.java | 8 +- 9 files changed, 1163 insertions(+), 1121 deletions(-) diff --git a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java index 8ba7df83..d8f90956 100644 --- a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java +++ b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4Solution.java @@ -1,5 +1,6 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang - * + * Electrum -- Copyright (c) 2014-present, Nuno Macedo + * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is @@ -97,1118 +98,1125 @@ /** This class stores a SATISFIABLE or UNSATISFIABLE solution. * It is also used as a staging area for the solver before generating the solution. * Once solve() has been called, then this object becomes immutable after that. + * + * @modified: nmm */ public final class A4Solution { - //====== static immutable fields ====================================================================// + //====== static immutable fields ====================================================================// + + /** The constant unary relation representing the smallest Int atom. */ + static final Relation KK_MIN = Relation.unary("Int/min"); + + /** The constant unary relation representing the Int atom "0". */ + static final Relation KK_ZERO = Relation.unary("Int/zero"); + + /** The constant unary relation representing the largest Int atom. */ + static final Relation KK_MAX = Relation.unary("Int/max"); + + /** The constant binary relation representing the "next" relation from each Int atom to its successor. */ + static final Relation KK_NEXT = Relation.binary("Int/next"); + + /** The constant unary relation representing the set of all seq/Int atoms. */ + static final Relation KK_SEQIDX = Relation.unary("seq/Int"); - /** The constant unary relation representing the smallest Int atom. */ - static final Relation KK_MIN = Relation.unary("Int/min"); + /** The constant unary relation representing the set of all String atoms. */ + static final Relation KK_STRING = Relation.unary("String"); - /** The constant unary relation representing the Int atom "0". */ - static final Relation KK_ZERO = Relation.unary("Int/zero"); + /** The constant unary relation representing the set of all Time atoms. */ + static final Relation KK_TIME = Relation.unary("Time"); // pt.uminho.haslab: time relations (deprecated) - /** The constant unary relation representing the largest Int atom. */ - static final Relation KK_MAX = Relation.unary("Int/max"); + /** The constant binary relation representing the "next" relation from each Time atom to its successor. */ + static final Relation KK_TIMENEXT = Relation.binary("Time/next"); // pt.uminho.haslab: time relations (deprecated) + static final Relation KK_TIMEINIT = Relation.unary("Time/init"); // pt.uminho.haslab: time relations (deprecated) + static final Relation KK_TIMEEND = Relation.unary("Time/end"); // pt.uminho.haslab: time relations (deprecated) + static final Relation KK_TIMELOOP = Relation.binary("Time/loop"); // pt.uminho.haslab: time relations (deprecated) - /** The constant binary relation representing the "next" relation from each Int atom to its successor. */ - static final Relation KK_NEXT = Relation.binary("Int/next"); - /** The constant unary relation representing the set of all seq/Int atoms. */ - static final Relation KK_SEQIDX = Relation.unary("seq/Int"); + //====== immutable fields ===========================================================================// - /** The constant unary relation representing the set of all String atoms. */ - static final Relation KK_STRING = Relation.unary("String"); + /** The original Alloy options that generated this solution. */ + private final A4Options originalOptions; - /** The constant unary relation representing the set of all String atoms. */ - static final Relation KK_TIME = Relation.unary("Time"); // pt.uminho.haslab - - /** The constant binary relation representing the "next" relation from each Int atom to its successor. */ - static final Relation KK_TIMENEXT = Relation.binary("Time/next"); - static final Relation KK_TIMEINIT = Relation.unary("Time/init"); - static final Relation KK_TIMEEND = Relation.unary("Time/end"); - static final Relation KK_TIMELOOP = Relation.binary("Time/loop"); + /** The original Alloy command that generated this solution; can be "" if unknown. */ + private final String originalCommand; + /** The bitwidth; always between 1 and 30. */ + private final int bitwidth; - //====== immutable fields ===========================================================================// + /** The maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ + private final int maxseq; - /** The original Alloy options that generated this solution. */ - private final A4Options originalOptions; + /** The maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ + private final int time; // pt.uminho.haslab: time scopes + private int loop; // pt.uminho.haslab: time scopes - /** The original Alloy command that generated this solution; can be "" if unknown. */ - private final String originalCommand; - /** The bitwidth; always between 1 and 30. */ - private final int bitwidth; + /** The maximum allowed number of loop unrolling and recursion level. */ + private final int unrolls; - /** The maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ - private final int maxseq; - - /** The maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ - private final int time; // pt.uminho.haslab - private int loop; // pt.uminho.haslab + /** The list of all atoms. */ + private final ConstList kAtoms; + /** The Kodkod TupleFactory object. */ + private final TupleFactory factory; - /** The maximum allowed number of loop unrolling and recursion level. */ - private final int unrolls; + /** The set of all Int atoms; immutable. */ + private final TupleSet sigintBounds; - /** The list of all atoms. */ - private final ConstList kAtoms; + /** The set of all seq/Int atoms; immutable. */ + private final TupleSet seqidxBounds; - /** The Kodkod TupleFactory object. */ - private final TupleFactory factory; + /** The set of all String atoms; immutable. */ + private final TupleSet stringBounds; - /** The set of all Int atoms; immutable. */ - private final TupleSet sigintBounds; + /** The set of all String atoms; immutable. */ + private final TupleSet timeBounds; // pt.uminho.haslab: time scopes - /** The set of all seq/Int atoms; immutable. */ - private final TupleSet seqidxBounds; + /** The Kodkod Solver object. */ + private final Solver solver; - /** The set of all String atoms; immutable. */ - private final TupleSet stringBounds; - - /** The set of all String atoms; immutable. */ - private final TupleSet timeBounds; // pt.uminho.haslab - - /** The Kodkod Solver object. */ - private final Solver solver; - - //====== mutable fields (immutable after solve() has been called) ===================================// - - /** True iff the problem is solved. */ - private boolean solved = false; - - /** The Kodkod Bounds object. */ - private Bounds bounds; - - /** The list of Kodkod formulas; can be empty if unknown; once a solution is solved we must not modify this anymore */ - private ArrayList formulas = new ArrayList(); - - /** The list of known Alloy4 sigs. */ - private SafeList sigs; - - /** If solved==true and is satisfiable, then this is the list of known skolems. */ - private SafeList skolems = new SafeList(); - - /** If solved==true and is satisfiable, then this is the list of actually used atoms. */ - private SafeList atoms = new SafeList(); - - /** If solved==true and is satisfiable, then this maps each Kodkod atom to a short name. */ - private Map atom2name = new LinkedHashMap(); - - /** If solved==true and is satisfiable, then this maps each Kodkod atom to its most specific sig. */ - private Map atom2sig = new LinkedHashMap(); - - /** If solved==true and is satisfiable, then this is the Kodkod evaluator. */ - private Evaluator eval = null; - - /** If not null, you can ask it to get another solution. */ - private Iterator kEnumerator = null; - - /** The map from each Sig/Field/Skolem/Atom to its corresponding Kodkod expression. */ - private Map a2k; - - /** The map from each String literal to its corresponding Kodkod expression. */ - private final ConstMap s2k; - - /** The map from each kodkod Formula to Alloy Expr or Alloy Pos (can be empty if unknown) */ - private Map k2pos; - - /** The map from each Kodkod Relation to Alloy Type (can be empty or incomplete if unknown) */ - private Map rel2type; - - /** The map from each Kodkod Variable to an Alloy Type and Alloy Pos. */ - private Map> decl2type; - - //===================================================================================================// - - /** Construct a blank A4Solution containing just UNIV, SIGINT, SEQIDX, STRING, and NONE as its only known sigs. - * @param originalCommand - the original Alloy command that generated this solution; can be "" if unknown - * @param bitwidth - the bitwidth; must be between 1 and 30 - * @param maxseq - the maximum allowed sequence length; must be between 0 and (2^(bitwidth-1))-1 - * @param time TODO - * @param loop TODO - * @param atoms - the set of atoms - * @param rep - the reporter that will receive diagnostic and progress messages - * @param opt - the Alloy options that will affect the solution and the solver - * @param expected - whether the user expected an instance or not (1 means yes, 0 means no, -1 means the user did not express an expectation) - */ - A4Solution(String originalCommand, int bitwidth, int maxseq, Set stringAtoms, int time, int loop, Collection atoms, final A4Reporter rep, A4Options opt, int expected) throws Err { //pt.uminho.haslab - opt = opt.dup(); - this.unrolls = opt.unrolls; - this.sigs = new SafeList(Arrays.asList(UNIV, SIGINT, SEQIDX, STRING, NONE, TIME)); //pt.uminho.haslab - this.a2k = Util.asMap(new Expr[]{UNIV, SIGINT, SEQIDX, STRING, NONE, TIME}, Relation.INTS.union(KK_STRING).union(KK_TIME), Relation.INTS, KK_SEQIDX, KK_STRING, Relation.NONE, KK_TIME); //pt.uminho.haslab - this.k2pos = new LinkedHashMap(); - this.rel2type = new LinkedHashMap(); - this.decl2type = new LinkedHashMap>(); - this.originalOptions = opt; - this.originalCommand = (originalCommand==null ? "" : originalCommand); - this.bitwidth = bitwidth; - this.maxseq = maxseq; - this.time = time; //pt.uminho.haslab - this.loop = loop; //pt.uminho.haslab - if (bitwidth < 0) throw new ErrorSyntax("Cannot specify a bitwidth less than 0"); - if (bitwidth > 30) throw new ErrorSyntax("Cannot specify a bitwidth greater than 30"); - if (maxseq < 0) throw new ErrorSyntax("The maximum sequence length cannot be negative."); - if (maxseq > 0 && maxseq > max()) throw new ErrorSyntax("With integer bitwidth of "+bitwidth+", you cannot have sequence length longer than "+max()); - if (atoms.isEmpty()) { - atoms = new ArrayList(1); - atoms.add(""); - } - kAtoms = ConstList.make(atoms); - bounds = new Bounds(new Universe(kAtoms)); - factory = bounds.universe().factory(); - TupleSet sigintBounds = factory.noneOf(1); - TupleSet seqidxBounds = factory.noneOf(1); - TupleSet stringBounds = factory.noneOf(1); - TupleSet timeBounds = factory.noneOf(1); - final TupleSet next = factory.noneOf(2); - final TupleSet timenext = factory.noneOf(2); - final TupleSet timeback = factory.noneOf(2); - int min=min(), max=max(); - if (max >= min) for(int i=min; i<=max; i++) { // Safe since we know 1 <= bitwidth <= 30 - Tuple ii = factory.tuple(""+i); - TupleSet is = factory.range(ii, ii); - bounds.boundExactly(i, is); - sigintBounds.add(ii); - if (i>=0 && i s2k = new HashMap(); - for(String e: stringAtoms) { - Relation r = Relation.unary(""); - Tuple t = factory.tuple(e); - s2k.put(e, r); - bounds.boundExactly(r, factory.range(t, t)); - stringBounds.add(t); - } - this.s2k = ConstMap.make(s2k); - this.stringBounds = stringBounds.unmodifiableView(); - bounds.boundExactly(KK_STRING, this.stringBounds); - if (time < 1) { - bounds.boundExactly(KK_TIMEINIT, factory.noneOf(1)); - bounds.boundExactly(KK_TIMEEND, factory.noneOf(1)); - bounds.boundExactly(KK_TIMELOOP, factory.noneOf(2)); - bounds.boundExactly(KK_TIMENEXT, factory.noneOf(2)); - } else { - for(int i=0; i= 0) { - timeback.add(factory.tuple("Time$"+(time-1),"Time$"+loop)); - bounds.boundExactly(KK_TIMELOOP, timeback); - timeback.addAll(timenext); - bounds.boundExactly(KK_TIMENEXT, timeback); - } else { - bounds.bound(KK_TIMELOOP, timeback); - timeback.addAll(timenext); - bounds.bound(KK_TIMENEXT, timenext, timeback); - } - } - this.timeBounds = timeBounds.unmodifiableView(); - bounds.boundExactly(KK_TIME, this.timeBounds); - int sym = (expected==1 ? 0 : opt.symmetry); - solver = new Solver(); - solver.options().setNoOverflow(opt.noOverflow); - solver.options().setFlatten(false); // added for now, since multiplication and division circuit takes forever to flatten - if (opt.solver.external()!=null) { - String ext = opt.solver.external(); - if (opt.solverDirectory.length()>0 && ext.indexOf(File.separatorChar)<0) ext=opt.solverDirectory+File.separatorChar+ext; - try { - File tmp = File.createTempFile("tmp", ".cnf", new File(opt.tempDirectory)); - tmp.deleteOnExit(); - solver.options().setSolver(SATFactory.externalFactory(ext, tmp.getAbsolutePath(), "", opt.solver.options())); - //solver.options().setSolver(SATFactory.externalFactory(ext, tmp.getAbsolutePath(), opt.solver.options())); - } catch(IOException ex) { throw new ErrorFatal("Cannot create temporary directory.", ex); } - } else if (opt.solver.equals(A4Options.SatSolver.ZChaffJNI)) { - solver.options().setSolver(SATFactory.ZChaff); - } else if (opt.solver.equals(A4Options.SatSolver.MiniSatJNI)) { - solver.options().setSolver(SATFactory.MiniSat); - } else if (opt.solver.equals(A4Options.SatSolver.MiniSatProverJNI)) { - sym=20; - solver.options().setSolver(SATFactory.MiniSatProver); - solver.options().setLogTranslation(2); - solver.options().setCoreGranularity(opt.coreGranularity); - } else { - solver.options().setSolver(SATFactory.DefaultSAT4J); // Even for "KK" and "CNF", we choose SAT4J here; later, just before solving, we'll change it to a Write2CNF solver - } - solver.options().setSymmetryBreaking(sym); - solver.options().setSkolemDepth(opt.skolemDepth); - solver.options().setBitwidth(bitwidth > 0 ? bitwidth : (int) Math.ceil(Math.log(atoms.size())) + 1); - solver.options().setIntEncoding(Options.IntEncoding.TWOSCOMPLEMENT); - } - - /** Construct a new A4Solution that is the continuation of the old one, but with the "next" instance. */ - private A4Solution(A4Solution old) throws Err { - if (!old.solved) throw new ErrorAPI("This solution is not yet solved, so next() is not allowed."); - if (old.kEnumerator==null) throw new ErrorAPI("This solution was not generated by an incremental SAT solver.\n" + "Solution enumeration is currently only implemented for MiniSat and SAT4J."); - if (old.eval==null) throw new ErrorAPI("This solution is already unsatisfiable, so you cannot call next() to get the next solution."); - Instance inst = old.kEnumerator.next().instance(); - unrolls = old.unrolls; - originalOptions = old.originalOptions; - originalCommand = old.originalCommand; - bitwidth = old.bitwidth; - time = old.time; // pt.uminho.haslab - loop = old.loop; // pt.uminho.haslab - maxseq = old.maxseq; - kAtoms = old.kAtoms; - factory = old.factory; - sigintBounds = old.sigintBounds; - seqidxBounds = old.seqidxBounds; - stringBounds = old.stringBounds; - timeBounds = old.timeBounds; // pt.uminho.haslab - solver = old.solver; - bounds = old.bounds; - formulas = old.formulas; - sigs = old.sigs; - kEnumerator = old.kEnumerator; - k2pos = old.k2pos; - rel2type = old.rel2type; - decl2type = old.decl2type; - if (inst!=null) { - eval = new Evaluator(inst, old.solver.options()); - a2k = new LinkedHashMap(); - for(Map.Entry e: old.a2k.entrySet()) - if (e.getKey() instanceof Sig || e.getKey() instanceof Field) - a2k.put(e.getKey(), e.getValue()); - UniqueNameGenerator un = new UniqueNameGenerator(); - rename(this, null, null, un); - a2k = ConstMap.make(a2k); - } else { - skolems = old.skolems; - eval = null; - a2k = old.a2k; - } - s2k = old.s2k; - atoms = atoms.dup(); - atom2name = ConstMap.make(atom2name); - atom2sig = ConstMap.make(atom2sig); - solved = true; - } - - /** Turn the solved flag to be true, and make all remaining fields immutable. */ - private void solved() { - if (solved) return; // already solved - bounds = bounds.clone().unmodifiableView(); - sigs = sigs.dup(); - skolems = skolems.dup(); - atoms = atoms.dup(); - atom2name = ConstMap.make(atom2name); - atom2sig = ConstMap.make(atom2sig); - a2k = ConstMap.make(a2k); - k2pos = ConstMap.make(k2pos); - rel2type = ConstMap.make(rel2type); - decl2type = ConstMap.make(decl2type); - solved = true; - } - - //===================================================================================================// - - /** Returns the bitwidth; always between 1 and 30. */ - public int getBitwidth() { return bitwidth; } - - /** Returns the maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ - public int getMaxSeq() { return maxseq; } - - public int getTime() { return time; } // pt.uminho.haslab - - public int getLoop() { return loop; } // pt.uminho.haslab - - /** Returns the largest allowed integer, or -1 if no integers are allowed. */ - public int max() { return Util.max(bitwidth); } - - /** Returns the smallest allowed integer, or 0 if no integers are allowed */ - public int min() { return Util.min(bitwidth); } - - /** Returns the maximum number of allowed loop unrolling or recursion level. */ - public int unrolls() { return unrolls; } - - //===================================================================================================// - - /** Returns the original Alloy file name that generated this solution; can be "" if unknown. */ - public String getOriginalFilename() { return originalOptions.originalFilename; } - - /** Returns the original command that generated this solution; can be "" if unknown. */ - public String getOriginalCommand() { return originalCommand; } - - //===================================================================================================// - - /** Returns the Kodkod input used to generate this solution; returns "" if unknown. */ - public String debugExtractKInput() { - if (solved) - return TranslateKodkodToJava.convert(Formula.and(formulas), bitwidth, kAtoms, bounds, atom2name); - else - return TranslateKodkodToJava.convert(Formula.and(formulas), bitwidth, kAtoms, bounds.unmodifiableView(), null); - } - - //===================================================================================================// - - /** Returns the Kodkod TupleFactory object. */ - TupleFactory getFactory() { return factory; } - - /** Returns a modifiable copy of the Kodkod Bounds object. */ - Bounds getBounds() { return bounds.clone(); } - - /** Add a new relation with the given label and the given lower and upper bound. - * @param label - the label for the new relation; need not be unique - * @param lower - the lowerbound; can be null if you want it to be the empty set - * @param upper - the upperbound; cannot be null; must contain everything in lowerbound - */ - Relation addRel(String label, TupleSet lower, TupleSet upper) throws ErrorFatal { - if (solved) throw new ErrorFatal("Cannot add a Kodkod relation since solve() has completed."); - Relation rel = Relation.nary(label, upper.arity()); - if (lower == upper) { - bounds.boundExactly(rel, upper); - } else if (lower == null) { - bounds.bound(rel, upper); - } else { - if (lower.arity() != upper.arity()) throw new ErrorFatal("Relation "+label+" must have same arity for lowerbound and upperbound."); - bounds.bound(rel, lower, upper); - } - return rel; - } - - /** Add a new sig to this solution and associate it with the given expression (and if s.isTopLevel then add this expression into Sig.UNIV). - *
The expression must contain only constant Relations or Relations that are already bound in this solution. - *
(If the sig was already added by a previous call to addSig(), then this call will return immediately without altering what it is associated with) - */ - void addSig(Sig s, Expression expr) throws ErrorFatal { - if (solved) throw new ErrorFatal("Cannot add an additional sig since solve() has completed."); - if (expr.arity()!=1) throw new ErrorFatal("Sig "+s+" must be associated with a unary relational value."); - if (a2k.containsKey(s)) return; - a2k.put(s, expr); - sigs.add(s); - if (s.isTopLevel()) a2k.put(UNIV, a2k.get(UNIV).union(expr)); - } - - /** Add a new field to this solution and associate it with the given expression. - *
The expression must contain only constant Relations or Relations that are already bound in this solution. - *
(If the field was already added by a previous call to addField(), then this call will return immediately without altering what it is associated with) - */ - void addField(Field f, Expression expr) throws ErrorFatal { - if (solved) throw new ErrorFatal("Cannot add an additional field since solve() has completed."); - if (expr.arity()!=f.type().arity()) throw new ErrorFatal("Field "+f+" must be associated with an "+f.type().arity()+"-ary relational value."); - if (a2k.containsKey(f)) return; - a2k.put(f, expr); - } - - /** Add a new skolem to this solution and associate it with the given expression. - *
The expression must contain only constant Relations or Relations that are already bound in this solution. - */ - private ExprVar addSkolem(String label, Type type, Expression expr) throws Err { - if (solved) throw new ErrorFatal("Cannot add an additional skolem since solve() has completed."); - int a = type.arity(); - if (a<1) throw new ErrorFatal("Skolem "+label+" must be associated with a relational value."); - if (a!=expr.arity()) throw new ErrorFatal("Skolem "+label+" must be associated with an "+a+"-ary relational value."); - ExprVar v = ExprVar.make(Pos.UNKNOWN, label, type); - a2k.put(v, expr); - skolems.add(v); - return v; - } - - /** Returns an unmodifiable copy of the map from each Sig/Field/Skolem/Atom to its corresponding Kodkod expression. */ - ConstMap a2k() { return ConstMap.make(a2k); } - - /** Returns an unmodifiable copy of the map from each String literal to its corresponding Kodkod expression. */ - ConstMap s2k() { return s2k; } - - /** Returns the corresponding Kodkod expression for the given Sig, or null if it is not associated with anything. */ - Expression a2k(Sig sig) { return a2k.get(sig); } - - /** Returns the corresponding Kodkod expression for the given Field, or null if it is not associated with anything. */ - Expression a2k(Field field) { return a2k.get(field); } - - /** Returns the corresponding Kodkod expression for the given Atom/Skolem, or null if it is not associated with anything. */ - Expression a2k(ExprVar var) { return a2k.get(var); } - - /** Returns the corresponding Kodkod expression for the given String constant, or null if it is not associated with anything. */ - Expression a2k(String stringConstant) { return s2k.get(stringConstant); } - - /** Returns the corresponding Kodkod expression for the given expression, or null if it is not associated with anything. */ - Expression a2k(Expr expr) throws ErrorFatal { - while(expr instanceof ExprUnary) { - if (((ExprUnary)expr).op==ExprUnary.Op.NOOP) { expr = ((ExprUnary)expr).sub; continue; } - if (((ExprUnary)expr).op==ExprUnary.Op.EXACTLYOF) { expr = ((ExprUnary)expr).sub; continue; } - break; - } - if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.EMPTYNESS) return Expression.NONE; - if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.STRING) return s2k.get(((ExprConstant)expr).string); - if (expr instanceof Sig || expr instanceof Field || expr instanceof ExprVar) return a2k.get(expr); - if (expr instanceof ExprBinary) { - Expr a=((ExprBinary)expr).left, b=((ExprBinary)expr).right; - switch(((ExprBinary)expr).op) { - case ARROW: return a2k(a).product(a2k(b)); - case PLUS: return a2k(a).union(a2k(b)); - case MINUS: return a2k(a).difference(a2k(b)); - //TODO: IPLUS, IMINUS??? - } - } - return null; // Current only UNION, PRODUCT, and DIFFERENCE of Sigs and Fields and ExprConstant.EMPTYNESS are allowed in a defined field's definition. - } - - /** Return a modifiable TupleSet representing a sound overapproximation of the given expression. */ - TupleSet approximate(Expression expression) { - return factory.setOf(expression.arity(), Translator.approximate(expression, bounds, solver.options()).denseIndices()); - } - - /** Query the Bounds object to find the lower/upper bound; throws ErrorFatal if expr is not Relation, nor a {union, product} of Relations. */ - TupleSet query(boolean findUpper, Expression expr, boolean makeMutable) throws ErrorFatal { - if (expr==Relation.NONE) return factory.noneOf(1); - if (expr==Relation.INTS) return makeMutable ? sigintBounds.clone() : sigintBounds; - if (expr==KK_SEQIDX) return makeMutable ? seqidxBounds.clone() : seqidxBounds; - if (expr==KK_STRING) return makeMutable ? stringBounds.clone() : stringBounds; - if (expr==KK_TIME) return makeMutable ? timeBounds.clone() : timeBounds; // pt.uminho.haslab - if (expr instanceof Relation) { - TupleSet ans = findUpper ? bounds.upperBound((Relation)expr) : bounds.lowerBound((Relation)expr); - if (ans!=null) return makeMutable ? ans.clone() : ans; - } - else if (expr instanceof BinaryExpression) { - BinaryExpression b = (BinaryExpression)expr; - if (b.op() == ExprOperator.UNION) { - TupleSet left = query(findUpper, b.left(), true); - TupleSet right = query(findUpper, b.right(), false); - left.addAll(right); - return left; - } else if (b.op() == ExprOperator.PRODUCT) { - TupleSet left = query(findUpper, b.left(), true); - TupleSet right = query(findUpper, b.right(), false); - return left.product(right); - } - } - throw new ErrorFatal("Unknown expression encountered during bounds computation: "+expr); - } - - /** Shrink the bounds for the given relation; throws an exception if the new bounds is not sameAs/subsetOf the old bounds. */ - void shrink(Relation relation, TupleSet lowerBound, TupleSet upperBound) throws Err { - if (solved) throw new ErrorFatal("Cannot shrink a Kodkod relation since solve() has completed."); - TupleSet oldL = bounds.lowerBound(relation); - TupleSet oldU = bounds.upperBound(relation); - if (oldU.containsAll(upperBound) && upperBound.containsAll(lowerBound) && lowerBound.containsAll(oldL)) { - bounds.bound(relation, lowerBound, upperBound); - } else { - throw new ErrorAPI("Inconsistent bounds shrinking on relation: "+relation); - } - } - - //===================================================================================================// - - /** Returns true iff the problem has been solved and the result is satisfiable. */ - public boolean satisfiable() { return eval!=null; } - - /** Returns an unmodifiable copy of the list of all sigs in this solution's model; always contains UNIV+SIGINT+SEQIDX+STRING+NONE and has no duplicates. */ - public SafeList getAllReachableSigs() { return sigs.dup(); } - - /** 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(); } - - /** Returns an unmodifiable copy of the list of all atoms if the problem is solved and is satisfiable; else returns an empty list. */ - public Iterable getAllAtoms() { return atoms.dup(); } - - /** Returns the short unique name corresponding to the given atom if the problem is solved and is satisfiable; else returns atom.toString(). */ - String atom2name(Object atom) { String ans=atom2name.get(atom); return ans==null ? atom.toString() : ans; } - - /** Returns the most specific sig corresponding to the given atom if the problem is solved and is satisfiable; else returns UNIV. */ - PrimSig atom2sig(Object atom) { PrimSig sig=atom2sig.get(atom); return sig==null ? UNIV : sig; } - - /** Caches eval(Sig) and eval(Field) results. */ - private Map evalCache = new LinkedHashMap(); - - /** Return the A4TupleSet for the given sig (if solution not yet solved, or unsatisfiable, or sig not found, then return an empty tupleset) */ - public A4TupleSet eval(Sig sig) { - try { - if (!solved || eval==null) return new A4TupleSet(factory.noneOf(1), this); - A4TupleSet ans = evalCache.get(sig); - if (ans!=null) return ans; - TupleSet ts = eval.evaluate((Expression) TranslateAlloyToKodkod.alloy2kodkod(this, sig)); - ans = new A4TupleSet(ts, this); - evalCache.put(sig, ans); - return ans; - } catch(Err er) { - return new A4TupleSet(factory.noneOf(1), this); - } - } - - /** Return the A4TupleSet for the given field (if solution not yet solved, or unsatisfiable, or field not found, then return an empty tupleset) */ - public A4TupleSet eval(Field field) { - try { - if (!solved || eval==null) return new A4TupleSet(factory.noneOf(field.type().arity()), this); - A4TupleSet ans = evalCache.get(field); - if (ans!=null) return ans; - TupleSet ts = eval.evaluate((Expression) TranslateAlloyToKodkod.alloy2kodkod(this, field)); - ans = new A4TupleSet(ts, this); - evalCache.put(field, ans); - return ans; - } catch(Err er) { - return new A4TupleSet(factory.noneOf(field.type().arity()), this); - } - } - - /** If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean. */ - public Object eval(Expr expr) throws Err { - try { - if (expr instanceof Sig) return eval((Sig)expr); - if (expr instanceof Field) return eval((Field)expr); - if (!solved) throw new ErrorAPI("This solution is not yet solved, so eval() is not allowed."); - if (eval==null) throw new ErrorAPI("This solution is unsatisfiable, so eval() is not allowed."); - if (expr.ambiguous && !expr.errors.isEmpty()) expr = expr.resolve(expr.type(), null); - if (!expr.errors.isEmpty()) throw expr.errors.pick(); - Object result = TranslateAlloyToKodkod.alloy2kodkod(this, expr); - if (result instanceof IntExpression) return eval.evaluate((IntExpression)result) + (eval.wasOverflow() ? " (OF)" : ""); - if (result instanceof Formula) return eval.evaluate((Formula)result); - if (result instanceof Expression) return new A4TupleSet(eval.evaluate((Expression)result), this); - throw new ErrorFatal("Unknown internal error encountered in the evaluator."); - } catch(CapacityExceededException ex) { - throw TranslateAlloyToKodkod.rethrow(ex); - } - } - - /** Returns the Kodkod instance represented by this solution; throws an exception if the problem is not yet solved or if it is unsatisfiable. */ - public Instance debugExtractKInstance() throws Err { - if (!solved) throw new ErrorAPI("This solution is not yet solved, so instance() is not allowed."); - if (eval==null) throw new ErrorAPI("This solution is unsatisfiable, so instance() is not allowed."); - return eval.instance().unmodifiableView(); - } - - //===================================================================================================// - - /** Maps a Kodkod formula to an Alloy Expr or Alloy Pos (or null if no such mapping) */ - Object k2pos(Node formula) { return k2pos.get(formula); } - - /** Associates the Kodkod formula to a particular Alloy Expr (if the Kodkod formula is not already associated with an Alloy Expr or Alloy Pos) */ - Formula k2pos(Formula formula, Expr expr) throws Err { - if (solved) throw new ErrorFatal("Cannot alter the k->pos mapping since solve() has completed."); - if (formula==null || expr==null || k2pos.containsKey(formula)) return formula; - k2pos.put(formula, expr); - if (formula instanceof BinaryFormula) { - BinaryFormula b = (BinaryFormula)formula; - if (b.op() == FormulaOperator.AND) { k2pos(b.left(), expr); k2pos(b.right(), expr); } - } - return formula; - } - - /** Associates the Kodkod formula to a particular Alloy Pos (if the Kodkod formula is not already associated with an Alloy Expr or Alloy Pos) */ - Formula k2pos(Formula formula, Pos pos) throws Err { - if (solved) throw new ErrorFatal("Cannot alter the k->pos mapping since solve() has completed."); - if (formula==null || pos==null || pos==Pos.UNKNOWN || k2pos.containsKey(formula)) return formula; - k2pos.put(formula, pos); - if (formula instanceof BinaryFormula) { - BinaryFormula b = (BinaryFormula)formula; - if (b.op() == FormulaOperator.AND) { k2pos(b.left(), pos); k2pos(b.right(), pos); } - } - return formula; - } - - //===================================================================================================// - - /** Associates the Kodkod relation to a particular Alloy Type (if it is not already associated with something) */ - void kr2type(Relation relation, Type newType) throws Err { - if (solved) throw new ErrorFatal("Cannot alter the k->type mapping since solve() has completed."); - if (!rel2type.containsKey(relation)) rel2type.put(relation, newType); - } - - /** Remove all mapping from Kodkod relation to Alloy Type. */ - void kr2typeCLEAR() throws Err { - if (solved) throw new ErrorFatal("Cannot clear the k->type mapping since solve() has completed."); - rel2type.clear(); - } - - //===================================================================================================// - - /** Caches a constant pair of Type.EMPTY and Pos.UNKNOWN */ - private Pair cachedPAIR = null; - - /** Maps a Kodkod variable to an Alloy Type and Alloy Pos (if no association exists, it will return (Type.EMPTY , Pos.UNKNOWN) */ - Pair kv2typepos(Variable var) { - Pair ans=decl2type.get(var); - if (ans!=null) return ans; - if (cachedPAIR==null) cachedPAIR=new Pair(Type.EMPTY, Pos.UNKNOWN); - return cachedPAIR; - } - - /** Associates the Kodkod variable to a particular Alloy Type and Alloy Pos (if it is not already associated with something) */ - void kv2typepos(Variable var, Type type, Pos pos) throws Err { - if (solved) throw new ErrorFatal("Cannot alter the k->type mapping since solve() has completed."); - if (type==null) type=Type.EMPTY; - if (pos==null) pos=Pos.UNKNOWN; - if (!decl2type.containsKey(var)) decl2type.put(var, new Pair(type, pos)); - } - - //===================================================================================================// - - /** Add the given formula to the list of Kodkod formulas, and associate it with the given Pos object (pos can be null if unknown). */ - void addFormula(Formula newFormula, Pos pos) throws Err { - if (solved) throw new ErrorFatal("Cannot add an additional formula since solve() has completed."); - if (formulas.size()>0 && formulas.get(0)==Formula.FALSE) return; // If one formula is false, we don't need the others - if (newFormula==Formula.FALSE) formulas.clear(); // If one formula is false, we don't need the others - formulas.add(newFormula); - if (pos!=null && pos!=Pos.UNKNOWN) k2pos(newFormula, pos); - } - - /** Add the given formula to the list of Kodkod formulas, and associate it with the given Expr object (expr can be null if unknown) */ - void addFormula(Formula newFormula, Expr expr) throws Err { - if (solved) throw new ErrorFatal("Cannot add an additional formula since solve() has completed."); - if (formulas.size()>0 && formulas.get(0)==Formula.FALSE) return; // If one formula is false, we don't need the others - if (newFormula==Formula.FALSE) formulas.clear(); // If one formula is false, we don't need the others - formulas.add(newFormula); - if (expr!=null) k2pos(newFormula, expr); - } - - //===================================================================================================// - - /** Helper class that wraps an iterator up where it will pre-fetch the first element (note: it will not prefetch subsequent elements). */ - private static final class Peeker implements Iterator { - /** The encapsulated iterator. */ - private Iterator iterator; - /** True iff we have captured the first element. */ - private boolean hasFirst; - /** If hasFirst is true, then this is the captured first element. */ - private T first; - /** Constructrs a Peeker object. */ - private Peeker(Iterator it) { - iterator = it; - if (it.hasNext()) { hasFirst=true; first=it.next(); } - } - /** {@inheritDoc} */ - public boolean hasNext() { - return hasFirst || iterator.hasNext(); - } - /** {@inheritDoc} */ - public T next() { - if (hasFirst) { hasFirst=false; T ans=first; first=null; return ans; } else return iterator.next(); - } - /** {@inheritDoc} */ - public void remove() { throw new UnsupportedOperationException(); } - } - - //===================================================================================================// - - /** Helper method to determine if a given binary relation is a total order over a given unary relation. */ - private static List isOrder(TupleSet b, TupleSet u) { - // Size check - final int n = u.size(); - final List list = new ArrayList(n); - if (b.size() == 0 && n <= 1) return list; - if (b.size() != n-1) return null; - // Find the starting element - Tuple head = null; - TupleSet right = b.project(1); - for(Tuple x: u) if (!right.contains(x)) {head = x; break;} - if (head==null) return null; - final TupleFactory f = head.universe().factory(); - // Form the list - list.add(head); - while(true) { - // Find head.next - Tuple headnext = null; - for(Tuple x: b) if (x.atom(0)==head.atom(0)) { headnext = f.tuple(x.atom(1)); break; } - // If we've reached the end of the chain, and indeed we've formed exactly n elements (and all are in u), we're done - if (headnext==null) return list.size()==n ? list : null; - // If we've accumulated more than n elements, or if we reached an element not in u, then we declare failure - if (list.size()==n || !u.contains(headnext)) return null; - // Move on to the next step - head = headnext; - list.add(head); - } - } - - /** Helper method that chooses a name for each atom based on its most specific sig; (external caller should call this method with s==null and nexts==null) */ - private static void rename (A4Solution frame, PrimSig s, Map> nexts, UniqueNameGenerator un) throws Err { - if (s==null) { - for(ExprVar sk:frame.skolems) un.seen(sk.label); - // Store up the skolems - List skolems = new ArrayList(); - for(Map.Entry e: frame.rel2type.entrySet()) { - Relation r = e.getKey(); if (!frame.eval.instance().contains(r)) continue; - Type t = e.getValue(); if (t.arity() > r.arity()) continue; // Something is wrong; let's skip it - while (t.arity() < r.arity()) t = UNIV.type().product(t); - String n = Util.tail(r.name()); - while(n.length()>0 && n.charAt(0)=='$') n = n.substring(1); - skolems.add(n); - skolems.add(t); - skolems.add(r); - } - // Find all suitable "next" or "prev" relations - nexts = new LinkedHashMap>(); - for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("next")==0) { - List> fold = f.type().fold(); - if (fold.size()==1) { - List t = fold.get(0); - if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) { - TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1))); - if (set.size()<=1) continue; - TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f))); - List test = isOrder(next, set); - if (test!=null) nexts.put(t.get(1), test); - } else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) { - TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0))); - if (set.size()<=1) continue; - TupleSet next = frame.eval.evaluate(frame.a2k(f)); - List test = isOrder(next, set); - if (test!=null) nexts.put(t.get(1), test); - } - } - } - for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("prev")==0) { - List> fold = f.type().fold(); - if (fold.size()==1) { - List t = fold.get(0); - if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) { - TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1))); - if (set.size()<=1) continue; - TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f)).transpose()); - List test = isOrder(next, set); - if (test!=null) nexts.put(t.get(1), test); - } else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) { - TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0))); - if (set.size()<=1) continue; - TupleSet next = frame.eval.evaluate(frame.a2k(f).transpose()); - List test = isOrder(next, set); - if (test!=null) nexts.put(t.get(1), test); - } - } - } - // Assign atom->name and atom->MostSignificantSig - for(Tuple t:frame.eval.evaluate(Relation.INTS)) { frame.atom2sig.put(t.atom(0), SIGINT); } - for(Tuple t:frame.eval.evaluate(KK_SEQIDX)) { frame.atom2sig.put(t.atom(0), SEQIDX); } - for(Tuple t:frame.eval.evaluate(KK_STRING)) { frame.atom2sig.put(t.atom(0), STRING); } - for(Tuple t:frame.eval.evaluate(KK_TIME)) { frame.atom2sig.put(t.atom(0), TIME); } // pt.uminho.haslab - for(Sig sig:frame.sigs) if (sig instanceof PrimSig && !sig.builtin && ((PrimSig)sig).isTopLevel()) rename(frame, (PrimSig)sig, nexts, un); - // These are redundant atoms that were not chosen to be in the final instance - int unused=0; - for(Tuple tuple:frame.eval.evaluate(Relation.UNIV)) { - Object atom = tuple.atom(0); - if (!frame.atom2sig.containsKey(atom)) { frame.atom2name.put(atom, "unused"+unused); unused++; } - } - // Add the skolems - for(int num=skolems.size(), i=0; i0 && n.charAt(0)=='$') n=n.substring(1); - Type t = (Type) skolems.get(i+1); - Relation r = (Relation) skolems.get(i+2); - frame.addSkolem(un.make("$"+n), t, r); - } - return; - } - for(PrimSig c: s.children()) rename(frame, c, nexts, un); - String signame = un.make(s.label.startsWith("this/") ? s.label.substring(5) : s.label); - List list = new ArrayList(); - for(Tuple t: frame.eval.evaluate(frame.a2k(s))) list.add(t); - List order = nexts.get(s); - if (order!=null && order.size()==list.size() && order.containsAll(list)) { list=order; } - int i = 0; - for(Tuple t: list) { - if (frame.atom2sig.containsKey(t.atom(0))) continue; // This means one of the subsig has already claimed this atom. - String x = signame + "$" + i; - i++; - frame.atom2sig.put(t.atom(0), s); - frame.atom2name.put(t.atom(0), x); - ExprVar v = ExprVar.make(null, x, s.type()); - TupleSet ts = t.universe().factory().range(t, t); - Relation r = Relation.unary(x); - frame.eval.instance().add(r, ts); - frame.a2k.put(v, r); - frame.atoms.add(v); - } - } - - //===================================================================================================// - - /** Solve for the solution if not solved already; if cmd==null, we will simply use the lowerbound of each relation as its value. */ - A4Solution solve(final A4Reporter rep, Command cmd, Simplifier simp, boolean tryBookExamples) throws Err, IOException { - // If already solved, then return this object as is - if (solved) return this; - // If cmd==null, then all four arguments are ignored, and we simply use the lower bound of each relation - if (cmd==null) { - Instance inst = new Instance(bounds.universe()); - for(int max=max(), i=min(); i<=max; i++) { - Tuple it = factory.tuple(""+i); - inst.add(i, factory.range(it, it)); - } - for(Relation r: bounds.relations()) inst.add(r, bounds.lowerBound(r)); - eval = new Evaluator(inst, solver.options()); - rename(this, null, null, new UniqueNameGenerator()); - solved(); - return this; - } - // Otherwise, prepare to do the solve... - final A4Options opt = originalOptions; - long time = System.currentTimeMillis(); - rep.debug("Simplifying the bounds...\n"); - if (simp!=null && formulas.size()>0 && !simp.simplify(rep, this, formulas)) addFormula(Formula.FALSE, Pos.UNKNOWN); - rep.translate(opt.solver.id(), bitwidth, maxseq, solver.options().skolemDepth(), solver.options().symmetryBreaking()); - Formula 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}; - solver.options().setReporter(new AbstractReporter() { // Set up a reporter to catch the type+pos of skolems - @Override public void skolemizing(Decl decl, Relation skolem, List predecl) { - try { - Type t=kv2typepos(decl.variable()).a; - if (t==Type.EMPTY) return; - for(int i=(predecl==null ? -1 : predecl.size()-1); i>=0; i--) { - Type pp=kv2typepos(predecl.get(i).variable()).a; - if (pp==Type.EMPTY) return; - t=pp.product(t); - } - kr2type(skolem, t); - } catch(Throwable ex) { } // Exception here is not fatal - } - @Override public void solvingCNF(int primaryVars, int vars, int clauses) { - if (solved[0]) return; else solved[0]=true; // initially solved[0] is true, so we won't report the # of vars/clauses - if (rep!=null) rep.solve(primaryVars, vars, clauses); - } - }); - if (!opt.solver.equals(SatSolver.CNF) && !opt.solver.equals(SatSolver.KK) && tryBookExamples) { // try book examples - A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null; - try { sol = BookExamples.trial(r, this, fgoal, solver, cmd.check); } catch(Throwable ex) { sol = null; } - } - solved[0] = false; // this allows the reporter to report the # of 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(SatSolver.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(SatSolver.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()) { - if (sol==null) sol = solver.solve(fgoal, bounds); - } else { - kEnumerator = new Peeker(solver.solveAll(fgoal, bounds)); - if (sol==null) sol = kEnumerator.next(); - } - if (!solved[0]) rep.solve(0, 0, 0); - final Instance inst = sol.instance(); - // To ensure no more output during SolutionEnumeration - solver.options().setReporter(oldReporter); - // If unsatisfiable, then retreive the unsat core if desired - if (inst==null && solver.options().solver()==SATFactory.MiniSatProver) { - try { - lCore = new LinkedHashSet(); - Proof p = sol.proof(); - if (sol.outcome()==UNSATISFIABLE) { - // only perform the minimization if it was UNSATISFIABLE, rather than TRIVIALLY_UNSATISFIABLE - int i = p.highLevelCore().size(); - rep.minimizing(cmd, i); - if (opt.coreMinimization==0) try { p.minimize(new RCEStrategy(p.log())); } catch(Throwable ex) {} - if (opt.coreMinimization==1) try { p.minimize(new HybridStrategy(p.log())); } catch(Throwable ex) {} - rep.minimized(cmd, i, p.highLevelCore().size()); - } - for(Iterator it=p.core(); it.hasNext();) { - Object n=it.next().node(); - if (n instanceof Formula) lCore.add((Formula)n); - } - Map map = p.highLevelCore(); - hCore = new LinkedHashSet(map.keySet()); - hCore.addAll(map.values()); - } catch(Throwable ex) { - lCore = hCore = null; - } - } - // If satisfiable, then add/rename the atoms and skolems - if (inst!=null) { - eval = new Evaluator(inst, solver.options()); - rename(this, null, null, new UniqueNameGenerator()); - } - // report the result - solved(); - time = System.currentTimeMillis() - time; - if (eval!=null) { - String[] aux0 = eval(PrimSig.TIME.join(ExprConstant.LOOP)).toString().split("\\$"); - if (aux0.length > 1) { - String aux = aux0[1]; -// rep.debug("LOOP: "+eval((ExprConstant.LOOP)).toString()); -// rep.debug("NEXT: "+eval((ExprConstant.NEXTTIME)).toString()); - loop = Integer.parseInt(aux.substring(0, aux.length()-1)); - } - } - - if (inst!=null) rep.resultSAT(cmd, time, this); else rep.resultUNSAT(cmd, time, this); - return this; - } - - //===================================================================================================// - - /** This caches the toString() output. */ - private String toStringCache = null; - - /** Dumps the Kodkod solution into String. */ - @Override public String toString() { - if (!solved) return "---OUTCOME---\nUnknown.\n"; - if (eval == null) return "---OUTCOME---\nUnsatisfiable.\n"; - String answer = toStringCache; - if (answer != null) return answer; - Instance sol = eval.instance(); - StringBuilder sb = new StringBuilder(); - sb.append("---INSTANCE---\n" + "integers={"); - boolean firstTuple = true; - for(IndexedEntry e:sol.intTuples()) { - if (firstTuple) firstTuple=false; else sb.append(", "); - // No need to print e.index() since we've ensured the Int atom's String representation is always equal to ""+e.index() - Object atom = e.value().iterator().next().atom(0); - sb.append(atom2name(atom)); - } - sb.append("}\n"); - try { - for(Sig s:sigs) { - sb.append(s.label).append("=").append(eval(s)).append("\n"); - for(Field f:s.getFields()) sb.append(s.label).append("<:").append(f.label).append("=").append(eval(f)).append("\n"); - } - for(ExprVar v:skolems) { - sb.append("skolem ").append(v.label).append("=").append(eval(v)).append("\n"); - } - sb.append("loop ").append(eval(ExprConstant.LOOP)).append("\n"); - sb.append("next ").append(eval(ExprConstant.NEXTTIME)).append("\n"); - sb.append("next ").append(eval.evaluate(KK_TIMEINIT)).append("\n"); - - return toStringCache = sb.toString(); - } catch(Err er) { - return toStringCache = (""); - } - } - - //===================================================================================================// - - /** If nonnull, it caches the result of calling "next()". */ - private A4Solution nextCache = null; - - /** If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT). - * @throws ErrorAPI if the solver was not an incremental solver - */ - public A4Solution next() throws Err { - if (!solved) throw new ErrorAPI("This solution is not yet solved, so next() is not allowed."); - if (eval==null) return this; - if (nextCache==null) nextCache=new A4Solution(this); - return nextCache; - } - - /** Returns true if this solution was generated by an incremental SAT solver. */ - public boolean isIncremental() { return kEnumerator!=null; } - - //===================================================================================================// - - /** The low-level unsat core; null if it is not available. */ - private LinkedHashSet lCore = null; - - /** This caches the result of lowLevelCore(). */ - private Set lCoreCache = null; - - /** If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set. */ - public Set lowLevelCore() { - if (lCoreCache!=null) return lCoreCache; - Set ans1 = new LinkedHashSet(); - if (lCore!=null) for(Node f: lCore) { - Object y = k2pos(f); - if (y instanceof Pos) ans1.add( (Pos)y ); else if (y instanceof Expr) ans1.add( ((Expr)y).span() ); - } - return lCoreCache = Collections.unmodifiableSet(ans1); - } - - //===================================================================================================// - - /** The high-level unsat core; null if it is not available. */ - private LinkedHashSet hCore = null; - - /** This caches the result of highLevelCore(). */ - private Pair,Set> hCoreCache = null; - - /** If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set. */ - public Pair,Set> highLevelCore() { - if (hCoreCache!=null) return hCoreCache; - Set ans1 = new LinkedHashSet(), ans2 = new LinkedHashSet(); - if (hCore!=null) for(Node f: hCore) { - Object x = k2pos(f); - if (x instanceof Pos) { - // System.out.println("F: "+f+" at "+x+"\n"); System.out.flush(); - ans1.add((Pos)x); - } else if (x instanceof Expr) { - Expr expr = (Expr)x; - Pos p = ((Expr)x).span(); - ans1.add(p); - // System.out.println("F: "+f+" by "+p.x+","+p.y+"->"+p.x2+","+p.y2+" for "+x+"\n\n"); System.out.flush(); - for(Func func: expr.findAllFunctions()) ans2.add(func.getBody().span()); - } - } - return hCoreCache = new Pair,Set>(Collections.unmodifiableSet(ans1), Collections.unmodifiableSet(ans2)); - } - - //===================================================================================================// - - /** Helper method to write out a full XML file. */ - public void writeXML(String filename) throws Err { - writeXML(filename, null, null); - } - - /** Helper method to write out a full XML file. */ - public void writeXML(String filename, Iterable macros) throws Err { - writeXML(filename, macros, null); - } - - /** Helper method to write out a full XML file. */ - public void writeXML(String filename, Iterable macros, Map sourceFiles) throws Err { - PrintWriter out=null; - try { - out=new PrintWriter(filename,"UTF-8"); - writeXML(out, macros, sourceFiles); - if (!Util.close(out)) throw new ErrorFatal("Error writing the solution XML file."); - } catch(IOException ex) { - Util.close(out); - throw new ErrorFatal("Error writing the solution XML file.", ex); - } - } - - /** Helper method to write out a full XML file. */ - public void writeXML(A4Reporter rep, String filename, Iterable macros, Map sourceFiles) throws Err { - PrintWriter out=null; - try { - out=new PrintWriter(filename,"UTF-8"); - writeXML(rep, out, macros, sourceFiles); - if (!Util.close(out)) throw new ErrorFatal("Error writing the solution XML file."); - } catch(IOException ex) { - Util.close(out); - throw new ErrorFatal("Error writing the solution XML file.", ex); - } - } - - /** Helper method to write out a full XML file. */ - public void writeXML(PrintWriter writer, Iterable macros, Map sourceFiles) throws Err { - A4SolutionWriter.writeInstance(null, this, writer, macros, sourceFiles); - if (writer.checkError()) throw new ErrorFatal("Error writing the solution XML file."); - } - - /** Helper method to write out a full XML file. */ - public void writeXML(A4Reporter rep, PrintWriter writer, Iterable macros, Map sourceFiles) throws Err { - A4SolutionWriter.writeInstance(rep, this, writer, macros, sourceFiles); - if (writer.checkError()) throw new ErrorFatal("Error writing the solution XML file."); - } + //====== mutable fields (immutable after solve() has been called) ===================================// + + /** True iff the problem is solved. */ + private boolean solved = false; + + /** The Kodkod Bounds object. */ + private Bounds bounds; + + /** The list of Kodkod formulas; can be empty if unknown; once a solution is solved we must not modify this anymore */ + private ArrayList formulas = new ArrayList(); + + /** The list of known Alloy4 sigs. */ + private SafeList sigs; + + /** If solved==true and is satisfiable, then this is the list of known skolems. */ + private SafeList skolems = new SafeList(); + + /** If solved==true and is satisfiable, then this is the list of actually used atoms. */ + private SafeList atoms = new SafeList(); + + /** If solved==true and is satisfiable, then this maps each Kodkod atom to a short name. */ + private Map atom2name = new LinkedHashMap(); + + /** If solved==true and is satisfiable, then this maps each Kodkod atom to its most specific sig. */ + private Map atom2sig = new LinkedHashMap(); + + /** If solved==true and is satisfiable, then this is the Kodkod evaluator. */ + private Evaluator eval = null; + + /** If not null, you can ask it to get another solution. */ + private Iterator kEnumerator = null; + + /** The map from each Sig/Field/Skolem/Atom to its corresponding Kodkod expression. */ + private Map a2k; + + /** The map from each String literal to its corresponding Kodkod expression. */ + private final ConstMap s2k; + + /** The map from each kodkod Formula to Alloy Expr or Alloy Pos (can be empty if unknown) */ + private Map k2pos; + + /** The map from each Kodkod Relation to Alloy Type (can be empty or incomplete if unknown) */ + private Map rel2type; + + /** The map from each Kodkod Variable to an Alloy Type and Alloy Pos. */ + private Map> decl2type; + + //===================================================================================================// + + /** Construct a blank A4Solution containing just UNIV, SIGINT, SEQIDX, STRING, and NONE as its only known sigs. + * @param originalCommand - the original Alloy command that generated this solution; can be "" if unknown + * @param bitwidth - the bitwidth; must be between 1 and 30 + * @param maxseq - the maximum allowed sequence length; must be between 0 and (2^(bitwidth-1))-1 + * @param time TODO + * @param loop TODO + * @param atoms - the set of atoms + * @param rep - the reporter that will receive diagnostic and progress messages + * @param opt - the Alloy options that will affect the solution and the solver + * @param expected - whether the user expected an instance or not (1 means yes, 0 means no, -1 means the user did not express an expectation) + */ + // pt.uminho.haslab: extended with time scopes + A4Solution(String originalCommand, int bitwidth, int maxseq, Set stringAtoms, int time, int loop, Collection atoms, final A4Reporter rep, A4Options opt, int expected) throws Err { + opt = opt.dup(); + this.unrolls = opt.unrolls; + this.sigs = new SafeList(Arrays.asList(UNIV, SIGINT, SEQIDX, STRING, NONE, TIME)); //pt.uminho.haslab: time sig + this.a2k = Util.asMap(new Expr[]{UNIV, SIGINT, SEQIDX, STRING, NONE, TIME}, Relation.INTS.union(KK_STRING).union(KK_TIME), Relation.INTS, KK_SEQIDX, KK_STRING, Relation.NONE, KK_TIME); //pt.uminho.haslab: time sig + this.k2pos = new LinkedHashMap(); + this.rel2type = new LinkedHashMap(); + this.decl2type = new LinkedHashMap>(); + this.originalOptions = opt; + this.originalCommand = (originalCommand==null ? "" : originalCommand); + this.bitwidth = bitwidth; + this.maxseq = maxseq; + this.time = time; //pt.uminho.haslab: time scopes + this.loop = loop; //pt.uminho.haslab: time scopes + if (bitwidth < 0) throw new ErrorSyntax("Cannot specify a bitwidth less than 0"); + if (bitwidth > 30) throw new ErrorSyntax("Cannot specify a bitwidth greater than 30"); + if (maxseq < 0) throw new ErrorSyntax("The maximum sequence length cannot be negative."); + if (maxseq > 0 && maxseq > max()) throw new ErrorSyntax("With integer bitwidth of "+bitwidth+", you cannot have sequence length longer than "+max()); + if (atoms.isEmpty()) { + atoms = new ArrayList(1); + atoms.add(""); + } + kAtoms = ConstList.make(atoms); + bounds = new Bounds(new Universe(kAtoms)); + factory = bounds.universe().factory(); + TupleSet sigintBounds = factory.noneOf(1); + TupleSet seqidxBounds = factory.noneOf(1); + TupleSet stringBounds = factory.noneOf(1); + TupleSet timeBounds = factory.noneOf(1); + final TupleSet next = factory.noneOf(2); + final TupleSet timenext = factory.noneOf(2); + final TupleSet timeback = factory.noneOf(2); + int min=min(), max=max(); + if (max >= min) for(int i=min; i<=max; i++) { // Safe since we know 1 <= bitwidth <= 30 + Tuple ii = factory.tuple(""+i); + TupleSet is = factory.range(ii, ii); + bounds.boundExactly(i, is); + sigintBounds.add(ii); + if (i>=0 && i s2k = new HashMap(); + for(String e: stringAtoms) { + Relation r = Relation.unary(""); + Tuple t = factory.tuple(e); + s2k.put(e, r); + bounds.boundExactly(r, factory.range(t, t)); + stringBounds.add(t); + } + this.s2k = ConstMap.make(s2k); + this.stringBounds = stringBounds.unmodifiableView(); + bounds.boundExactly(KK_STRING, this.stringBounds); + // pt.uminho.haslab: create time bounds (deprecated) + if (time < 1) { + bounds.boundExactly(KK_TIMEINIT, factory.noneOf(1)); + bounds.boundExactly(KK_TIMEEND, factory.noneOf(1)); + bounds.boundExactly(KK_TIMELOOP, factory.noneOf(2)); + bounds.boundExactly(KK_TIMENEXT, factory.noneOf(2)); + } else { + for(int i=0; i= 0) { + timeback.add(factory.tuple("Time$"+(time-1),"Time$"+loop)); + bounds.boundExactly(KK_TIMELOOP, timeback); + timeback.addAll(timenext); + bounds.boundExactly(KK_TIMENEXT, timeback); + } else { + bounds.bound(KK_TIMELOOP, timeback); + timeback.addAll(timenext); + bounds.bound(KK_TIMENEXT, timenext, timeback); + } + } + this.timeBounds = timeBounds.unmodifiableView(); + bounds.boundExactly(KK_TIME, this.timeBounds); + int sym = (expected==1 ? 0 : opt.symmetry); + solver = new Solver(); + solver.options().setNoOverflow(opt.noOverflow); + solver.options().setFlatten(false); // added for now, since multiplication and division circuit takes forever to flatten + if (opt.solver.external()!=null) { + String ext = opt.solver.external(); + if (opt.solverDirectory.length()>0 && ext.indexOf(File.separatorChar)<0) ext=opt.solverDirectory+File.separatorChar+ext; + try { + File tmp = File.createTempFile("tmp", ".cnf", new File(opt.tempDirectory)); + tmp.deleteOnExit(); + solver.options().setSolver(SATFactory.externalFactory(ext, tmp.getAbsolutePath(), "", opt.solver.options())); + //solver.options().setSolver(SATFactory.externalFactory(ext, tmp.getAbsolutePath(), opt.solver.options())); + } catch(IOException ex) { throw new ErrorFatal("Cannot create temporary directory.", ex); } + } else if (opt.solver.equals(A4Options.SatSolver.ZChaffJNI)) { + solver.options().setSolver(SATFactory.ZChaff); + } else if (opt.solver.equals(A4Options.SatSolver.MiniSatJNI)) { + solver.options().setSolver(SATFactory.MiniSat); + } else if (opt.solver.equals(A4Options.SatSolver.MiniSatProverJNI)) { + sym=20; + solver.options().setSolver(SATFactory.MiniSatProver); + solver.options().setLogTranslation(2); + solver.options().setCoreGranularity(opt.coreGranularity); + } else { + solver.options().setSolver(SATFactory.DefaultSAT4J); // Even for "KK" and "CNF", we choose SAT4J here; later, just before solving, we'll change it to a Write2CNF solver + } + solver.options().setSymmetryBreaking(sym); + solver.options().setSkolemDepth(opt.skolemDepth); + solver.options().setBitwidth(bitwidth > 0 ? bitwidth : (int) Math.ceil(Math.log(atoms.size())) + 1); + solver.options().setIntEncoding(Options.IntEncoding.TWOSCOMPLEMENT); + } + + /** Construct a new A4Solution that is the continuation of the old one, but with the "next" instance. */ + // pt.uminho.haslab: extended with time scopes + private A4Solution(A4Solution old) throws Err { + if (!old.solved) throw new ErrorAPI("This solution is not yet solved, so next() is not allowed."); + if (old.kEnumerator==null) throw new ErrorAPI("This solution was not generated by an incremental SAT solver.\n" + "Solution enumeration is currently only implemented for MiniSat and SAT4J."); + if (old.eval==null) throw new ErrorAPI("This solution is already unsatisfiable, so you cannot call next() to get the next solution."); + Instance inst = old.kEnumerator.next().instance(); + unrolls = old.unrolls; + originalOptions = old.originalOptions; + originalCommand = old.originalCommand; + bitwidth = old.bitwidth; + time = old.time; // pt.uminho.haslab: time scopes + loop = old.loop; // pt.uminho.haslab: time scopes + maxseq = old.maxseq; + kAtoms = old.kAtoms; + factory = old.factory; + sigintBounds = old.sigintBounds; + seqidxBounds = old.seqidxBounds; + stringBounds = old.stringBounds; + timeBounds = old.timeBounds; // pt.uminho.haslab: time scopes + solver = old.solver; + bounds = old.bounds; + formulas = old.formulas; + sigs = old.sigs; + kEnumerator = old.kEnumerator; + k2pos = old.k2pos; + rel2type = old.rel2type; + decl2type = old.decl2type; + if (inst!=null) { + eval = new Evaluator(inst, old.solver.options()); + a2k = new LinkedHashMap(); + for(Map.Entry e: old.a2k.entrySet()) + if (e.getKey() instanceof Sig || e.getKey() instanceof Field) + a2k.put(e.getKey(), e.getValue()); + UniqueNameGenerator un = new UniqueNameGenerator(); + rename(this, null, null, un); + a2k = ConstMap.make(a2k); + } else { + skolems = old.skolems; + eval = null; + a2k = old.a2k; + } + s2k = old.s2k; + atoms = atoms.dup(); + atom2name = ConstMap.make(atom2name); + atom2sig = ConstMap.make(atom2sig); + solved = true; + } + + /** Turn the solved flag to be true, and make all remaining fields immutable. */ + private void solved() { + if (solved) return; // already solved + bounds = bounds.clone().unmodifiableView(); + sigs = sigs.dup(); + skolems = skolems.dup(); + atoms = atoms.dup(); + atom2name = ConstMap.make(atom2name); + atom2sig = ConstMap.make(atom2sig); + a2k = ConstMap.make(a2k); + k2pos = ConstMap.make(k2pos); + rel2type = ConstMap.make(rel2type); + decl2type = ConstMap.make(decl2type); + solved = true; + } + + //===================================================================================================// + + /** Returns the bitwidth; always between 1 and 30. */ + public int getBitwidth() { return bitwidth; } + + /** Returns the maximum allowed sequence length; always between 0 and 2^(bitwidth-1)-1. */ + public int getMaxSeq() { return maxseq; } + + public int getTime() { return time; } // pt.uminho.haslab: time scopes + + public int getLoop() { return loop; } // pt.uminho.haslab: time scopes + + /** Returns the largest allowed integer, or -1 if no integers are allowed. */ + public int max() { return Util.max(bitwidth); } + + /** Returns the smallest allowed integer, or 0 if no integers are allowed */ + public int min() { return Util.min(bitwidth); } + + /** Returns the maximum number of allowed loop unrolling or recursion level. */ + public int unrolls() { return unrolls; } + + //===================================================================================================// + + /** Returns the original Alloy file name that generated this solution; can be "" if unknown. */ + public String getOriginalFilename() { return originalOptions.originalFilename; } + + /** Returns the original command that generated this solution; can be "" if unknown. */ + public String getOriginalCommand() { return originalCommand; } + + //===================================================================================================// + + /** Returns the Kodkod input used to generate this solution; returns "" if unknown. */ + public String debugExtractKInput() { + if (solved) + return TranslateKodkodToJava.convert(Formula.and(formulas), bitwidth, kAtoms, bounds, atom2name); + else + return TranslateKodkodToJava.convert(Formula.and(formulas), bitwidth, kAtoms, bounds.unmodifiableView(), null); + } + + //===================================================================================================// + + /** Returns the Kodkod TupleFactory object. */ + TupleFactory getFactory() { return factory; } + + /** Returns a modifiable copy of the Kodkod Bounds object. */ + Bounds getBounds() { return bounds.clone(); } + + /** Add a new relation with the given label and the given lower and upper bound. + * @param label - the label for the new relation; need not be unique + * @param lower - the lowerbound; can be null if you want it to be the empty set + * @param upper - the upperbound; cannot be null; must contain everything in lowerbound + */ + Relation addRel(String label, TupleSet lower, TupleSet upper) throws ErrorFatal { + if (solved) throw new ErrorFatal("Cannot add a Kodkod relation since solve() has completed."); + Relation rel = Relation.nary(label, upper.arity()); + if (lower == upper) { + bounds.boundExactly(rel, upper); + } else if (lower == null) { + bounds.bound(rel, upper); + } else { + if (lower.arity() != upper.arity()) throw new ErrorFatal("Relation "+label+" must have same arity for lowerbound and upperbound."); + bounds.bound(rel, lower, upper); + } + return rel; + } + + /** Add a new sig to this solution and associate it with the given expression (and if s.isTopLevel then add this expression into Sig.UNIV). + *
The expression must contain only constant Relations or Relations that are already bound in this solution. + *
(If the sig was already added by a previous call to addSig(), then this call will return immediately without altering what it is associated with) + */ + void addSig(Sig s, Expression expr) throws ErrorFatal { + if (solved) throw new ErrorFatal("Cannot add an additional sig since solve() has completed."); + if (expr.arity()!=1) throw new ErrorFatal("Sig "+s+" must be associated with a unary relational value."); + if (a2k.containsKey(s)) return; + a2k.put(s, expr); + sigs.add(s); + if (s.isTopLevel()) a2k.put(UNIV, a2k.get(UNIV).union(expr)); + } + + /** Add a new field to this solution and associate it with the given expression. + *
The expression must contain only constant Relations or Relations that are already bound in this solution. + *
(If the field was already added by a previous call to addField(), then this call will return immediately without altering what it is associated with) + */ + void addField(Field f, Expression expr) throws ErrorFatal { + if (solved) throw new ErrorFatal("Cannot add an additional field since solve() has completed."); + if (expr.arity()!=f.type().arity()) throw new ErrorFatal("Field "+f+" must be associated with an "+f.type().arity()+"-ary relational value."); + if (a2k.containsKey(f)) return; + a2k.put(f, expr); + } + + /** Add a new skolem to this solution and associate it with the given expression. + *
The expression must contain only constant Relations or Relations that are already bound in this solution. + */ + private ExprVar addSkolem(String label, Type type, Expression expr) throws Err { + if (solved) throw new ErrorFatal("Cannot add an additional skolem since solve() has completed."); + int a = type.arity(); + if (a<1) throw new ErrorFatal("Skolem "+label+" must be associated with a relational value."); + if (a!=expr.arity()) throw new ErrorFatal("Skolem "+label+" must be associated with an "+a+"-ary relational value."); + ExprVar v = ExprVar.make(Pos.UNKNOWN, label, type); + a2k.put(v, expr); + skolems.add(v); + return v; + } + + /** Returns an unmodifiable copy of the map from each Sig/Field/Skolem/Atom to its corresponding Kodkod expression. */ + ConstMap a2k() { return ConstMap.make(a2k); } + + /** Returns an unmodifiable copy of the map from each String literal to its corresponding Kodkod expression. */ + ConstMap s2k() { return s2k; } + + /** Returns the corresponding Kodkod expression for the given Sig, or null if it is not associated with anything. */ + Expression a2k(Sig sig) { return a2k.get(sig); } + + /** Returns the corresponding Kodkod expression for the given Field, or null if it is not associated with anything. */ + Expression a2k(Field field) { return a2k.get(field); } + + /** Returns the corresponding Kodkod expression for the given Atom/Skolem, or null if it is not associated with anything. */ + Expression a2k(ExprVar var) { return a2k.get(var); } + + /** Returns the corresponding Kodkod expression for the given String constant, or null if it is not associated with anything. */ + Expression a2k(String stringConstant) { return s2k.get(stringConstant); } + + /** Returns the corresponding Kodkod expression for the given expression, or null if it is not associated with anything. */ + Expression a2k(Expr expr) throws ErrorFatal { + while(expr instanceof ExprUnary) { + if (((ExprUnary)expr).op==ExprUnary.Op.NOOP) { expr = ((ExprUnary)expr).sub; continue; } + if (((ExprUnary)expr).op==ExprUnary.Op.EXACTLYOF) { expr = ((ExprUnary)expr).sub; continue; } + break; + } + if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.EMPTYNESS) return Expression.NONE; + if (expr instanceof ExprConstant && ((ExprConstant)expr).op==ExprConstant.Op.STRING) return s2k.get(((ExprConstant)expr).string); + if (expr instanceof Sig || expr instanceof Field || expr instanceof ExprVar) return a2k.get(expr); + if (expr instanceof ExprBinary) { + Expr a=((ExprBinary)expr).left, b=((ExprBinary)expr).right; + switch(((ExprBinary)expr).op) { + case ARROW: return a2k(a).product(a2k(b)); + case PLUS: return a2k(a).union(a2k(b)); + case MINUS: return a2k(a).difference(a2k(b)); + //TODO: IPLUS, IMINUS??? + } + } + return null; // Current only UNION, PRODUCT, and DIFFERENCE of Sigs and Fields and ExprConstant.EMPTYNESS are allowed in a defined field's definition. + } + + /** Return a modifiable TupleSet representing a sound overapproximation of the given expression. */ + TupleSet approximate(Expression expression) { + return factory.setOf(expression.arity(), Translator.approximate(expression, bounds, solver.options()).denseIndices()); + } + + /** Query the Bounds object to find the lower/upper bound; throws ErrorFatal if expr is not Relation, nor a {union, product} of Relations. */ + TupleSet query(boolean findUpper, Expression expr, boolean makeMutable) throws ErrorFatal { + if (expr==Relation.NONE) return factory.noneOf(1); + if (expr==Relation.INTS) return makeMutable ? sigintBounds.clone() : sigintBounds; + if (expr==KK_SEQIDX) return makeMutable ? seqidxBounds.clone() : seqidxBounds; + if (expr==KK_STRING) return makeMutable ? stringBounds.clone() : stringBounds; + if (expr==KK_TIME) return makeMutable ? timeBounds.clone() : timeBounds; // pt.uminho.haslab: time bounds (deprecated) + if (expr instanceof Relation) { + TupleSet ans = findUpper ? bounds.upperBound((Relation)expr) : bounds.lowerBound((Relation)expr); + if (ans!=null) return makeMutable ? ans.clone() : ans; + } + else if (expr instanceof BinaryExpression) { + BinaryExpression b = (BinaryExpression)expr; + if (b.op() == ExprOperator.UNION) { + TupleSet left = query(findUpper, b.left(), true); + TupleSet right = query(findUpper, b.right(), false); + left.addAll(right); + return left; + } else if (b.op() == ExprOperator.PRODUCT) { + TupleSet left = query(findUpper, b.left(), true); + TupleSet right = query(findUpper, b.right(), false); + return left.product(right); + } + } + throw new ErrorFatal("Unknown expression encountered during bounds computation: "+expr); + } + + /** Shrink the bounds for the given relation; throws an exception if the new bounds is not sameAs/subsetOf the old bounds. */ + void shrink(Relation relation, TupleSet lowerBound, TupleSet upperBound) throws Err { + if (solved) throw new ErrorFatal("Cannot shrink a Kodkod relation since solve() has completed."); + TupleSet oldL = bounds.lowerBound(relation); + TupleSet oldU = bounds.upperBound(relation); + if (oldU.containsAll(upperBound) && upperBound.containsAll(lowerBound) && lowerBound.containsAll(oldL)) { + bounds.bound(relation, lowerBound, upperBound); + } else { + throw new ErrorAPI("Inconsistent bounds shrinking on relation: "+relation); + } + } + + //===================================================================================================// + + /** Returns true iff the problem has been solved and the result is satisfiable. */ + public boolean satisfiable() { return eval!=null; } + + /** Returns an unmodifiable copy of the list of all sigs in this solution's model; always contains UNIV+SIGINT+SEQIDX+STRING+NONE and has no duplicates. */ + public SafeList getAllReachableSigs() { return sigs.dup(); } + + /** 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(); } + + /** Returns an unmodifiable copy of the list of all atoms if the problem is solved and is satisfiable; else returns an empty list. */ + public Iterable getAllAtoms() { return atoms.dup(); } + + /** Returns the short unique name corresponding to the given atom if the problem is solved and is satisfiable; else returns atom.toString(). */ + String atom2name(Object atom) { String ans=atom2name.get(atom); return ans==null ? atom.toString() : ans; } + + /** Returns the most specific sig corresponding to the given atom if the problem is solved and is satisfiable; else returns UNIV. */ + PrimSig atom2sig(Object atom) { PrimSig sig=atom2sig.get(atom); return sig==null ? UNIV : sig; } + + /** Caches eval(Sig) and eval(Field) results. */ + private Map evalCache = new LinkedHashMap(); + + /** Return the A4TupleSet for the given sig (if solution not yet solved, or unsatisfiable, or sig not found, then return an empty tupleset) */ + public A4TupleSet eval(Sig sig) { + try { + if (!solved || eval==null) return new A4TupleSet(factory.noneOf(1), this); + A4TupleSet ans = evalCache.get(sig); + if (ans!=null) return ans; + TupleSet ts = eval.evaluate((Expression) TranslateAlloyToKodkod.alloy2kodkod(this, sig)); + ans = new A4TupleSet(ts, this); + evalCache.put(sig, ans); + return ans; + } catch(Err er) { + return new A4TupleSet(factory.noneOf(1), this); + } + } + + /** Return the A4TupleSet for the given field (if solution not yet solved, or unsatisfiable, or field not found, then return an empty tupleset) */ + public A4TupleSet eval(Field field) { + try { + if (!solved || eval==null) return new A4TupleSet(factory.noneOf(field.type().arity()), this); + A4TupleSet ans = evalCache.get(field); + if (ans!=null) return ans; + TupleSet ts = eval.evaluate((Expression) TranslateAlloyToKodkod.alloy2kodkod(this, field)); + ans = new A4TupleSet(ts, this); + evalCache.put(field, ans); + return ans; + } catch(Err er) { + return new A4TupleSet(factory.noneOf(field.type().arity()), this); + } + } + + /** If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean. */ + public Object eval(Expr expr) throws Err { + try { + if (expr instanceof Sig) return eval((Sig)expr); + if (expr instanceof Field) return eval((Field)expr); + if (!solved) throw new ErrorAPI("This solution is not yet solved, so eval() is not allowed."); + if (eval==null) throw new ErrorAPI("This solution is unsatisfiable, so eval() is not allowed."); + if (expr.ambiguous && !expr.errors.isEmpty()) expr = expr.resolve(expr.type(), null); + if (!expr.errors.isEmpty()) throw expr.errors.pick(); + Object result = TranslateAlloyToKodkod.alloy2kodkod(this, expr); + if (result instanceof IntExpression) return eval.evaluate((IntExpression)result) + (eval.wasOverflow() ? " (OF)" : ""); + if (result instanceof Formula) return eval.evaluate((Formula)result); + if (result instanceof Expression) return new A4TupleSet(eval.evaluate((Expression)result), this); + throw new ErrorFatal("Unknown internal error encountered in the evaluator."); + } catch(CapacityExceededException ex) { + throw TranslateAlloyToKodkod.rethrow(ex); + } + } + + /** Returns the Kodkod instance represented by this solution; throws an exception if the problem is not yet solved or if it is unsatisfiable. */ + public Instance debugExtractKInstance() throws Err { + if (!solved) throw new ErrorAPI("This solution is not yet solved, so instance() is not allowed."); + if (eval==null) throw new ErrorAPI("This solution is unsatisfiable, so instance() is not allowed."); + return eval.instance().unmodifiableView(); + } + + //===================================================================================================// + + /** Maps a Kodkod formula to an Alloy Expr or Alloy Pos (or null if no such mapping) */ + Object k2pos(Node formula) { return k2pos.get(formula); } + + /** Associates the Kodkod formula to a particular Alloy Expr (if the Kodkod formula is not already associated with an Alloy Expr or Alloy Pos) */ + Formula k2pos(Formula formula, Expr expr) throws Err { + if (solved) throw new ErrorFatal("Cannot alter the k->pos mapping since solve() has completed."); + if (formula==null || expr==null || k2pos.containsKey(formula)) return formula; + k2pos.put(formula, expr); + if (formula instanceof BinaryFormula) { + BinaryFormula b = (BinaryFormula)formula; + if (b.op() == FormulaOperator.AND) { k2pos(b.left(), expr); k2pos(b.right(), expr); } + } + return formula; + } + + /** Associates the Kodkod formula to a particular Alloy Pos (if the Kodkod formula is not already associated with an Alloy Expr or Alloy Pos) */ + Formula k2pos(Formula formula, Pos pos) throws Err { + if (solved) throw new ErrorFatal("Cannot alter the k->pos mapping since solve() has completed."); + if (formula==null || pos==null || pos==Pos.UNKNOWN || k2pos.containsKey(formula)) return formula; + k2pos.put(formula, pos); + if (formula instanceof BinaryFormula) { + BinaryFormula b = (BinaryFormula)formula; + if (b.op() == FormulaOperator.AND) { k2pos(b.left(), pos); k2pos(b.right(), pos); } + } + return formula; + } + + //===================================================================================================// + + /** Associates the Kodkod relation to a particular Alloy Type (if it is not already associated with something) */ + void kr2type(Relation relation, Type newType) throws Err { + if (solved) throw new ErrorFatal("Cannot alter the k->type mapping since solve() has completed."); + if (!rel2type.containsKey(relation)) rel2type.put(relation, newType); + } + + /** Remove all mapping from Kodkod relation to Alloy Type. */ + void kr2typeCLEAR() throws Err { + if (solved) throw new ErrorFatal("Cannot clear the k->type mapping since solve() has completed."); + rel2type.clear(); + } + + //===================================================================================================// + + /** Caches a constant pair of Type.EMPTY and Pos.UNKNOWN */ + private Pair cachedPAIR = null; + + /** Maps a Kodkod variable to an Alloy Type and Alloy Pos (if no association exists, it will return (Type.EMPTY , Pos.UNKNOWN) */ + Pair kv2typepos(Variable var) { + Pair ans=decl2type.get(var); + if (ans!=null) return ans; + if (cachedPAIR==null) cachedPAIR=new Pair(Type.EMPTY, Pos.UNKNOWN); + return cachedPAIR; + } + + /** Associates the Kodkod variable to a particular Alloy Type and Alloy Pos (if it is not already associated with something) */ + void kv2typepos(Variable var, Type type, Pos pos) throws Err { + if (solved) throw new ErrorFatal("Cannot alter the k->type mapping since solve() has completed."); + if (type==null) type=Type.EMPTY; + if (pos==null) pos=Pos.UNKNOWN; + if (!decl2type.containsKey(var)) decl2type.put(var, new Pair(type, pos)); + } + + //===================================================================================================// + + /** Add the given formula to the list of Kodkod formulas, and associate it with the given Pos object (pos can be null if unknown). */ + void addFormula(Formula newFormula, Pos pos) throws Err { + if (solved) throw new ErrorFatal("Cannot add an additional formula since solve() has completed."); + if (formulas.size()>0 && formulas.get(0)==Formula.FALSE) return; // If one formula is false, we don't need the others + if (newFormula==Formula.FALSE) formulas.clear(); // If one formula is false, we don't need the others + formulas.add(newFormula); + if (pos!=null && pos!=Pos.UNKNOWN) k2pos(newFormula, pos); + } + + /** Add the given formula to the list of Kodkod formulas, and associate it with the given Expr object (expr can be null if unknown) */ + void addFormula(Formula newFormula, Expr expr) throws Err { + if (solved) throw new ErrorFatal("Cannot add an additional formula since solve() has completed."); + if (formulas.size()>0 && formulas.get(0)==Formula.FALSE) return; // If one formula is false, we don't need the others + if (newFormula==Formula.FALSE) formulas.clear(); // If one formula is false, we don't need the others + formulas.add(newFormula); + if (expr!=null) k2pos(newFormula, expr); + } + + //===================================================================================================// + + /** Helper class that wraps an iterator up where it will pre-fetch the first element (note: it will not prefetch subsequent elements). */ + private static final class Peeker implements Iterator { + /** The encapsulated iterator. */ + private Iterator iterator; + /** True iff we have captured the first element. */ + private boolean hasFirst; + /** If hasFirst is true, then this is the captured first element. */ + private T first; + /** Constructrs a Peeker object. */ + private Peeker(Iterator it) { + iterator = it; + if (it.hasNext()) { hasFirst=true; first=it.next(); } + } + /** {@inheritDoc} */ + public boolean hasNext() { + return hasFirst || iterator.hasNext(); + } + /** {@inheritDoc} */ + public T next() { + if (hasFirst) { hasFirst=false; T ans=first; first=null; return ans; } else return iterator.next(); + } + /** {@inheritDoc} */ + public void remove() { throw new UnsupportedOperationException(); } + } + + //===================================================================================================// + + /** Helper method to determine if a given binary relation is a total order over a given unary relation. */ + private static List isOrder(TupleSet b, TupleSet u) { + // Size check + final int n = u.size(); + final List list = new ArrayList(n); + if (b.size() == 0 && n <= 1) return list; + if (b.size() != n-1) return null; + // Find the starting element + Tuple head = null; + TupleSet right = b.project(1); + for(Tuple x: u) if (!right.contains(x)) {head = x; break;} + if (head==null) return null; + final TupleFactory f = head.universe().factory(); + // Form the list + list.add(head); + while(true) { + // Find head.next + Tuple headnext = null; + for(Tuple x: b) if (x.atom(0)==head.atom(0)) { headnext = f.tuple(x.atom(1)); break; } + // If we've reached the end of the chain, and indeed we've formed exactly n elements (and all are in u), we're done + if (headnext==null) return list.size()==n ? list : null; + // If we've accumulated more than n elements, or if we reached an element not in u, then we declare failure + if (list.size()==n || !u.contains(headnext)) return null; + // Move on to the next step + head = headnext; + list.add(head); + } + } + + /** Helper method that chooses a name for each atom based on its most specific sig; (external caller should call this method with s==null and nexts==null) */ + private static void rename (A4Solution frame, PrimSig s, Map> nexts, UniqueNameGenerator un) throws Err { + if (s==null) { + for(ExprVar sk:frame.skolems) un.seen(sk.label); + // Store up the skolems + List skolems = new ArrayList(); + for(Map.Entry e: frame.rel2type.entrySet()) { + Relation r = e.getKey(); if (!frame.eval.instance().contains(r)) continue; + Type t = e.getValue(); if (t.arity() > r.arity()) continue; // Something is wrong; let's skip it + while (t.arity() < r.arity()) t = UNIV.type().product(t); + String n = Util.tail(r.name()); + while(n.length()>0 && n.charAt(0)=='$') n = n.substring(1); + skolems.add(n); + skolems.add(t); + skolems.add(r); + } + // Find all suitable "next" or "prev" relations + nexts = new LinkedHashMap>(); + for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("next")==0) { + List> fold = f.type().fold(); + if (fold.size()==1) { + List t = fold.get(0); + if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) { + TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1))); + if (set.size()<=1) continue; + TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f))); + List test = isOrder(next, set); + if (test!=null) nexts.put(t.get(1), test); + } else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) { + TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0))); + if (set.size()<=1) continue; + TupleSet next = frame.eval.evaluate(frame.a2k(f)); + List test = isOrder(next, set); + if (test!=null) nexts.put(t.get(1), test); + } + } + } + for(Sig sig:frame.sigs) for(Field f: sig.getFields()) if (f.label.compareToIgnoreCase("prev")==0) { + List> fold = f.type().fold(); + if (fold.size()==1) { + List t = fold.get(0); + if (t.size()==3 && t.get(0).isOne!=null && t.get(1)==t.get(2) && !nexts.containsKey(t.get(1))) { + TupleSet set = frame.eval.evaluate(frame.a2k(t.get(1))); + if (set.size()<=1) continue; + TupleSet next = frame.eval.evaluate(frame.a2k(t.get(0)).join(frame.a2k(f)).transpose()); + List test = isOrder(next, set); + if (test!=null) nexts.put(t.get(1), test); + } else if (t.size()==2 && t.get(0)==t.get(1) && !nexts.containsKey(t.get(0))) { + TupleSet set = frame.eval.evaluate(frame.a2k(t.get(0))); + if (set.size()<=1) continue; + TupleSet next = frame.eval.evaluate(frame.a2k(f).transpose()); + List test = isOrder(next, set); + if (test!=null) nexts.put(t.get(1), test); + } + } + } + // Assign atom->name and atom->MostSignificantSig + for(Tuple t:frame.eval.evaluate(Relation.INTS)) { frame.atom2sig.put(t.atom(0), SIGINT); } + for(Tuple t:frame.eval.evaluate(KK_SEQIDX)) { frame.atom2sig.put(t.atom(0), SEQIDX); } + for(Tuple t:frame.eval.evaluate(KK_STRING)) { frame.atom2sig.put(t.atom(0), STRING); } + for(Tuple t:frame.eval.evaluate(KK_TIME)) { frame.atom2sig.put(t.atom(0), TIME); } // pt.uminho.haslab: time sig (deprecated) + for(Sig sig:frame.sigs) if (sig instanceof PrimSig && !sig.builtin && ((PrimSig)sig).isTopLevel()) rename(frame, (PrimSig)sig, nexts, un); + // These are redundant atoms that were not chosen to be in the final instance + int unused=0; + for(Tuple tuple:frame.eval.evaluate(Relation.UNIV)) { + Object atom = tuple.atom(0); + if (!frame.atom2sig.containsKey(atom)) { frame.atom2name.put(atom, "unused"+unused); unused++; } + } + // Add the skolems + for(int num=skolems.size(), i=0; i0 && n.charAt(0)=='$') n=n.substring(1); + Type t = (Type) skolems.get(i+1); + Relation r = (Relation) skolems.get(i+2); + frame.addSkolem(un.make("$"+n), t, r); + } + return; + } + for(PrimSig c: s.children()) rename(frame, c, nexts, un); + String signame = un.make(s.label.startsWith("this/") ? s.label.substring(5) : s.label); + List list = new ArrayList(); + for(Tuple t: frame.eval.evaluate(frame.a2k(s))) list.add(t); + List order = nexts.get(s); + if (order!=null && order.size()==list.size() && order.containsAll(list)) { list=order; } + int i = 0; + for(Tuple t: list) { + if (frame.atom2sig.containsKey(t.atom(0))) continue; // This means one of the subsig has already claimed this atom. + String x = signame + "$" + i; + i++; + frame.atom2sig.put(t.atom(0), s); + frame.atom2name.put(t.atom(0), x); + ExprVar v = ExprVar.make(null, x, s.type()); + TupleSet ts = t.universe().factory().range(t, t); + Relation r = Relation.unary(x); + frame.eval.instance().add(r, ts); + frame.a2k.put(v, r); + frame.atoms.add(v); + } + } + + //===================================================================================================// + + /** Solve for the solution if not solved already; if cmd==null, we will simply use the lowerbound of each relation as its value. */ + // pt.uminho.haslab: extended with time + A4Solution solve(final A4Reporter rep, Command cmd, Simplifier simp, boolean tryBookExamples) throws Err, IOException { + // If already solved, then return this object as is + if (solved) return this; + // If cmd==null, then all four arguments are ignored, and we simply use the lower bound of each relation + if (cmd==null) { + Instance inst = new Instance(bounds.universe()); + for(int max=max(), i=min(); i<=max; i++) { + Tuple it = factory.tuple(""+i); + inst.add(i, factory.range(it, it)); + } + for(Relation r: bounds.relations()) inst.add(r, bounds.lowerBound(r)); + eval = new Evaluator(inst, solver.options()); + rename(this, null, null, new UniqueNameGenerator()); + solved(); + return this; + } + // Otherwise, prepare to do the solve... + final A4Options opt = originalOptions; + long time = System.currentTimeMillis(); + rep.debug("Simplifying the bounds...\n"); + if (simp!=null && formulas.size()>0 && !simp.simplify(rep, this, formulas)) addFormula(Formula.FALSE, Pos.UNKNOWN); + rep.translate(opt.solver.id(), bitwidth, maxseq, solver.options().skolemDepth(), solver.options().symmetryBreaking()); + Formula 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}; + solver.options().setReporter(new AbstractReporter() { // Set up a reporter to catch the type+pos of skolems + @Override public void skolemizing(Decl decl, Relation skolem, List predecl) { + try { + Type t=kv2typepos(decl.variable()).a; + if (t==Type.EMPTY) return; + for(int i=(predecl==null ? -1 : predecl.size()-1); i>=0; i--) { + Type pp=kv2typepos(predecl.get(i).variable()).a; + if (pp==Type.EMPTY) return; + t=pp.product(t); + } + kr2type(skolem, t); + } catch(Throwable ex) { } // Exception here is not fatal + } + @Override public void solvingCNF(int primaryVars, int vars, int clauses) { + if (solved[0]) return; else solved[0]=true; // initially solved[0] is true, so we won't report the # of vars/clauses + if (rep!=null) rep.solve(primaryVars, vars, clauses); + } + }); + if (!opt.solver.equals(SatSolver.CNF) && !opt.solver.equals(SatSolver.KK) && tryBookExamples) { // try book examples + A4Reporter r = "yes".equals(System.getProperty("debug")) ? rep : null; + try { sol = BookExamples.trial(r, this, fgoal, solver, cmd.check); } catch(Throwable ex) { sol = null; } + } + solved[0] = false; // this allows the reporter to report the # of 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(SatSolver.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(SatSolver.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()) { + if (sol==null) sol = solver.solve(fgoal, bounds); + } else { + kEnumerator = new Peeker(solver.solveAll(fgoal, bounds)); + if (sol==null) sol = kEnumerator.next(); + } + if (!solved[0]) rep.solve(0, 0, 0); + final Instance inst = sol.instance(); + // To ensure no more output during SolutionEnumeration + solver.options().setReporter(oldReporter); + // If unsatisfiable, then retreive the unsat core if desired + if (inst==null && solver.options().solver()==SATFactory.MiniSatProver) { + try { + lCore = new LinkedHashSet(); + Proof p = sol.proof(); + if (sol.outcome()==UNSATISFIABLE) { + // only perform the minimization if it was UNSATISFIABLE, rather than TRIVIALLY_UNSATISFIABLE + int i = p.highLevelCore().size(); + rep.minimizing(cmd, i); + if (opt.coreMinimization==0) try { p.minimize(new RCEStrategy(p.log())); } catch(Throwable ex) {} + if (opt.coreMinimization==1) try { p.minimize(new HybridStrategy(p.log())); } catch(Throwable ex) {} + rep.minimized(cmd, i, p.highLevelCore().size()); + } + for(Iterator it=p.core(); it.hasNext();) { + Object n=it.next().node(); + if (n instanceof Formula) lCore.add((Formula)n); + } + Map map = p.highLevelCore(); + hCore = new LinkedHashSet(map.keySet()); + hCore.addAll(map.values()); + } catch(Throwable ex) { + lCore = hCore = null; + } + } + // If satisfiable, then add/rename the atoms and skolems + if (inst!=null) { + eval = new Evaluator(inst, solver.options()); + rename(this, null, null, new UniqueNameGenerator()); + } + // report the result + solved(); + time = System.currentTimeMillis() - time; + if (eval!=null) { + String[] aux0 = eval(PrimSig.TIME.join(ExprConstant.LOOP)).toString().split("\\$"); // pt.uminho.haslab + if (aux0.length > 1) { + String aux = aux0[1]; + // rep.debug("LOOP: "+eval((ExprConstant.LOOP)).toString()); + // rep.debug("NEXT: "+eval((ExprConstant.NEXTTIME)).toString()); + loop = Integer.parseInt(aux.substring(0, aux.length()-1)); + } + } + + if (inst!=null) rep.resultSAT(cmd, time, this); else rep.resultUNSAT(cmd, time, this); + return this; + } + + //===================================================================================================// + + /** This caches the toString() output. */ + private String toStringCache = null; + + /** Dumps the Kodkod solution into String. */ + // pt.uminho.haslab: extended with time + @Override public String toString() { + if (!solved) return "---OUTCOME---\nUnknown.\n"; + if (eval == null) return "---OUTCOME---\nUnsatisfiable.\n"; + String answer = toStringCache; + if (answer != null) return answer; + Instance sol = eval.instance(); + StringBuilder sb = new StringBuilder(); + sb.append("---INSTANCE---\n" + "integers={"); + boolean firstTuple = true; + for(IndexedEntry e:sol.intTuples()) { + if (firstTuple) firstTuple=false; else sb.append(", "); + // No need to print e.index() since we've ensured the Int atom's String representation is always equal to ""+e.index() + Object atom = e.value().iterator().next().atom(0); + sb.append(atom2name(atom)); + } + sb.append("}\n"); + try { + for(Sig s:sigs) { + sb.append(s.label).append("=").append(eval(s)).append("\n"); + for(Field f:s.getFields()) sb.append(s.label).append("<:").append(f.label).append("=").append(eval(f)).append("\n"); + } + for(ExprVar v:skolems) { + sb.append("skolem ").append(v.label).append("=").append(eval(v)).append("\n"); + } + sb.append("loop ").append(eval(ExprConstant.LOOP)).append("\n"); // pt.uminho.haslab: time relations + sb.append("next ").append(eval(ExprConstant.NEXTTIME)).append("\n"); // pt.uminho.haslab: time relations + sb.append("next ").append(eval.evaluate(KK_TIMEINIT)).append("\n"); // pt.uminho.haslab: time relations + + return toStringCache = sb.toString(); + } catch(Err er) { + return toStringCache = (""); + } + } + + //===================================================================================================// + + /** If nonnull, it caches the result of calling "next()". */ + private A4Solution nextCache = null; + + /** If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT). + * @throws ErrorAPI if the solver was not an incremental solver + */ + public A4Solution next() throws Err { + if (!solved) throw new ErrorAPI("This solution is not yet solved, so next() is not allowed."); + if (eval==null) return this; + if (nextCache==null) nextCache=new A4Solution(this); + return nextCache; + } + + /** Returns true if this solution was generated by an incremental SAT solver. */ + public boolean isIncremental() { return kEnumerator!=null; } + + //===================================================================================================// + + /** The low-level unsat core; null if it is not available. */ + private LinkedHashSet lCore = null; + + /** This caches the result of lowLevelCore(). */ + private Set lCoreCache = null; + + /** If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set. */ + public Set lowLevelCore() { + if (lCoreCache!=null) return lCoreCache; + Set ans1 = new LinkedHashSet(); + if (lCore!=null) for(Node f: lCore) { + Object y = k2pos(f); + if (y instanceof Pos) ans1.add( (Pos)y ); else if (y instanceof Expr) ans1.add( ((Expr)y).span() ); + } + return lCoreCache = Collections.unmodifiableSet(ans1); + } + + //===================================================================================================// + + /** The high-level unsat core; null if it is not available. */ + private LinkedHashSet hCore = null; + + /** This caches the result of highLevelCore(). */ + private Pair,Set> hCoreCache = null; + + /** If this solution is unsatisfiable and its unsat core is available, then return the core; else return an empty set. */ + public Pair,Set> highLevelCore() { + if (hCoreCache!=null) return hCoreCache; + Set ans1 = new LinkedHashSet(), ans2 = new LinkedHashSet(); + if (hCore!=null) for(Node f: hCore) { + Object x = k2pos(f); + if (x instanceof Pos) { + // System.out.println("F: "+f+" at "+x+"\n"); System.out.flush(); + ans1.add((Pos)x); + } else if (x instanceof Expr) { + Expr expr = (Expr)x; + Pos p = ((Expr)x).span(); + ans1.add(p); + // System.out.println("F: "+f+" by "+p.x+","+p.y+"->"+p.x2+","+p.y2+" for "+x+"\n\n"); System.out.flush(); + for(Func func: expr.findAllFunctions()) ans2.add(func.getBody().span()); + } + } + return hCoreCache = new Pair,Set>(Collections.unmodifiableSet(ans1), Collections.unmodifiableSet(ans2)); + } + + //===================================================================================================// + + /** Helper method to write out a full XML file. */ + public void writeXML(String filename) throws Err { + writeXML(filename, null, null); + } + + /** Helper method to write out a full XML file. */ + public void writeXML(String filename, Iterable macros) throws Err { + writeXML(filename, macros, null); + } + + /** Helper method to write out a full XML file. */ + public void writeXML(String filename, Iterable macros, Map sourceFiles) throws Err { + PrintWriter out=null; + try { + out=new PrintWriter(filename,"UTF-8"); + writeXML(out, macros, sourceFiles); + if (!Util.close(out)) throw new ErrorFatal("Error writing the solution XML file."); + } catch(IOException ex) { + Util.close(out); + throw new ErrorFatal("Error writing the solution XML file.", ex); + } + } + + /** Helper method to write out a full XML file. */ + public void writeXML(A4Reporter rep, String filename, Iterable macros, Map sourceFiles) throws Err { + PrintWriter out=null; + try { + out=new PrintWriter(filename,"UTF-8"); + writeXML(rep, out, macros, sourceFiles); + if (!Util.close(out)) throw new ErrorFatal("Error writing the solution XML file."); + } catch(IOException ex) { + Util.close(out); + throw new ErrorFatal("Error writing the solution XML file.", ex); + } + } + + /** Helper method to write out a full XML file. */ + public void writeXML(PrintWriter writer, Iterable macros, Map sourceFiles) throws Err { + A4SolutionWriter.writeInstance(null, this, writer, macros, sourceFiles); + if (writer.checkError()) throw new ErrorFatal("Error writing the solution XML file."); + } + + /** Helper method to write out a full XML file. */ + public void writeXML(A4Reporter rep, PrintWriter writer, Iterable macros, Map sourceFiles) throws Err { + A4SolutionWriter.writeInstance(rep, this, writer, macros, sourceFiles); + if (writer.checkError()) throw new ErrorFatal("Error writing the solution XML file."); + } } diff --git a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java index 0f4e6723..f010af88 100644 --- a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java +++ b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionReader.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyright (c) 2014-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -49,7 +50,10 @@ import edu.mit.csail.sdg.alloy4compiler.ast.Sig.PrimSig; import edu.mit.csail.sdg.alloy4compiler.ast.Sig.SubsetSig; -/** This helper class contains helper routines for reading an A4Solution object from an XML file. */ +/** This helper class contains helper routines for reading an A4Solution object from an XML file. + * + * @modified: nmm + * */ public final class A4SolutionReader { @@ -72,7 +76,7 @@ public final class A4SolutionReader { private final Map id2sig = new LinkedHashMap(); /** Stores the set of all sigs. */ - private final Set allsigs = Util.asSet((Sig)UNIV, SIGINT, SEQIDX, STRING, NONE, TIME); //pt.uminho.haslab + private final Set allsigs = Util.asSet((Sig)UNIV, SIGINT, SEQIDX, STRING, NONE, TIME); //pt.uminho.haslab: time sigs /** Mapes each expression we've seen to its TupleSet. */ private final Map expr2ts = new LinkedHashMap(); @@ -138,7 +142,7 @@ private Sig parseSig(String id, int depth) throws IOException, Err { if (label.equals(SIGINT.label)) { id2sig.put(id, SIGINT); return SIGINT; } if (label.equals(SEQIDX.label)) { id2sig.put(id, SEQIDX); return SEQIDX; } if (label.equals(STRING.label)) { id2sig.put(id, STRING); return STRING; } - if (label.equals(TIME.label)) { id2sig.put(id, TIME); return TIME; } // pt.uminho.haslab + if (label.equals(TIME.label)) { id2sig.put(id, TIME); return TIME; } // pt.uminho.haslab: time sigs throw new IOException("Unknown builtin sig: "+label+" (id="+id+")"); } if (depth > nmap.size()) throw new IOException("Sig "+label+" (id="+id+") is in a cyclic inheritance relationship."); diff --git a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java index e32e77e6..9bdb9a97 100644 --- a/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java +++ b/src/edu/mit/csail/sdg/alloy4compiler/translator/A4SolutionWriter.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyright (c) 2015-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -37,7 +38,10 @@ import edu.mit.csail.sdg.alloy4compiler.ast.Sig.SubsetSig; import edu.mit.csail.sdg.alloy4compiler.ast.Type; -/** This helper class contains helper routines for writing an A4Solution object out as an XML file. */ +/** This helper class contains helper routines for writing an A4Solution object out as an XML file. + * + * @modified: nmm + * */ public final class A4SolutionWriter { @@ -108,6 +112,7 @@ private boolean writeExpr(String prefix, Expr expr) throws Err { } /** Write the given Sig. */ + // pt.uminho.haslab: extended with time sigs private A4TupleSet writesig(final Sig x) throws Err { A4TupleSet ts = null, ts2 = null; if (x==Sig.NONE) return null; // should not happen, but we test for it anyway @@ -130,7 +135,7 @@ private A4TupleSet writesig(final Sig x) throws Err { if (x.isEnum!=null) out.print("\" enum=\"yes"); out.print("\">\n"); try { - if (sol!=null && x!=Sig.UNIV && x!=Sig.SIGINT && x!=Sig.SEQIDX && x!=Sig.TIME) { // pt.uminho.haslab + if (sol!=null && x!=Sig.UNIV && x!=Sig.SIGINT && x!=Sig.SEQIDX && x!=Sig.TIME) { // pt.uminho.haslab: time sigs ts = (A4TupleSet)(sol.eval(x)); for(A4Tuple t: ts.minus(ts2)) Util.encodeXMLs(out, " \n"); } @@ -174,6 +179,7 @@ private void writeSkolem(ExprVar x) throws Err { } /** If sol==null, write the list of Sigs as a Metamodel, else write the solution as an XML file. */ + // pt.uminho.haslab: extended with time scopes and sigs private A4SolutionWriter(A4Reporter rep, A4Solution sol, Iterable sigs, int bitwidth, int maxseq, int time, int loop, String originalCommand, String originalFileName, PrintWriter out, Iterable extraSkolems) throws Err { this.rep = rep; this.out = out; @@ -181,8 +187,8 @@ private A4SolutionWriter(A4Reporter rep, A4Solution sol, Iterable sigs, int for (Sig s:sigs) if (s instanceof PrimSig && ((PrimSig)s).parent==Sig.UNIV) toplevels.add((PrimSig)s); out.print(" sigs, int } /** If this solution is a satisfiable solution, this method will write it out in XML format. */ + // pt.uminho.haslab: extended with time scopes and sigs static void writeInstance(A4Reporter rep, A4Solution sol, PrintWriter out, Iterable extraSkolems, Map sources) throws Err { if (!sol.satisfiable()) throw new ErrorAPI("This solution is unsatisfiable."); try { Util.encodeXMLs(out, "\n\n"); - new A4SolutionWriter(rep, sol, sol.getAllReachableSigs(), sol.getBitwidth(), sol.getMaxSeq(), sol.getTime(), sol.getLoop(), sol.getOriginalCommand(), sol.getOriginalFilename(), out, extraSkolems); // pt.uminho.haslab + new A4SolutionWriter(rep, sol, sol.getAllReachableSigs(), sol.getBitwidth(), sol.getMaxSeq(), sol.getTime(), sol.getLoop(), sol.getOriginalCommand(), sol.getOriginalFilename(), out, extraSkolems); // pt.uminho.haslab: time scopes if (sources!=null) for(Map.Entry e: sources.entrySet()) { Util.encodeXMLs(out, "\n\n"); } @@ -239,9 +246,10 @@ static void writeInstance(A4Reporter rep, A4Solution sol, PrintWriter out, Itera } /** Write the metamodel as <instance>..</instance> in XML format. */ + // pt.uminho.haslab: extended with time scopes and sigs public static void writeMetamodel(ConstList sigs, String originalFilename, PrintWriter out) throws Err { try { - new A4SolutionWriter(null, null, sigs, 4, 4, 4, 4, "show metamodel", originalFilename, out, null); // pt.uminho.haslab + new A4SolutionWriter(null, null, sigs, 4, 4, 4, 4, "show metamodel", originalFilename, out, null); // pt.uminho.haslab: time scopes } catch(Throwable ex) { if (ex instanceof Err) throw (Err)ex; else throw new ErrorFatal("Error writing the solution XML file.", ex); } diff --git a/src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java b/src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java index 4cbdd5b3..1f13bcc5 100644 --- a/src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java +++ b/src/edu/mit/csail/sdg/alloy4compiler/translator/ScopeComputer.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyrght (c) 2015-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -70,6 +71,8 @@ *
we will give an error message. * *

Please see ScopeComputer.java for the exact rules for deriving the missing scopes. + * + * @modified: nmm */ final class ScopeComputer { @@ -91,7 +94,7 @@ final class ScopeComputer { /** The number of STRING atoms to allocate; -1 if it was not specified. */ private int maxstring = (-1); - private int time = (-1); // pt.uminho.haslab + private int time = (-1); // pt.uminho.haslab: time scopes /** The scope for each sig. */ private final IdentityHashMap sig2scope = new IdentityHashMap(); @@ -110,7 +113,7 @@ public int sig2scope(Sig sig) { if (sig==SIGINT) return 1< sigs, Command cmd) throws Err { this.rep = rep; this.cmd = cmd; @@ -329,9 +333,9 @@ private ScopeComputer(A4Reporter rep, Iterable sigs, Command cmd) throws Er for(Sig s:sigs) if (s.isTopLevel()) computeLowerBound((PrimSig)s); int max = max(), min = min(); if (max >= min) for(int i=min; i<=max; i++) atoms.add(""+i); - time = cmd.time; // pt.uminho.haslab - sig2scope.put(TIME, time < 1 ? 0 : time); // pt.uminho.haslab - if (time > 0) for(int i=0; i 0) for(int i=0; i { @@ -414,6 +418,7 @@ public static A4Solution execute_command (A4Reporter rep, Iterable sigs, Co *

If the return value X is satisfiable, you can call X.next() to get the next satisfying solution X2; * and you can call X2.next() to get the next satisfying solution X3... until you get an unsatisfying solution. */ + // pt.uminho.haslab: extended for timed iterations public static A4Solution execute_commandFromBook (A4Reporter rep, Iterable sigs, Command cmd, A4Options opt) throws Err { if (rep==null) rep = A4Reporter.NOP; TranslateAlloyToKodkod tr = null; @@ -599,10 +604,10 @@ private static Relation right(Expression x) { case MIN: return IntConstant.constant(min); //TODO case MAX: return IntConstant.constant(max); //TODO case NEXT: return A4Solution.KK_NEXT; - case NEXTTIME: return A4Solution.KK_TIMENEXT; // pt.uminho.haslab - case END: return A4Solution.KK_TIMEEND; // pt.uminho.haslab - case LOOP: return A4Solution.KK_TIMELOOP; // pt.uminho.haslab - case INIT: return A4Solution.KK_TIMEINIT; // pt.uminho.haslab + case NEXTTIME: return A4Solution.KK_TIMENEXT; // pt.uminho.haslab: time relations (deprecated) + case END: return A4Solution.KK_TIMEEND; // pt.uminho.haslab: time relations (deprecated) + case LOOP: return A4Solution.KK_TIMELOOP; // pt.uminho.haslab: time relations (deprecated) + case INIT: return A4Solution.KK_TIMEINIT; // pt.uminho.haslab: time relations (deprecated) case TRUE: return Formula.TRUE; case FALSE: return Formula.FALSE; case EMPTYNESS: return Expression.NONE; diff --git a/src/edu/mit/csail/sdg/alloy4viz/AlloyType.java b/src/edu/mit/csail/sdg/alloy4viz/AlloyType.java index bc7d8ac5..e0d6fbbf 100644 --- a/src/edu/mit/csail/sdg/alloy4viz/AlloyType.java +++ b/src/edu/mit/csail/sdg/alloy4viz/AlloyType.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyright (c) 2015-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -20,6 +21,8 @@ /** Immutable; represents an Alloy toplevel signature or an Alloy subsignature. * *

Thread Safety: Can be called only by the AWT event thread. + * + * @modified: nmm */ public final class AlloyType extends AlloyNodeElement { @@ -40,7 +43,7 @@ public final class AlloyType extends AlloyNodeElement { public static final AlloyType SET=new AlloyType("set", false, false, false, false, false, false); - public static final AlloyType TIME=new AlloyType("Time", false, false, true, false, false, false); // pt.uminho.haslab + public static final AlloyType TIME=new AlloyType("Time", false, false, true, false, false, false); // pt.uminho.haslab: time types (deprecated) /** Constructs an AlloyType object with that name. */ diff --git a/src/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java b/src/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java index 1cd726da..10e30b84 100644 --- a/src/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java +++ b/src/edu/mit/csail/sdg/alloy4viz/StaticInstanceReader.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyright (c) 2015-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -94,7 +95,7 @@ private AlloyType makeType(String label, boolean isOne, boolean isAbstract, bool /** Create a new AlloySet whose label is unambiguous with any existing one. */ private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, AlloyType type) { - while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab + while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab: time sigs while(true) { AlloySet ans = new AlloySet(label, isPrivate, isMeta, type); if (!sets.contains(ans)) return ans; @@ -104,7 +105,7 @@ private AlloySet makeSet(String label, boolean isPrivate, boolean isMeta, AlloyT /** Create a new AlloyRelation whose label is unambiguous with any existing one. */ private AlloyRelation makeRel(String label, boolean isPrivate, boolean isMeta, List types) { - while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab + while(label.equals(Sig.UNIV.label) || label.equals(Sig.SIGINT.label) || label.equals(Sig.SEQIDX.label) || label.equals(Sig.STRING.label) || label.equals(Sig.TIME.label)) label=label+"'"; // pt.uminho.haslab: time sigs while(true) { AlloyRelation ans = new AlloyRelation(label, isPrivate, isMeta, types); if (!rels.containsKey(ans)) return ans; @@ -212,6 +213,7 @@ private void setOrRel(A4Solution sol, String label, Expr expr, boolean isPrivate } /** Parse the file into an AlloyInstance if possible. */ + // pt.uminho.haslab: extended with time sigs private StaticInstanceReader(XMLNode root) throws Err { XMLNode inst = null; for(XMLNode sub: root) if (sub.is("instance")) { inst=sub; break; } @@ -224,7 +226,7 @@ private StaticInstanceReader(XMLNode root) throws Err { sig2type.put(Sig.SIGINT, AlloyType.INT); sig2type.put(Sig.SEQIDX, AlloyType.SEQINT); sig2type.put(Sig.STRING, AlloyType.STRING); - sig2type.put(Sig.TIME, AlloyType.TIME); // pt.uminho.haslab + sig2type.put(Sig.TIME, AlloyType.TIME); // pt.uminho.haslab: time sigs ts.put(AlloyType.SEQINT, AlloyType.INT); for(int i=sol.min(), max=sol.max(), maxseq=sol.getMaxSeq(); i<=max; i++) { AlloyAtom at = new AlloyAtom(i>=0 && i t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(univAtom)) { univAtom=null; break; } for(Set t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(intAtom)) { intAtom=null; break; } for(Set t: rels.values()) for(AlloyTuple at: t) if (at.getAtoms().contains(seqAtom)) { seqAtom=null; break; } @@ -282,7 +284,7 @@ private StaticInstanceReader(XMLNode root) throws Err { } atom2sets.remove(strAtom); } - if (timAtom!=null) { // pt.uminho.haslab + if (timAtom!=null) { // pt.uminho.haslab: time sigs for(Iterator it=exts.iterator(); it.hasNext();) { AlloyTuple at=it.next(); if (at.getStart()==timAtom || at.getEnd()==timAtom) it.remove(); diff --git a/src/edu/mit/csail/sdg/alloy4viz/VizGraphPanel.java b/src/edu/mit/csail/sdg/alloy4viz/VizGraphPanel.java index 568fc2c4..4cc3db7c 100644 --- a/src/edu/mit/csail/sdg/alloy4viz/VizGraphPanel.java +++ b/src/edu/mit/csail/sdg/alloy4viz/VizGraphPanel.java @@ -1,4 +1,5 @@ /* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang + * Electrum -- Copyright (c) 2015-present, Nuno Macedo * * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, @@ -56,6 +57,8 @@ /** GUI panel that houses the actual graph, as well as any projection comboboxes. * *

Thread Safety: Can be called only by the AWT event thread. + * + * @modifed: nmm */ public final class VizGraphPanel extends JPanel { @@ -118,6 +121,7 @@ private boolean upToDate(AlloyType type, List atoms) { * @param type - the type being projected * @param atoms - the list of possible projection atom choices */ + // pt.uminho.haslab: extended to allow loops private TypePanel(AlloyType type, List atoms, AlloyAtom initialValue) { super(); System.out.println("Combo atoms: "+atoms); @@ -135,7 +139,7 @@ private TypePanel(AlloyType type, List atoms, AlloyAtom initialValue) if (this.atoms.get(i).equals(initialValue)) initialIndex=i; } - final int backIndex = vizState.getOriginalInstance().loop; // pt.uminho.haslab + final int backIndex = vizState.getOriginalInstance().loop; // pt.uminho.haslab: loop times add(left = new JButton("<<")); add(Box.createRigidArea(new Dimension(2,2))); add(atomCombo = new OurCombobox(atomnames.length<1 ? new String[]{" "} : atomnames)); @@ -147,7 +151,7 @@ private TypePanel(AlloyType type, List atoms, AlloyAtom initialValue) int idealWidth = Util.onMac() ? 120 : 80; if (dim.width0); - right.setEnabled(initialIndex