diff --git a/pom.xml b/pom.xml index 3c77acb6..05d06cb0 100644 --- a/pom.xml +++ b/pom.xml @@ -4,7 +4,7 @@ 4.0.0 pt.uminho.haslab.pardinus pardinus - 1.2.1 + 1.2.2 jar pardinus diff --git a/src/main/java/kodkod/engine/TemporalPardinusSolver.java b/src/main/java/kodkod/engine/TemporalPardinusSolver.java index e391a8a1..e4278f66 100644 --- a/src/main/java/kodkod/engine/TemporalPardinusSolver.java +++ b/src/main/java/kodkod/engine/TemporalPardinusSolver.java @@ -563,6 +563,10 @@ private Solution nextNonTrivialSolution(int state, int steps, Set fix, private int iteration_stage = 0; private Solution nextNonTrivialSolutionSAT(int state, int steps, Set fix, Set change) { + if (change.isEmpty()) { + translation = null; + return Solution.unsatisfiable(new Statistics(0, 0, 0, 0, 0), null); + } boolean isSat = false; long solveTime = 0; diff --git a/src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java b/src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java index 8fd046f2..207fbb13 100644 --- a/src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java +++ b/src/main/java/kodkod/engine/fol2sat/SymmetryBreaker.java @@ -211,7 +211,7 @@ final BooleanValue generateSBP(LeafInterpreter interpreter, Options options) { int curIndex = indeces.next(); Iterator times = null; if (bounds.relations().contains(TemporalTranslator.STATE)) - bounds.lowerBound(TemporalTranslator.STATE).iterator(); + times = bounds.lowerBound(TemporalTranslator.STATE).iterator(); Tuple time = null; do { for(Iterator rIter = relParts.iterator(); rIter.hasNext() && original.size() < predLength;) { @@ -239,7 +239,7 @@ final BooleanValue generateSBP(LeafInterpreter interpreter, Options options) { continue; boolean zzz = false; - if (times != null) { + if (times != null) { TupleSet yyy = bounds.lowerBound(TemporalTranslator.STATE); Tuple xxx = interpreter.universe().factory().tuple(interpreter.universe().factory().tuple(r.arity(), entry.index()).atom(r.arity()-1)); zzz = yyy.contains(xxx); diff --git a/src/main/java/kodkod/instance/Instance.java b/src/main/java/kodkod/instance/Instance.java index 32524e08..18b69965 100644 --- a/src/main/java/kodkod/instance/Instance.java +++ b/src/main/java/kodkod/instance/Instance.java @@ -34,6 +34,7 @@ import kodkod.ast.ConstantExpression; import kodkod.ast.Expression; import kodkod.ast.Formula; +import kodkod.ast.IntConstant; import kodkod.ast.NaryFormula; import kodkod.ast.Relation; import kodkod.ast.Variable; @@ -235,37 +236,76 @@ public Instance clone() { } } + /** * Converts an instance into a formula that exactly identifies it. Requires that - * every relevant atom be reified into a singleton relation, which may be - * re-used between calls. Relevant atoms are determined from the provided formulas. + * every relevant atom be reified into a singleton relation or quantified in a + * some-disj pattern, which may be re-used between calls. Relevant atoms are + * determined from the provided formulas. * - * Will change if not all atoms of the universe are present at . + * Will change if not all atoms of the universe are present at + * and false. * - * @assumes reif != null - * @param reif - * the previously reified atoms - * @throws NullPointerException - * reif = null + * @assumes reif != null + * @assumes !someDisj => bounds != null + * @param reif the previously reified atoms, as relations or quantified vars depending on + * @param formula a formula from which the relevant relations are identified + * @param someDisj whether the formula will use atoms reified as relations or a some-disj pattern + * @param bounds the problem's bounds, updated if !someDisj + * @throws NullPointerException reif = null + * @throws NullPointerException !someDisj && bounds == null + * @return the formula representing + */ + public Formula formulate(Map reif, Formula formula, boolean someDisj, Bounds bounds) { + return formulate(reif,formula,someDisj,bounds,false); + } + + /** + * Converts an instance into a formula that exactly identifies it. Requires that + * every relevant atom be reified into a singleton relation or quantified in a + * some-disj pattern, which may be re-used between calls. Relevant atoms are + * determined from the provided formulas. + * + * Will change if not all atoms of the universe are present at + * and false. + * + * @assumes reif != null + * @assumes !someDisj => bounds != null + * @param reif the previously reified atoms, as relations or quantified vars depending on + * @param formula a formula from which the relevant relations are identified + * @param someDisj whether the formula will use atoms reified as relations or a some-disj pattern + * @param bounds the problem's bounds, updated if !someDisj + * @param localUniv whether to restrict the universe of atoms locally, only relevant if some-disj pattern + * @throws NullPointerException reif = null + * @throws NullPointerException !someDisj && bounds == null * @return the formula representing */ // [HASLab] - public Formula formulate(Bounds bounds, Map reif, Formula formula, boolean someDisj) { - + public Formula formulate(Map reif, Formula formula, boolean someDisj, Bounds bounds, boolean localUniv) { + Set relevants = formula.accept(new RelationCollector(new HashSet<>())); // reify atoms not yet reified for (int i = 0; i < universe().size(); i++) { - Expression r; - if (reif.keySet().contains(universe().atom(i))) - r = reif.get(universe().atom(i)); - else { - r = Relation.atom(universe().atom(i).toString()); - reif.put(universe().atom(i), r); + // integers do not need to be quantified + if (!universe().atom(i).toString().matches("-?\\d+")) { + Expression r; + if (reif.keySet().contains(universe().atom(i))) + r = reif.get(universe().atom(i)); + else { + if (someDisj) { + r = Variable.unary(universe().atom(i).toString()); + } else { + r = Relation.atom(universe().atom(i).toString()); + } + reif.put(universe().atom(i), r); + } + if (!someDisj && !bounds.relations.contains(r)) + bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(universe().atom(i))); } - if (r instanceof Relation && !bounds.relations.contains(r)) - bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(universe().atom(i))); } + List locals = new ArrayList(); + // create an equality for every relation // a = A + ... && r = A -> B + ... List res = new ArrayList(); @@ -281,6 +321,7 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo if (it.hasNext()) { Tuple u = it.next(); Expression r1 = reif.get(u.atom(0)); + locals.add(r1); for (int i = 1; i < u.arity(); i++) r1 = r1.product(reif.get(u.atom(i))); r = r1; @@ -293,12 +334,26 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo while (it.hasNext()) { Tuple u = it.next(); Expression r1 = reif.get(u.atom(0)); + locals.add(r1); for (int i = 1; i < u.arity(); i++) r1 = r1.product(reif.get(u.atom(i))); r = r.union(r1); } res.add(rel.eq(r)); } + + if (someDisj && localUniv) { + Expression al = null; + for (Expression e : locals) + al = al == null? e : al.union(e); + for (int i = 0; i < universe().size(); i++) + if (universe().atom(i).toString().matches("-?\\d+")) { + Expression intexp = IntConstant.constant(Integer.valueOf(universe().atom(i).toString())).toExpression(); + al = al == null ? intexp : al.union(intexp); + } + res.add(al.eq(Expression.UNIV)); + } + return NaryFormula.and(res); } diff --git a/src/main/java/kodkod/instance/TemporalInstance.java b/src/main/java/kodkod/instance/TemporalInstance.java index d5096ffa..c30f8f7d 100644 --- a/src/main/java/kodkod/instance/TemporalInstance.java +++ b/src/main/java/kodkod/instance/TemporalInstance.java @@ -35,6 +35,7 @@ import kodkod.ast.Decls; import kodkod.ast.Expression; import kodkod.ast.Formula; +import kodkod.ast.IntConstant; import kodkod.ast.Relation; import kodkod.ast.Variable; import kodkod.engine.Evaluator; @@ -235,16 +236,25 @@ public TemporalInstance(Instance instance, PardinusBounds extbounds) { * Will change if not all atoms of the universe are present at . * * @assumes reif != null - * @param bounds the declaration of the relations * @param reif the previously reified atoms * @param formula formula used to identify the relevant relations + * @param bounds the declaration of the relations * @throws NullPointerException reif = null * @return the formula representing */ // [HASLab] @Override - public Formula formulate(Bounds bounds, Map reif, Formula formula, boolean someDisj) { - return formulate(bounds, reif, formula, -1, null, someDisj); + public Formula formulate(Map reif, Formula formula, boolean someDisj, Bounds bounds) { + return formulate(bounds, reif, formula, -1, null, someDisj, true); + } + + @Override + public Formula formulate(Map reif, Formula formula, boolean someDisj, Bounds bounds, boolean localUniv) { + return formulate(bounds, reif, formula, -1, null, someDisj, localUniv); + } + + public Formula formulate(Bounds bounds, Map reif, Formula formula, int start, Integer end, boolean someDisj) { + return formulate(bounds, reif, formula, start, end, someDisj, true); } /** @@ -274,7 +284,7 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo * @return the formula representing */ // [HASLab] - public Formula formulate(Bounds bounds, Map reif, Formula formula, int start, Integer end, boolean someDisj) { + public Formula formulate(Bounds bounds, Map reif, Formula formula, int start, Integer end, boolean someDisj, boolean localUniv) { if (start < -1) throw new IllegalArgumentException("Segment start must be >= -1."); if (end != null && end < start) @@ -283,22 +293,24 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo // reify atoms not yet reified Universe sta_uni = states.get(0).universe(); for (int i = 0; i < sta_uni.size(); i++) { - Expression r; - if (!reif.keySet().contains(sta_uni.atom(i))) { - if (someDisj) { - r = Variable.unary(sta_uni.atom(i).toString()); + // integers do not need to be quantified + if (!sta_uni.atom(i).toString().matches("-?\\d+")) { + Expression r; + if (!reif.keySet().contains(sta_uni.atom(i))) { + if (someDisj) { + r = Variable.unary(sta_uni.atom(i).toString()); + } else { + r = Relation.atom(sta_uni.atom(i).toString()); + } + reif.put(sta_uni.atom(i), r); } else { - r = Relation.atom(sta_uni.atom(i).toString()); + r = reif.get(sta_uni.atom(i)); } - reif.put(sta_uni.atom(i), r); - } else { - r = reif.get(sta_uni.atom(i)); + if (!someDisj && !bounds.relations.contains(r)) + bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(sta_uni.atom(i))); } - if (!someDisj && !bounds.relations.contains((Relation) r)) - bounds.boundExactly((Relation) r, bounds.universe().factory().setOf(sta_uni.atom(i))); } - Set staticss = new HashSet(); for (Relation r : states.get(0).relations()) if (!r.isVariable()) @@ -318,11 +330,11 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo // TODO: the looping formula should also be offset in this case! if (j == null) j = Integer.max(start + (prefixLength() - 1) - loop, prefixLength() - 1); - if (j >= 0) { + if (j != null && j >= 0) { // the state formulas, start from the end and accumulate afters - res = state(j--).formulate(bounds, reif, slcs.getValue(), someDisj); + res = state(j--).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv); for (; j >= Integer.max(0, start); j--) - res = state(j).formulate(bounds, reif, slcs.getValue(), someDisj).and(res.after()); + res = state(j).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv).and(res.after()); // after offset when start > 0 for (; j >= 0; j--) res = res.after(); @@ -331,7 +343,7 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo // the configuration formula, if start = -1 if (start < 0 && !slcs.getKey().equals(Formula.TRUE)) { - Formula sres = states.get(prefixLength() - 1).formulate(bounds, reif, slcs.getKey(), someDisj); + Formula sres = states.get(prefixLength() - 1).formulate(reif, slcs.getKey(), someDisj, bounds, false); res = res.equals(Formula.TRUE) ? sres : sres.and(res); } @@ -340,14 +352,14 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo // create the looping constraint // after^loop always (Sloop => after^(end-loop) Sloop && Sloop+1 => // after^(end-loop) Sloop+1 && ...) - Formula rei = states.get(loop).formulate(bounds, reif, slcs.getValue(), someDisj); + Formula rei = states.get(loop).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv); Formula rei2 = rei; for (int i = loop; i < prefixLength(); i++) rei2 = rei2.after(); Formula looping = rei.implies(rei2); for (int i = loop + 1; i < prefixLength(); i++) { - rei = states.get(i).formulate(bounds, reif, slcs.getValue(), someDisj); + rei = states.get(i).formulate(reif, slcs.getValue(), someDisj, bounds, !localUniv); rei2 = rei; for (int k = loop; k < prefixLength(); k++) rei2 = rei2.after(); @@ -372,7 +384,11 @@ public Formula formulate(Bounds bounds, Map reif, Formula fo decls = decls.and(((Variable) e).oneOf(Expression.UNIV)); } } - res = (al.eq(Expression.UNIV)).and(res); + for (int i = 0; i < sta_uni.size(); i++) + if (sta_uni.atom(i).toString().matches("-?\\d+")) + al = al.union(IntConstant.constant(Integer.valueOf(sta_uni.atom(i).toString())).toExpression()); + if (localUniv) + res = (al.eq(Expression.UNIV)).and(res); res = res.forSome(decls); } } diff --git a/src/main/java/kodkod/util/nodes/PrettyPrinter.java b/src/main/java/kodkod/util/nodes/PrettyPrinter.java index 773684e4..aaac0552 100644 --- a/src/main/java/kodkod/util/nodes/PrettyPrinter.java +++ b/src/main/java/kodkod/util/nodes/PrettyPrinter.java @@ -349,8 +349,8 @@ public void visit(UnaryTempFormula node) { * parenthesized if it's an instance of binary expression or an if expression. **/ // [HASLab] public void visit(TempExpression node) { - keyword(node.op()); visitChild(node.expression(), parenthesize(node.op(), node.expression())); + append(node.op()); } diff --git a/src/test/java/kodkod/test/pardinus/ReificationTests.java b/src/test/java/kodkod/test/pardinus/ReificationTests.java index 5f93af47..737d71af 100644 --- a/src/test/java/kodkod/test/pardinus/ReificationTests.java +++ b/src/test/java/kodkod/test/pardinus/ReificationTests.java @@ -83,9 +83,9 @@ public void testStaticReif() { opt.reporter().debug(inst.toString()); // relations: {a=[[A2]], b=[[B2]]} - assertEquals("((a = $$A2$$) and (b = $$B2$$))", inst.formulate(bounds.clone(), x, formula, false).toString()); + assertEquals("((a = $$A2$$) and (b = $$B2$$))", inst.formulate(x, formula, false, bounds.clone()).toString()); - formula = formula.and(inst.formulate(bounds, x, formula, false).not()); + formula = formula.and(inst.formulate(x, formula, false, bounds).not()); inst = new Instance(uni); inst.add(a, f.range(f.tuple("A1"),f.tuple("A2"))); @@ -96,9 +96,9 @@ public void testStaticReif() { // relations: {a=[[A1], [A2]], b=[[B1], [B2]], $$A2$$=[[A2]], $$B2$$=[[B2]], $$A0$$=[[A0]], $$A1$$=[[A1]], $$B0$$=[[B0]], $$B1$$=[[B1]]} assertEquals("((a = ($$A1$$ + $$A2$$)) and (b = ($$B1$$ + $$B2$$)))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); - formula = formula.and(inst.formulate(bounds, x, formula, false).not()); + formula = formula.and(inst.formulate(x, formula, false, bounds).not()); inst = new Instance(uni); inst.add(a, f.range(f.tuple("A1"),f.tuple("A2"))); @@ -109,7 +109,7 @@ public void testStaticReif() { // relations: {a=[[A1], [A2]], b=[[B2]], $$A1$$=[[A1]], $$A2$$=[[A2]], $$B1$$=[[B1]], $$B2$$=[[B2]], $$A0$$=[[A0]], $$B0$$=[[B0]]} assertEquals("((a = ($$A1$$ + $$A2$$)) and (b = $$B2$$))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); } @@ -159,7 +159,7 @@ public void testTmpReif() { assertEquals( "(((a = none) and after((a = (($$A0$$ + $$A1$$) + $$A2$$)))) and always((((a = none) implies after(after((a = none)))) and ((a = (($$A0$$ + $$A1$$) + $$A2$$)) implies after(after((a = (($$A0$$ + $$A1$$) + $$A2$$))))))))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); inst0 = new Instance(uni); inst0.add(a, f.setOf("A"+(n-1))); @@ -178,7 +178,7 @@ public void testTmpReif() { assertEquals( "(((a = $$A2$$) and after((a = ($$A0$$ + $$A1$$)))) and always((((a = $$A2$$) implies after(after((a = $$A2$$)))) and ((a = ($$A0$$ + $$A1$$)) implies after(after((a = ($$A0$$ + $$A1$$))))))))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); } /* Temporal reification. */ @@ -233,7 +233,7 @@ public void testTmp2Reif() { assertEquals( "((((a = ($$A1$$ + $$A2$$)) and (b = none)) and after((((a = ($$A0$$ + $$A2$$)) and (b = $$B2$$)) and after(((a = $$A1$$) and (b = $$B1$$)))))) and after(always(((((a = ($$A0$$ + $$A2$$)) and (b = $$B2$$)) implies after(after(((a = ($$A0$$ + $$A2$$)) and (b = $$B2$$))))) and (((a = $$A1$$) and (b = $$B1$$)) implies after(after(((a = $$A1$$) and (b = $$B1$$)))))))))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); inst0 = new Instance(uni); inst0.add(a, f.setOf("A2")); @@ -257,7 +257,7 @@ public void testTmp2Reif() { assertEquals( "((((a = $$A2$$) and (b = none)) and after((((a = $$A1$$) and (b = $$B2$$)) and after(((a = ($$A0$$ + $$A2$$)) and (b = $$B1$$)))))) and after(always(((((a = $$A1$$) and (b = $$B2$$)) implies after(after(((a = $$A1$$) and (b = $$B2$$))))) and (((a = ($$A0$$ + $$A2$$)) and (b = $$B1$$)) implies after(after(((a = ($$A0$$ + $$A2$$)) and (b = $$B1$$)))))))))", - inst.formulate(bounds.clone(), x, formula, false).toString()); + inst.formulate(x, formula, false, bounds.clone()).toString()); } @@ -532,9 +532,9 @@ public void testStaticSome() { // relations: {a=[[A2]], b=[[B2]]} - assertEquals("((a = $$A2$$) and (b = $$B2$$))", inst.formulate(bounds.clone(), x, formula, true).toString()); + assertEquals("((a = A2) and (b = B2))", inst.formulate(x, formula, true, bounds.clone()).toString()); - formula = formula.and(inst.formulate(bounds, x, formula, true).not()); + formula = formula.and(inst.formulate(x, formula, true, bounds).not()); inst = new Instance(uni); inst.add(a, f.setOf("A1","A2")); @@ -546,10 +546,10 @@ public void testStaticSome() { // relations: {a=[[A1], [A2]], b=[[B1], [B2]], $$A2$$=[[A2]], $$B2$$=[[B2]], $$A0$$=[[A0]], $$A1$$=[[A1]], $$B0$$=[[B0]], $$B1$$=[[B1]]} - assertEquals("((a = ($$A1$$ + $$A2$$)) and (b = ($$B1$$ + $$B2$$)))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + assertEquals("((a = (A1 + A2)) and (b = (B1 + B2)))", + inst.formulate(x, formula, true, bounds.clone()).toString()); - formula = formula.and(inst.formulate(bounds, x, formula, true).not()); + formula = formula.and(inst.formulate(x, formula, true, bounds).not()); inst = new Instance(uni); inst.add(a, f.setOf("A1","A2")); @@ -561,8 +561,8 @@ public void testStaticSome() { // relations: {a=[[A1], [A2]], b=[[B2]], $$A1$$=[[A1]], $$A2$$=[[A2]], $$B1$$=[[B1]], $$B2$$=[[B2]], $$A0$$=[[A0]], $$B0$$=[[B0]]} - assertEquals("((a = ($$A1$$ + $$A2$$)) and (b = $$B2$$))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + assertEquals("((a = (A1 + A2)) and (b = B2))", + inst.formulate(x, formula, true, bounds.clone()).toString()); } @@ -616,7 +616,7 @@ public void testTmpSome() { assertEquals( "(some [A1: one univ, B2: one univ, A2: one univ, B0: one univ, A0: one univ, B1: one univ] | (((((((A1 + B2) + A2) + B0) + A0) + B1) = univ) and (((a = none) and after((a = ((A0 + A1) + A2)))) and always((((a = none) implies after(after((a = none)))) and ((a = ((A0 + A1) + A2)) implies after(after((a = ((A0 + A1) + A2))))))))))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + inst.formulate(x, formula, true, bounds.clone()).toString()); inst0 = new Instance(uni); inst0.add(a, f.setOf("A2")); @@ -635,7 +635,7 @@ public void testTmpSome() { assertEquals( "(some [A1: one univ, B2: one univ, A2: one univ, B0: one univ, A0: one univ, B1: one univ] | (((((((A1 + B2) + A2) + B0) + A0) + B1) = univ) and (((a = A2) and after((a = (A0 + A1)))) and always((((a = A2) implies after(after((a = A2)))) and ((a = (A0 + A1)) implies after(after((a = (A0 + A1))))))))))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + inst.formulate(x, formula, true, bounds.clone()).toString()); } @@ -691,7 +691,7 @@ public void testTmp2Some() { assertEquals( "(some [A1: one univ, B2: one univ, A2: one univ, B0: one univ, A0: one univ, B1: one univ] | (((((((A1 + B2) + A2) + B0) + A0) + B1) = univ) and ((((a = (A1 + A2)) and (b = none)) and after((((a = none) and (b = B2)) and after(((a = A0) and (b = B2)))))) and after(always(((((a = none) and (b = B2)) implies after(after(((a = none) and (b = B2))))) and (((a = A0) and (b = B2)) implies after(after(((a = A0) and (b = B2)))))))))))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + inst.formulate(x, formula, true, bounds.clone()).toString()); inst0 = new Instance(uni); inst0.add(a, f.setOf("A1","A2")); @@ -715,7 +715,7 @@ public void testTmp2Some() { assertEquals( "(some [A1: one univ, B2: one univ, A2: one univ, B0: one univ, A0: one univ, B1: one univ] | (((((((A1 + B2) + A2) + B0) + A0) + B1) = univ) and ((((a = (A1 + A2)) and (b = none)) and after((((a = none) and (b = B2)) and after(((a = A0) and (b = B2)))))) and after(always(((((a = none) and (b = B2)) implies after(after(((a = none) and (b = B2))))) and (((a = A0) and (b = B2)) implies after(after(((a = A0) and (b = B2)))))))))))", - inst.formulate(bounds.clone(), x, formula, true).toString()); + inst.formulate(x, formula, true, bounds.clone()).toString()); } diff --git a/src/test/java/kodkod/test/pardinus/decomp/ExplorationQualityTests.java b/src/test/java/kodkod/test/pardinus/decomp/ExplorationQualityTests.java index bccf9ff6..777ad8cf 100644 --- a/src/test/java/kodkod/test/pardinus/decomp/ExplorationQualityTests.java +++ b/src/test/java/kodkod/test/pardinus/decomp/ExplorationQualityTests.java @@ -364,45 +364,33 @@ public void testSegIterationsNoChanges() { // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // beyond prefix length, must unroll sol = sols.nextS(2,5, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(7, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // prefix is already fixed up to 6 sol = sols.nextS(0,1, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(7, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // beyond the maximum trace length sol = sols.nextS(9,2, new HashSet()); diff --git a/src/test/java/kodkod/test/pardinus/decomp/TemporalSymmetryTests.java b/src/test/java/kodkod/test/pardinus/decomp/TemporalSymmetryTests.java index ae545b46..fff9fe9f 100644 --- a/src/test/java/kodkod/test/pardinus/decomp/TemporalSymmetryTests.java +++ b/src/test/java/kodkod/test/pardinus/decomp/TemporalSymmetryTests.java @@ -36,7 +36,6 @@ import kodkod.engine.config.DecomposedOptions.DMode; import kodkod.engine.config.AbstractReporter; import kodkod.engine.config.ExtendedOptions; -import kodkod.engine.config.SLF4JReporter; import kodkod.engine.config.Options; import kodkod.engine.config.Reporter; import kodkod.engine.decomp.DModel; diff --git a/src/test/java/kodkod/test/pardinus/temporal/ExplorationQualityTests.java b/src/test/java/kodkod/test/pardinus/temporal/ExplorationQualityTests.java index 91305a71..a2742660 100644 --- a/src/test/java/kodkod/test/pardinus/temporal/ExplorationQualityTests.java +++ b/src/test/java/kodkod/test/pardinus/temporal/ExplorationQualityTests.java @@ -23,8 +23,11 @@ package kodkod.test.pardinus.temporal; +import kodkod.ast.Expression; import kodkod.ast.Formula; import kodkod.ast.Relation; +import kodkod.ast.Variable; +import kodkod.engine.Evaluator; import kodkod.engine.Explorer; import kodkod.engine.PardinusSolver; import kodkod.engine.Solution; @@ -355,45 +358,33 @@ public void testSegIterationsNoChanges() { // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // just fixing, solution never changes sol = sols.nextS(2,2, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(4, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // beyond prefix length, must unroll sol = sols.nextS(2,5, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(7, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // prefix is already fixed up to 6 sol = sols.nextS(0,1, new HashSet()); - assertTrue(sol.sat()); + assertFalse(sol.sat()); assertTrue(sols.hasNext()); - assertEquals(7, ((TemporalInstance) sol.instance()).prefixLength()); - opt.reporter().debug(sol.instance().toString()); // beyond the maximum trace length sol = sols.nextS(9,2, new HashSet()); @@ -757,4 +748,149 @@ public void testConfigPath() { solver.free(); } + + @Test + public void testStateWiseSB() { + int n = 3; + + Relation file = Relation.unary_variable("F"); + Relation trash = Relation.unary_variable("T"); + + Object[] atoms = new Object[n]; + for (int i = 0; i < n; i ++) + atoms[i] = "A"+i; + + Universe uni = new Universe(atoms); + TupleFactory f = uni.factory(); + TupleSet as = f.range(f.tuple("A0"), f.tuple("A"+(n-1))); + + PardinusBounds bounds = new PardinusBounds(uni); + bounds.bound(file, as); + bounds.bound(trash, as); + + Formula type=trash.in(file).always(); + Formula init=trash.no(); + Variable vr=Variable.unary("f"); + Formula delete=((vr.in(trash).not()).and(trash.prime().eq(trash.union(vr)))).and(file.prime().eq(file)); + Formula retore=((vr.in(trash)).and(trash.prime().eq(trash.difference(vr)))).and(file.prime().eq(file)); + Formula x15=(delete.or(retore)).forSome(vr.oneOf(file)); + Formula empty=(trash.some().and(trash.prime().no())).and(file.prime().eq(file.difference(trash))); + Formula act=x15.or(empty); + Formula stutter = (file.prime().eq(file)).and(trash.prime().eq(trash)); + Formula step=act.or(stutter).always(); + Formula x55=file.eq(file); + Formula x56=trash.eq(trash); + Formula formula=Formula.and(type, init, step, x55, x56); + + + ExtendedOptions opt = new ExtendedOptions(); + +// opt.setReporter(new SLF4JReporter()); + opt.setRunTemporal(true); + opt.setRunUnbounded(false); + opt.setRunDecomposed(false); + opt.setMaxTraceLength(4); + opt.setSolver(SATFactory.MiniSat); + PardinusSolver solver = new PardinusSolver(opt); + + Set changes = new HashSet(); + changes.add(file); + changes.add(trash); + + Explorer sols = (Explorer) solver.solveAll(formula, bounds); + Solution sol = sols.next(); + sol = sols.nextS(0, 1, changes); + sol = sols.nextS(1, 1, changes); + sol = sols.nextS(1, 1, changes); + assertFalse("returned two isomorphic instance, bad statewise sbp", sol.sat()); + + solver.free(); + } + + @Test + public void testStateWiseSB2() { + int n = 2; + + Relation a = Relation.unary_variable("a"); + Relation b = Relation.unary_variable("b"); + + Object[] atoms = new Object[n]; + for (int i = 0; i < n; i ++) + atoms[i] = "A"+i; + + Universe uni = new Universe(atoms); + TupleFactory f = uni.factory(); + TupleSet as = f.range(f.tuple("A0"), f.tuple("A"+(n-1))); + + PardinusBounds bounds = new PardinusBounds(uni); + bounds.bound(a, as); + bounds.bound(b, as); + + Formula f1 = a.eq(a.prime()).not().always(); + Formula f2 = b.eq(b.prime()).not().always(); + Formula f3 = a.eq(Expression.UNIV); + Formula formula=Formula.and(f1, f2, f3); + + + ExtendedOptions opt = new ExtendedOptions(); + +// opt.setReporter(new SLF4JReporter()); + opt.setRunTemporal(true); + opt.setRunUnbounded(false); + opt.setRunDecomposed(false); + opt.setMaxTraceLength(2); + opt.setSolver(SATFactory.MiniSat); + PardinusSolver solver = new PardinusSolver(opt); + + Explorer sols = (Explorer) solver.solveAll(formula, bounds); + Solution sol = sols.next(); + while (sols.hasNext()) { + Evaluator eval = new Evaluator(sol.instance()); + assertFalse("symmetry not broken statewise", eval.evaluate(b).toString().equals("[[A0]]")); + sol = sols.nextP(); + } + + solver.free(); + } + + @Test + public void testConfigNoConfigs() { + int n = 2; + + Relation a = Relation.unary_variable("a"); + + Object[] atoms = new Object[n]; + for (int i = 0; i < n; i ++) + atoms[i] = "A"+i; + + Universe uni = new Universe(atoms); + TupleFactory f = uni.factory(); + TupleSet as = f.range(f.tuple("A0"), f.tuple("A"+(n-1))); + + PardinusBounds bounds = new PardinusBounds(uni); + bounds.bound(a, as); + + Formula formula = a.eq(a.prime()).not().always(); + + ExtendedOptions opt = new ExtendedOptions(); + +// opt.setReporter(new SLF4JReporter()); + opt.setRunTemporal(true); + opt.setRunUnbounded(false); + opt.setRunDecomposed(false); + opt.setMaxTraceLength(2); + opt.setSolver(SATFactory.MiniSat); + PardinusSolver solver = new PardinusSolver(opt); + + Explorer sols = (Explorer) solver.solveAll(formula, bounds); + int c = 0; + while (sols.hasNextC()) { + sols.nextC(); + c++; + } + + assertEquals("nothing to change, should not have iterated",1,c); + + solver.free(); + } } \ No newline at end of file diff --git a/src/test/java/kodkod/test/pardinus/temporal/InstanceExpansionTests.java b/src/test/java/kodkod/test/pardinus/temporal/InstanceExpansionTests.java index b48cd68e..17d9ca16 100644 --- a/src/test/java/kodkod/test/pardinus/temporal/InstanceExpansionTests.java +++ b/src/test/java/kodkod/test/pardinus/temporal/InstanceExpansionTests.java @@ -415,7 +415,7 @@ public void testSta2SAT() { PardinusSolver solver = new PardinusSolver(opt); Explorer solution = solver.solveAll(formula, bounds); - TemporalInstance inst = (TemporalInstance) solution.next().instance(); + TemporalInstance inst = (TemporalInstance) solution.nextC().instance(); Evaluator e1 = new Evaluator(inst); for (int i = 0; i < inst.prefixLength() + 3; i++) { Evaluator e2 = new Evaluator(inst.state(i)); diff --git a/src/test/java/kodkod/test/pardinus/temporal/TemporalUCoreMappingTest.java b/src/test/java/kodkod/test/pardinus/temporal/TemporalUCoreMappingTest.java index 6aebd490..3f93128c 100644 --- a/src/test/java/kodkod/test/pardinus/temporal/TemporalUCoreMappingTest.java +++ b/src/test/java/kodkod/test/pardinus/temporal/TemporalUCoreMappingTest.java @@ -111,7 +111,7 @@ public void testUnsatGran1() { assertFalse(hCore.contains(f10)); assertFalse(hCore.contains(f11)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @Test @@ -161,7 +161,7 @@ public void testUnsatGran2() { assertFalse(hCore.contains(f10)); assertFalse(hCore.contains(f11)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @Test @@ -211,7 +211,7 @@ public void testUnsatGran3() { assertFalse(hCore.contains(f10)); assertTrue(hCore.contains(f11)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @Test @@ -264,7 +264,7 @@ public void testUnsatGran1Skolem() { assertFalse(hCore.contains(f11)); assertFalse(hCore.contains(f20)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @Test @@ -317,7 +317,7 @@ public void testUnsatGran2Skolem() { assertFalse(hCore.contains(f11)); assertTrue(hCore.contains(f20)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @@ -371,7 +371,7 @@ public void testUnsatGran3Skolem() { assertTrue(hCore.contains(f11)); assertTrue(hCore.contains(f20)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } @Test @@ -422,7 +422,7 @@ public void testUnsatGran1SkolemTrivial() { assertFalse(hCore.contains(f10)); assertFalse(hCore.contains(f11)); - System.out.println(hCore); + opt.reporter().debug(hCore.toString()); } }