From 894476fa9fb6a59dbf249c99b417fbd3c828303d Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sat, 21 Oct 2023 18:24:29 +0100 Subject: [PATCH 1/4] Small DBGP tweak --- dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StderrRedirector.java | 2 ++ dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StdoutRedirector.java | 2 ++ 2 files changed, 4 insertions(+) diff --git a/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StderrRedirector.java b/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StderrRedirector.java index e695ea8b2..cde4ff82e 100644 --- a/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StderrRedirector.java +++ b/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StderrRedirector.java @@ -45,10 +45,12 @@ public void print(String line) { case DISABLE: out.print(line); + out.flush(); break; case COPY: out.print(line); + out.flush(); dbgp.stderr(line); break; diff --git a/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StdoutRedirector.java b/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StdoutRedirector.java index 7ce477006..b3fb58802 100644 --- a/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StdoutRedirector.java +++ b/dbgp/src/main/java/com/fujitsu/vdmj/dbgp/StdoutRedirector.java @@ -45,10 +45,12 @@ public void print(String line) { case DISABLE: out.print(line); + out.flush(); break; case COPY: out.print(line); + out.flush(); dbgp.stdout(line); break; From 326a70c7798dbca33847685f6c477c864752b298 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 22 Oct 2023 19:05:31 +0100 Subject: [PATCH 2/4] Use provedBy string --- .../src/main/java/quickcheck/QuickCheck.java | 18 ++++++++++-------- .../strategies/FiniteQCStrategy.java | 8 ++++---- .../quickcheck/strategies/FixedQCStrategy.java | 2 +- .../strategies/RandomQCStrategy.java | 2 +- .../java/quickcheck/strategies/Results.java | 8 ++++---- .../strategies/SearchQCStrategy.java | 2 +- .../strategies/TrivialQCStrategy.java | 2 +- .../quickcheck/example/ExampleQCStrategy.java | 2 +- 8 files changed, 23 insertions(+), 21 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 363e942ff..ce27f239e 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -317,11 +317,10 @@ public List getINBindList(INExpression inexp) public Results getValues(ProofObligation po) { Map union = new HashMap(); - boolean proved = false; if (!po.isCheckable) { - return new Results(false, union, 0); + return new Results(null, union, 0); } INExpression exp = getINExpression(po); @@ -335,8 +334,8 @@ public Results getValues(ProofObligation po) for (QCStrategy strategy: strategies) { - Results presults = strategy.getValues(po, exp, binds, ictxt); - Map cexamples = presults.counterexamples; + Results sresults = strategy.getValues(po, exp, binds, ictxt); + Map cexamples = sresults.counterexamples; for (String bind: cexamples.keySet()) { @@ -350,7 +349,10 @@ public Results getValues(ProofObligation po) } } - proved |= presults.proved; + if (sresults.provedBy != null) // No need to go further + { + return new Results(sresults.provedBy, cexamples, System.currentTimeMillis() - before); + } } for (INBindingSetter bind: binds) @@ -365,7 +367,7 @@ public Results getValues(ProofObligation po) } } - return new Results(proved, union, System.currentTimeMillis() - before); + return new Results(null, union, System.currentTimeMillis() - before); } public void checkObligation(ProofObligation po, Results results) @@ -386,7 +388,7 @@ else if (po.status == POStatus.TRIVIAL) printf("PO #%d, TRIVIAL by %s\n", po.number, po.proof); return; } - else if (results.proved && + else if (results.provedBy != null && results.counterexamples.isEmpty() && !bindings.isEmpty()) // empty binds => simple forall over sets, so must execute { @@ -480,7 +482,7 @@ else if (result instanceof BooleanValue) } else { - outcome = (results.proved) ? POStatus.PROVED : POStatus.MAYBE; + outcome = (results.provedBy != null) ? POStatus.PROVED : POStatus.MAYBE; } printf("PO #%d, %s %s\n", po.number, outcome.toString().toUpperCase(), duration(before, after)); diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 943c36104..adb346b18 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -140,16 +140,16 @@ public Results getValues(ProofObligation po, INExpression exp, List expansionLimit) { - return new Results(false, result, 0); // Too big + return new Results(null, result, 0); // Too big } } catch (InternalException e) // Infinite { - return new Results(false, result, 0); + return new Results(null, result, 0); } catch (ArithmeticException e) // Overflow probably { - return new Results(false, result, 0); + return new Results(null, result, 0); } } @@ -162,7 +162,7 @@ public Results getValues(ProofObligation po, INExpression exp, List counterexamples; public final long duration; // time to generate counterexamples, in millisecs - public Results(boolean proved, Map counterexamples, long duration) + public Results(String proved, Map counterexamples, long duration) { - this.proved = proved; + this.provedBy = proved; this.counterexamples = counterexamples; this.duration = duration; } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index 24edea90b..24d7b4dd5 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -134,7 +134,7 @@ public Results getValues(ProofObligation po, INExpression exp, List()); } - return new Results(proved, new HashMap(), System.currentTimeMillis() - before); + return new Results(proved ? getName() : null, new HashMap(), System.currentTimeMillis() - before); } @Override diff --git a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index 46b63f111..8f6747849 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -104,7 +104,7 @@ public Results getValues(ProofObligation po, INExpression exp, List Date: Sun, 22 Oct 2023 20:34:44 +0100 Subject: [PATCH 3/4] Add provedBy to ProofObligation and print --- .../quickcheck/src/main/java/quickcheck/QuickCheck.java | 9 ++++----- .../main/java/com/fujitsu/vdmj/pog/ProofObligation.java | 7 +++++++ .../java/com/fujitsu/vdmj/pog/ProofObligationList.java | 6 ++++++ 3 files changed, 17 insertions(+), 5 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index ce27f239e..344859b38 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -388,12 +388,11 @@ else if (po.status == POStatus.TRIVIAL) printf("PO #%d, TRIVIAL by %s\n", po.number, po.proof); return; } - else if (results.provedBy != null && - results.counterexamples.isEmpty() && - !bindings.isEmpty()) // empty binds => simple forall over sets, so must execute + else if (results.provedBy != null) { po.setStatus(POStatus.PROVED); - printf("PO #%d, PROVED %s\n", po.number, duration(results.duration)); + po.setProvedBy(results.provedBy); + printf("PO #%d, PROVED by %s strategy %s\n", po.number, results.provedBy, duration(results.duration)); return; } @@ -482,7 +481,7 @@ else if (result instanceof BooleanValue) } else { - outcome = (results.provedBy != null) ? POStatus.PROVED : POStatus.MAYBE; + outcome = POStatus.MAYBE; } printf("PO #%d, %s %s\n", po.number, outcome.toString().toUpperCase(), duration(before, after)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 12cfe1d0a..d18e397d2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -47,6 +47,7 @@ abstract public class ProofObligation implements Comparable public POAnnotationList annotations; public Context counterexample; public String countermessage; + public String provedBy; private int var = 1; private TCExpression checkedExpression = null; @@ -64,6 +65,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.annotations = ctxt.getAnnotations(); this.counterexample = new Context(location, "Counterexample", null); this.countermessage = null; + this.provedBy = null; if (!isCheckable) { @@ -83,6 +85,11 @@ public void setStatus(POStatus status) this.status = status; } + public void setProvedBy(String provedBy) + { + this.provedBy = provedBy; + } + public void setCounterexample(Context path) { counterexample.clear(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index b0d064ce0..0bfc468c8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -92,6 +92,12 @@ public String toString() sep = ", "; } } + + if (po.provedBy != null) + { + sb.append("proved by "); + sb.append(po.provedBy); + } sb.append(")\n"); From d8e6a19f663d5af07b1ce15e14fd20d68f437131 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 22 Oct 2023 20:43:51 +0100 Subject: [PATCH 4/4] Don't display prover strategy --- .../main/java/com/fujitsu/vdmj/pog/ProofObligationList.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 0bfc468c8..189a26e7e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -93,12 +93,6 @@ public String toString() } } - if (po.provedBy != null) - { - sb.append("proved by "); - sb.append(po.provedBy); - } - sb.append(")\n"); if (po.countermessage != null)