Merge branch 'master' into highprecision

nickbattle · Sep 11, 2023 · a69b7f7 · a69b7f7
2 parents a13927d + 9039438
commit a69b7f7
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 7 deletions.
diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -347,7 +347,8 @@ public void checkObligation(ProofObligation po, Results results)
 		{
 			resetErrors();	// Only flag fatal errors
 			RootContext ctxt = Interpreter.getInstance().getInitialContext();
-			List<INBindingSetter> bindings = null;
+			INExpression poexp = getINExpression(po);
+			List<INBindingSetter> bindings = getINBindList(poexp);;
 
 			if (!po.isCheckable)
 			{
@@ -359,18 +360,18 @@ else if (po.status == POStatus.TRIVIAL)
 				printf("PO #%d, TRIVIAL by %s\n", po.number, po.proof);
 				return;
 			}
-			else if (results.proved && results.counterexamples.isEmpty())
+			else if (results.proved &&
+					 results.counterexamples.isEmpty() &&
+					 !bindings.isEmpty())	// empty binds => simple forall over sets, so must execute
 			{
 				po.status = POStatus.PROVED;
-				printf("PO #%d, PROVED\n", po.number);
+				printf("PO #%d, PROVED %s\n", po.number, duration(results.duration));
 				return;
 			}
 
 			try
 			{
 				Map<String, ValueList> cexamples = results.counterexamples;
-				INExpression poexp = getINExpression(po);
-				bindings = getINBindList(poexp);
 
 				for (INBindingSetter mbind: bindings)
 				{
@@ -579,6 +580,12 @@ private void printFailPath(List<INBindingSetter> bindings)
 		println("");
 	}
 
+	private String duration(long time)
+	{
+		double duration = (double)(time)/1000;
+		return "in " + duration + "s";
+	}
+
 	private String duration(long before, long after)
 	{
 		double duration = (double)(after - before)/1000;

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/MapSetOfCompatibleObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/MapSetOfCompatibleObligation.java
@@ -41,7 +41,9 @@ private void append(StringBuilder sb, String exp)
 		String m1 = getVar("m");
 		String m2 = getVar("m");
 
-		sb.append("forall " + m1 + ", " + m2 + " in set ");
+		sb.append("forall " + m1 + " in set ");
+		sb.append(exp);
+		sb.append(", " + m2 + " in set ");
 		sb.append(exp);
 
 		String d1 = getVar("d");

diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java
@@ -123,7 +123,7 @@ protected void tearDown() throws Exception
 		"exists finmap1:map nat to (int) & forall a:int, b in set {1, 2, 3} & (a < 10) => exists findex2 in set dom finmap1 & finmap1(findex2) = (a + b)\n",
 		"(forall a:map (int) to (int), b:map (int) to (int) &\n  forall ldom1 in set dom a, rdom2 in set dom b & ldom1 = rdom2 => a(ldom1) = b(rdom2))\n",
 		"(forall x:int &\n  forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}, {x |-> 4}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4))\n",
-		"forall m1, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
+		"forall m1 in set {{1 |-> 2}, {2 |-> 3}}, m2 in set {{1 |-> 2}, {2 |-> 3}} & forall d3 in set dom m1, d4 in set dom m2 & d3 = d4 => m1(d3) = m2(d4)\n",
 		"(forall n:nat &\n  is_(measure_recursive(n), nat))\n",
 		"(forall n:nat &\n  (not (n = 1) =>\n    (n - 1) >= 0))\n",
 		"(forall n:nat &\n  (not (n = 1) =>\n    measure_recursive(n) > measure_recursive((n - 1))))\n",