From e04c9f038b0340fce7093de405b79a56f8a46713 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 15 Dec 2023 17:41:50 +0000 Subject: [PATCH 1/9] Expose some implicit operation POs to QC --- .../POImplicitOperationDefinition.java | 16 ++++++++-------- .../visitors/PORemoveIgnoresVisitor.java | 9 +++++++++ .../com/fujitsu/vdmj/pog/POImpliesContext.java | 4 ++-- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index 09cc8172c..dc70220ed 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -137,8 +137,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); TCNameList pids = new TCNameList(); boolean matchNeeded = false; - - ctxt.push(new PONoCheckContext()); for (POPatternListTypePair pltp: parameterPatterns) { @@ -178,9 +176,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.addAll(postdef.getProofObligations(ctxt, env)); } + ctxt.push(new PONoCheckContext()); obligations.add(new OperationPostConditionObligation(this, ctxt)); + ctxt.pop(); } + ctxt.push(new PONoCheckContext()); + if (body != null) { obligations.addAll(body.getProofObligations(ctxt, env)); @@ -195,8 +197,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - obligations.add( - new SubTypeObligation(this, actualResult, ctxt)); + obligations.add(new SubTypeObligation(this, actualResult, ctxt)); } } else @@ -204,14 +205,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (postcondition != null) { ctxt.push(new POOperationDefinitionContext(this, false, state)); - obligations.add( - new SatisfiabilityObligation(this, state, ctxt)); + obligations.add(new SatisfiabilityObligation(this, state, ctxt)); ctxt.pop(); } } - - ctxt.pop(); + ctxt.pop(); + if (annotations != null) annotations.poAfter(this, obligations, ctxt); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java index 35e09fc72..e17a40a2c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java @@ -94,6 +94,15 @@ public POPattern caseExpressionPattern(POExpressionPattern node, Object arg) @Override public POPattern caseIdentifierPattern(POIdentifierPattern node, Object arg) { + // If we encounter any "old" state names, like "Sigma~", we rename to + // "oldSigma" to allow POs to work as simple expressions. + + if (node.name.isOld()) + { + TCNameToken oldName = new TCNameToken(node.location, node.location.module, "old" + node.name.getName()); + return new POIdentifierPattern(oldName); + } + return node; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java index 355355ec6..08185acb7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java @@ -39,12 +39,12 @@ public POImpliesContext(POExpression precondition) public POImpliesContext(POExplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.predef.getParamPatternList(), def.precondition); } public POImpliesContext(POImplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.predef.getParamPatternList(), def.precondition); } @Override From c6c57b23bbb5fc7a839dafe31314b6e8f1b3ef02 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Fri, 15 Dec 2023 21:32:42 +0000 Subject: [PATCH 2/9] Add ExecutionResultFinder --- .../visitors/ExecutionResultFinder.java | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java diff --git a/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java b/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java new file mode 100644 index 000000000..d4575605a --- /dev/null +++ b/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java @@ -0,0 +1,56 @@ +/******************************************************************************* + * + * Copyright (c) 2023 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package quickcheck.visitors; + +import java.util.List; +import java.util.Vector; + +import com.fujitsu.vdmj.in.expressions.INExpression; +import com.fujitsu.vdmj.in.expressions.visitors.INLeafExpressionVisitor; +import com.fujitsu.vdmj.pog.POStatus; + +/** + * Search an expression tree after a QuickCheck execution to decide the outcome. + * This is affected by the forall/exists subexpressions, whether they have + * type bindings set and whether the binds have all type values. + */ +public class ExecutionResultFinder extends INLeafExpressionVisitor, Object> +{ + public ExecutionResultFinder(boolean allNodes) + { + super(allNodes); + } + + @Override + protected List newCollection() + { + return new Vector(); + } + + @Override + public List caseExpression(INExpression node, Object arg) + { + return newCollection(); + } +} From b70fe0a9a5a5f244ef66f4db47a3974dc9fd4b67 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Fri, 15 Dec 2023 23:08:57 +0000 Subject: [PATCH 3/9] Tidy binding interface for QC --- .../in/expressions/INExistsExpression.java | 78 ++------------ .../in/expressions/INForAllExpression.java | 60 +++-------- .../vdmj/in/patterns/INBindingSetter.java | 3 +- .../vdmj/in/patterns/INMultipleBindList.java | 102 ++++++++++++++++++ .../vdmj/in/patterns/INMultipleTypeBind.java | 11 +- .../fujitsu/vdmj/in/patterns/INTypeBind.java | 11 +- 6 files changed, 146 insertions(+), 119 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java index 6dce6eb75..2ad3c9cd6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java @@ -24,7 +24,6 @@ package com.fujitsu.vdmj.in.expressions; import com.fujitsu.vdmj.in.expressions.visitors.INExpressionVisitor; -import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.in.patterns.INMultipleBind; import com.fujitsu.vdmj.in.patterns.INMultipleBindList; import com.fujitsu.vdmj.in.patterns.INPattern; @@ -44,6 +43,9 @@ public class INExistsExpression extends INExpression private static final long serialVersionUID = 1L; public final INMultipleBindList bindList; public final INExpression predicate; + + /** True if the execution did not have all bind values on exit */ + public boolean maybe = false; public INExistsExpression(LexLocation location, INMultipleBindList bindList, INExpression predicate) { @@ -63,7 +65,7 @@ public Value eval(Context ctxt) { breakpoint.check(location, ctxt); long start = System.currentTimeMillis(); - long timeout = getTimeout(); + long timeout = bindList.getTimeout(); try { @@ -88,7 +90,8 @@ public Value eval(Context ctxt) { if (System.currentTimeMillis() - start > timeout) { - setCounterexample(null, true); + bindList.setCounterexample(null, true); + maybe = !bindList.hasAllValues(); return new BooleanValue(true); } } @@ -109,7 +112,6 @@ public Value eval(Context ctxt) { if (!v.equals(nvp.value)) { - setWitness(evalContext); matches = false; break; // This quantifier set does not match } @@ -120,7 +122,8 @@ public Value eval(Context ctxt) { if (matches && predicate.eval(evalContext).boolValue(ctxt)) { - setWitness(evalContext); + bindList.setWitness(evalContext); + maybe = !bindList.hasAllValues(); return new BooleanValue(true); } } @@ -135,71 +138,10 @@ public Value eval(Context ctxt) abort(e); } + maybe = !bindList.hasAllValues(); return new BooleanValue(false); } - - /** - * This is used by the QuickCheck plugin to limit PO execution times. - */ - private long getTimeout() - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - long timeout = setter.getTimeout(); - - if (timeout > 0) - { - return timeout; - } - } - } - - return 0; - } - - /** - * This is used by the QuickCheck plugin to report which values failed. - */ - private void setCounterexample(Context ctxt, boolean didTimeout) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setCounterexample(ctxt, didTimeout); - break; // Just one will do - see QC printFailPath - } - } - } - } - - /** - * This is used by the QuickCheck plugin to report which values succeeded. - */ - private void setWitness(Context ctxt) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setWitness(ctxt); - break; // Just one will do - see QC printFailPath - } - } - } - } - + @Override public R apply(INExpressionVisitor visitor, S arg) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java index d3a0b6236..c29346bec 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java @@ -25,7 +25,6 @@ package com.fujitsu.vdmj.in.expressions; import com.fujitsu.vdmj.in.expressions.visitors.INExpressionVisitor; -import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.in.patterns.INMultipleBind; import com.fujitsu.vdmj.in.patterns.INMultipleBindList; import com.fujitsu.vdmj.in.patterns.INPattern; @@ -48,6 +47,9 @@ public class INForAllExpression extends INExpression public final INMultipleBindList bindList; public final INExpression predicate; + /** True if the execution did not have all bind values on exit */ + public boolean maybe = false; + public INForAllExpression(LexLocation location, INMultipleBindList bindList, INExpression predicate) { super(location); @@ -66,7 +68,7 @@ public Value eval(Context ctxt) { breakpoint.check(location, ctxt); long start = System.currentTimeMillis(); - long timeout = getTimeout(); + long timeout = bindList.getTimeout(); try { @@ -91,7 +93,8 @@ public Value eval(Context ctxt) { if (System.currentTimeMillis() - start > timeout) { - setCounterexample(null, true); + bindList.setCounterexample(null, true); + maybe = !bindList.hasAllValues(); return new BooleanValue(true); } } @@ -122,13 +125,15 @@ public Value eval(Context ctxt) { if (matches && !predicate.eval(evalContext).boolValue(ctxt)) { - setCounterexample(evalContext, false); + bindList.setCounterexample(evalContext, false); + maybe = !bindList.hasAllValues(); return new BooleanValue(false); } } catch (ContextException e) { - setCounterexample(evalContext, false); + bindList.setCounterexample(evalContext, false); + maybe = !bindList.hasAllValues(); throw e; } catch (ValueException e) @@ -142,51 +147,10 @@ public Value eval(Context ctxt) return abort(e); } + maybe = !bindList.hasAllValues(); return new BooleanValue(true); } - - /** - * This is used by the QuickCheck plugin to limit PO execution times. - */ - private long getTimeout() - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - long timeout = setter.getTimeout(); - - if (timeout > 0) - { - return timeout; - } - } - } - - return 0; - } - - /** - * This is used by the QuickCheck plugin to report which values failed. - */ - private void setCounterexample(Context ctxt, boolean didTimeout) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setCounterexample(ctxt, didTimeout); - break; // Just one will do - see QC printFailPath - } - } - } - } - + @Override public R apply(INExpressionVisitor visitor, S arg) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java index 6adbc0b02..22cccff52 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java @@ -30,8 +30,9 @@ public interface INBindingSetter { - public void setBindValues(ValueList values, long timeout); + public void setBindValues(ValueList values, long timeout, boolean hasAllValues); public ValueList getBindValues(); + public boolean hasAllValues(); public long getTimeout(); public boolean didTimeout(); public TCType getType(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java index 09b4207ca..3525c7657 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java @@ -25,6 +25,7 @@ package com.fujitsu.vdmj.in.patterns; import com.fujitsu.vdmj.in.INMappedList; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.tc.patterns.TCMultipleBind; import com.fujitsu.vdmj.tc.patterns.TCMultipleBindList; @@ -41,4 +42,105 @@ public INMultipleBindList(TCMultipleBindList from) throws Exception { super(from); } + + /** + * QuickCheck has set some type binds? + */ + public boolean isInstrumented() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) + { + return true; + } + } + } + + return false; + } + + /** + * This is used by the QuickCheck plugin to limit PO execution times. + */ + public long getTimeout() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + long timeout = setter.getTimeout(); + + if (timeout > 0) + { + return timeout; + } + } + } + + return 0; + } + + /** + * This is used by the QuickCheck plugin to report which values failed. + */ + public void setCounterexample(Context ctxt, boolean didTimeout) + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) // One we care about (set QC values for) + { + setter.setCounterexample(ctxt, didTimeout); + break; // Just one will do - see QC printFailPath + } + } + } + } + + /** + * This is used by the QuickCheck plugin to report which values succeeded. + */ + public void setWitness(Context ctxt) + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) // One we care about (set QC values for) + { + setter.setWitness(ctxt); + break; // Just one will do - see QC printFailPath + } + } + } + } + + public boolean hasAllValues() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (!setter.hasAllValues()) + { + return false; // One hasn't + } + } + } + + return true; // All have + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java index 614a37676..3f5d96248 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java @@ -47,6 +47,7 @@ public class INMultipleTypeBind extends INMultipleBind implements INBindingSette private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; + private boolean bindAllValues = false; private long bindTimeout = 0; private boolean didTimeout = false; @@ -64,13 +65,14 @@ public String toString() } @Override - public void setBindValues(ValueList values, long timeout) + public void setBindValues(ValueList values, long timeout, boolean hasAllValues) { if (values == null) { bindValues = null; bindOverride = false; bindTimeout = 0; + bindAllValues = true; // NOTE: because execution usually does } else { @@ -78,6 +80,7 @@ public void setBindValues(ValueList values, long timeout) bindValues.addAll(values); bindOverride = true; bindTimeout = timeout; + bindAllValues = hasAllValues; } didTimeout = false; @@ -102,6 +105,12 @@ public boolean didTimeout() { return didTimeout; } + + @Override + public boolean hasAllValues() + { + return bindAllValues; + } @Override public void setCounterexample(Context ctxt, boolean didTimeout) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java index b21243a0c..6c2d4f710 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java @@ -47,6 +47,7 @@ public class INTypeBind extends INBind implements INBindingSetter private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; + private boolean bindAllValues = false; private long bindTimeout = 0; private boolean didTimeout = false; @@ -58,13 +59,14 @@ public INTypeBind(INPattern pattern, TCType type) } @Override - public void setBindValues(ValueList values, long timeout) + public void setBindValues(ValueList values, long timeout, boolean hasAllValues) { if (values == null) { bindValues = null; bindOverride = false; bindTimeout = 0; + bindAllValues = true; // NOTE: because execution usually does } else { @@ -72,6 +74,7 @@ public void setBindValues(ValueList values, long timeout) bindValues.addAll(values); bindOverride = true; bindTimeout = timeout; + bindAllValues = hasAllValues; } didTimeout = false; @@ -96,6 +99,12 @@ public boolean didTimeout() { return didTimeout; } + + @Override + public boolean hasAllValues() + { + return bindAllValues; + } @Override public TCType getType() From 4ceb9079ae43cc44a6324734c9322e62b2fc9d83 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Fri, 15 Dec 2023 23:09:21 +0000 Subject: [PATCH 4/9] Draft ExecutionResultFinder --- .../src/main/java/quickcheck/QuickCheck.java | 4 +- .../visitors/ExecutionResultFinder.java | 41 +++++++++++++++++++ 2 files changed, 43 insertions(+), 2 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 91833dc5e..35534a4e9 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -399,7 +399,7 @@ else if (results.provedBy != null) if (values != null) { verbose("PO #%d, setting %s, %d values\n", po.number, mbind.toString(), values.size()); - mbind.setBindValues(values, timeout); + mbind.setBindValues(values, timeout, results.hasAllValues); } else { @@ -615,7 +615,7 @@ else if (po.isExistential()) // Principal exp is "exists..." { for (INBindingSetter mbind: bindings) { - mbind.setBindValues(null, 0); // Clears everything + mbind.setBindValues(null, 0, false); // Clears everything } } } diff --git a/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java b/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java index d4575605a..73ea49458 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java +++ b/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java @@ -26,7 +26,9 @@ import java.util.List; import java.util.Vector; +import com.fujitsu.vdmj.in.expressions.INExistsExpression; import com.fujitsu.vdmj.in.expressions.INExpression; +import com.fujitsu.vdmj.in.expressions.INForAllExpression; import com.fujitsu.vdmj.in.expressions.visitors.INLeafExpressionVisitor; import com.fujitsu.vdmj.pog.POStatus; @@ -47,10 +49,49 @@ protected List newCollection() { return new Vector(); } + + private List result(POStatus status) + { + List one = newCollection(); + one.add(status); + return one; + } @Override public List caseExpression(INExpression node, Object arg) { return newCollection(); } + + @Override + public List caseForAllExpression(INForAllExpression node, Object arg) + { + if (node.bindList.isInstrumented()) + { + List inner = node.predicate.apply(this, arg); + POStatus subexp = !inner.isEmpty() ? inner.get(0) : POStatus.UNPROVED; + + // if (!node.maybe) // forall had everything + { + return result(POStatus.MAYBE); + } + } + else + { + return super.caseForAllExpression(node, arg); + } + } + + @Override + public List caseExistsExpression(INExistsExpression node, Object arg) + { + if (node.bindList.isInstrumented()) + { + return result(POStatus.MAYBE); + } + else + { + return super.caseExistsExpression(node, arg); + } + } } From c6b11140c4c8312d1f1e771a85fd0ed741f46c28 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 16 Dec 2023 10:24:00 +0000 Subject: [PATCH 5/9] Change QC to use MaybeFinder --- .../src/main/java/quickcheck/QuickCheck.java | 18 ++++++ ...tionResultFinder.java => MaybeFinder.java} | 59 ++++++++----------- 2 files changed, 43 insertions(+), 34 deletions(-) rename quickcheck/src/main/java/quickcheck/visitors/{ExecutionResultFinder.java => MaybeFinder.java} (59%) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 35534a4e9..dd8c529d7 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -73,6 +73,7 @@ import quickcheck.strategies.QCStrategy; import quickcheck.strategies.StrategyResults; import quickcheck.visitors.FixedRangeCreator; +import quickcheck.visitors.MaybeFinder; import quickcheck.visitors.TypeBindFinder; public class QuickCheck @@ -428,6 +429,7 @@ else if (results.provedBy != null) Value execResult = new BooleanValue(false); ContextException execException = null; boolean execCompleted = false; + boolean hasMaybe = false; long before = System.currentTimeMillis(); try @@ -442,6 +444,10 @@ else if (results.provedBy != null) { ictxt.next(); execResult = poexp.eval(ictxt); + + MaybeFinder finder = new MaybeFinder(); + poexp.apply(finder, null); + hasMaybe = finder.hasMaybe(); } while (ictxt.hasNext() && execResult.boolValue(ctxt)); @@ -502,6 +508,10 @@ else if (execResult instanceof BooleanValue) { outcome = POStatus.TIMEOUT; } + else if (hasMaybe) + { + outcome = POStatus.MAYBE; + } else if (po.isExistential()) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. @@ -540,6 +550,14 @@ else if (results.hasAllValues && execCompleted) po.setMessage(null); po.setWitness(null); } + else if (hasMaybe) + { + infof(POStatus.MAYBE, "PO #%d, MAYBE %s\n", po.number, duration(before, after)); + po.setStatus(POStatus.MAYBE); + po.setCounterexample(null); + po.setMessage(null); + po.setWitness(null); + } else if (po.isExistential()) // Principal exp is "exists..." { if (results.hasAllValues) diff --git a/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java b/quickcheck/src/main/java/quickcheck/visitors/MaybeFinder.java similarity index 59% rename from quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java rename to quickcheck/src/main/java/quickcheck/visitors/MaybeFinder.java index 73ea49458..c72ae5549 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/ExecutionResultFinder.java +++ b/quickcheck/src/main/java/quickcheck/visitors/MaybeFinder.java @@ -30,68 +30,59 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.expressions.INForAllExpression; import com.fujitsu.vdmj.in.expressions.visitors.INLeafExpressionVisitor; -import com.fujitsu.vdmj.pog.POStatus; /** * Search an expression tree after a QuickCheck execution to decide the outcome. * This is affected by the forall/exists subexpressions, whether they have * type bindings set and whether the binds have all type values. */ -public class ExecutionResultFinder extends INLeafExpressionVisitor, Object> +public class MaybeFinder extends INLeafExpressionVisitor, Object> { - public ExecutionResultFinder(boolean allNodes) + private int maybeCount = 0; + + public MaybeFinder() + { + super(false); + } + + public boolean hasMaybe() { - super(allNodes); + return maybeCount > 0; } @Override - protected List newCollection() + protected List newCollection() { - return new Vector(); + return new Vector(); } - private List result(POStatus status) - { - List one = newCollection(); - one.add(status); - return one; - } - @Override - public List caseExpression(INExpression node, Object arg) + public List caseExpression(INExpression node, Object arg) { return newCollection(); } @Override - public List caseForAllExpression(INForAllExpression node, Object arg) + public List caseForAllExpression(INForAllExpression node, Object arg) { - if (node.bindList.isInstrumented()) - { - List inner = node.predicate.apply(this, arg); - POStatus subexp = !inner.isEmpty() ? inner.get(0) : POStatus.UNPROVED; - - // if (!node.maybe) // forall had everything - { - return result(POStatus.MAYBE); - } - } - else + if (node.maybe) { - return super.caseForAllExpression(node, arg); + maybeCount++; + node.maybe = false; } + + return super.caseForAllExpression(node, arg); } @Override - public List caseExistsExpression(INExistsExpression node, Object arg) + public List caseExistsExpression(INExistsExpression node, Object arg) { - if (node.bindList.isInstrumented()) - { - return result(POStatus.MAYBE); - } - else + if (node.maybe) { - return super.caseExistsExpression(node, arg); + maybeCount++; + node.maybe = false; } + + return super.caseExistsExpression(node, arg); } } From d4745f2fbb3259b775be2e3998c63c968e70cc9a Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 16 Dec 2023 10:24:26 +0000 Subject: [PATCH 6/9] Tweak use of maybe in forall/exists execution --- .../com/fujitsu/vdmj/in/expressions/INExistsExpression.java | 2 +- .../com/fujitsu/vdmj/in/expressions/INForAllExpression.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java index 2ad3c9cd6..e69c224d4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java @@ -91,7 +91,7 @@ public Value eval(Context ctxt) if (System.currentTimeMillis() - start > timeout) { bindList.setCounterexample(null, true); - maybe = !bindList.hasAllValues(); + maybe = true; return new BooleanValue(true); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java index c29346bec..c63d6da21 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java @@ -94,7 +94,7 @@ public Value eval(Context ctxt) if (System.currentTimeMillis() - start > timeout) { bindList.setCounterexample(null, true); - maybe = !bindList.hasAllValues(); + maybe = true; return new BooleanValue(true); } } From 326b6cdb110377f77238165a31cd559eadc2d748 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 16 Dec 2023 11:34:53 +0000 Subject: [PATCH 7/9] Clean up isExistential in QC --- .../strategies/SearchQCStrategy.java | 2 +- .../in/expressions/INExistsExpression.java | 2 +- .../POImplicitOperationDefinition.java | 7 ++-- .../com/fujitsu/vdmj/pog/POContextStack.java | 38 ------------------- .../java/com/fujitsu/vdmj/pog/POType.java | 31 +++++---------- .../com/fujitsu/vdmj/pog/ProofObligation.java | 4 +- 6 files changed, 17 insertions(+), 67 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index a4eb814b0..054965c7e 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -90,7 +90,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List Date: Sat, 16 Dec 2023 11:35:14 +0000 Subject: [PATCH 8/9] Correction to op satisfiability obligation --- .../main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java | 1 + 1 file changed, 1 insertion(+) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java index ff83f4b83..a2d33d76e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java @@ -93,6 +93,7 @@ public SatisfiabilityObligation(POImplicitOperationDefinition op, separator = ""; appendResult(sb, op.result); appendStatePatterns(sb, stateDefinition, false, true); + appendStatePatterns(sb, stateDefinition, true, true); sb.append(" & "); } From fa491ce3c929333efe40558b20023ee76daafc6f Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 16 Dec 2023 12:12:37 +0000 Subject: [PATCH 9/9] Correction to operation definition context --- .../com/fujitsu/vdmj/pog/POOperationDefinitionContext.java | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java index f2a0246be..e4ae1891c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java @@ -61,7 +61,7 @@ public String getContext() { StringBuilder sb = new StringBuilder(); - if (!deftype.parameters.isEmpty()) + if (!deftype.parameters.isEmpty() || stateDefinition != null) { sb.append("forall "); String sep = ""; @@ -78,6 +78,7 @@ public String getContext() if (stateDefinition != null) { + sb.append(sep); appendStatePatterns(sb); } @@ -103,13 +104,13 @@ private void appendStatePatterns(StringBuilder sb) else if (stateDefinition instanceof POStateDefinition) { POStateDefinition def = (POStateDefinition)stateDefinition; - sb.append(", oldstate:"); + sb.append("oldstate:"); sb.append(def.name.getName()); } else { POClassDefinition def = (POClassDefinition)stateDefinition; - sb.append(", oldself:"); + sb.append("oldself:"); sb.append(def.name.getName()); } }