[recurse] When recursion is used a number of pre-checks (ints/strings…

…) fail.
AlloyTools · Nov 17, 2017 · 7abd6cb · 7abd6cb
1 parent ab3b00c
commit 7abd6cb
Showing 1 changed file with 31 additions and 0 deletions.
diff --git a/...ytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole/AlloyModelsTest.java b/...ytools.alloy.application/src/test/java/edu/mit/csail/sdg/alloy4whole/AlloyModelsTest.java
@@ -0,0 +1,31 @@
+package edu.mit.csail.sdg.alloy4whole;
+
+import org.junit.Test;
+
+import edu.mit.csail.sdg.alloy4.A4Reporter;
+import edu.mit.csail.sdg.ast.Command;
+import edu.mit.csail.sdg.ast.Module;
+import edu.mit.csail.sdg.parser.CompUtil;
+import edu.mit.csail.sdg.translator.A4Options;
+import edu.mit.csail.sdg.translator.A4Solution;
+import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
+
+public class AlloyModelsTest {
+
+	@Test
+	public void testRecursion() throws Exception {
+		String filename = "src/test/resources/test-recursion.als";
+		Module world = CompUtil.parseEverything_fromFile(A4Reporter.NOP, null, filename);
+
+		A4Options options = new A4Options();
+		for (Command command : world.getAllCommands()) {
+			A4Solution ans = TranslateAlloyToKodkod.execute_command(A4Reporter.NOP, world.getAllReachableSigs(),
+					command, options);
+			while (ans.satisfiable()) {
+				String hc = "Answer: " + ans.toString().hashCode();
+				ans = ans.next();
+			}
+			return;
+		}
+	}
+}