diff --git a/src/de/stups/probkodkod/Request.java b/src/de/stups/probkodkod/Request.java index 53ea99cc8523aa645e34e4390ce8251072d96f36..32f4bca4dedc95581790980cf9b81f6a0d9d9802 100644 --- a/src/de/stups/probkodkod/Request.java +++ b/src/de/stups/probkodkod/Request.java @@ -80,7 +80,8 @@ public final class Request { pto.openTerm(tupleType.isSingleton() ? "b" : "s"); pto.printAtom(relinfo.getId()); if (tupleType.isSingleton()) { - final Tuple tuple = tupleSet.iterator().next(); + final Tuple tuple = tupleSet.isEmpty() ? null + : tupleSet.iterator().next(); writeTuple(pto, tupleType, tupleSet, tuple); } else { pto.openList(); diff --git a/test/de/stups/probkodkod/KodkodTest.java b/test/de/stups/probkodkod/KodkodTest.java index 59048fc692c19c5800acddaaaab204007e024467..1fa5a353bb0d6c63f190776439ae4914d504bdd0 100644 --- a/test/de/stups/probkodkod/KodkodTest.java +++ b/test/de/stups/probkodkod/KodkodTest.java @@ -15,7 +15,7 @@ import de.stups.probkodkod.test.Result; import de.stups.probkodkod.test.ResultSetBuilder; public class KodkodTest extends InteractionTestBase { - // @Test + @Test public void testLoop() throws ParserException, LexerException, IOException, InterruptedException { String problem = load("loop.kodkod"); @@ -68,7 +68,7 @@ public class KodkodTest extends InteractionTestBase { checkSolutions(createExpResLoop(), loop2); } - // @Test + @Test public void testIntegers() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -76,7 +76,7 @@ public class KodkodTest extends InteractionTestBase { testAll("integers", b.toCollection()); } - // @Test + @Test public void testProjection() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -84,7 +84,7 @@ public class KodkodTest extends InteractionTestBase { testAll("projection", b.toCollection()); } - // @Test + @Test public void testFunctions() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -93,7 +93,7 @@ public class KodkodTest extends InteractionTestBase { testAll("functions", b.toCollection()); } - // @Test + @Test public void testIntegerCasts() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -101,7 +101,7 @@ public class KodkodTest extends InteractionTestBase { testAll("integercast", b.toCollection()); } - // @Test + @Test public void testIntegerVariable() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -109,7 +109,7 @@ public class KodkodTest extends InteractionTestBase { testAll("intvar", b.toCollection()); } - // @Test + @Test public void testIntegerRange() throws IOException, ParserException, LexerException, InterruptedException { ResultSetBuilder b = new ResultSetBuilder(); @@ -126,7 +126,7 @@ public class KodkodTest extends InteractionTestBase { testAll("negative", b.toCollection()); } - // @Test + @Test public void testEmptySetInRequest() throws IOException, ParserException, LexerException { final String problem = load("simpletwovars.kodkod"); @@ -145,4 +145,18 @@ public class KodkodTest extends InteractionTestBase { checkSolutions(b.toCollection(), sol); } + + @Test + public void testBug1() throws ParserException, LexerException, IOException { + final String problem = load("returnzero.kodkod"); + sendMessage(problem + "."); + + sendMessage("request returnzero 10 pos ()."); + List<SortedMap<String, Result>> sol = new LinkedList<SortedMap<String, Result>>(); + getSolutions(false, sol); + + ResultSetBuilder b = new ResultSetBuilder(); + b.single("x", t(0)).store(); + checkSolutions(b.toCollection(), sol); + } } diff --git a/test/de/stups/probkodkod/returnzero.kodkod b/test/de/stups/probkodkod/returnzero.kodkod new file mode 100644 index 0000000000000000000000000000000000000000..8437c86d322f020a23c970668f0d2679e9a738a9 --- /dev/null +++ b/test/de/stups/probkodkod/returnzero.kodkod @@ -0,0 +1,6 @@ +problem returnzero + ( (inttype(p2i 0 0)) ) + + ( (x singleton subset p2i) ) + + (equals(expr2int(relref x))(0))