From e7a97ed79508c9ec5195b9485983eb6a920f65e7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 27 Apr 2019 12:38:53 +0100 Subject: [PATCH] Change underlying mechanism for -exportvector (new "store" filter). This uses a new type of ExpressionFilter with op type "store", rather than setting a boolean flag on existing filter objects. Includes two test-cases showing examples where the old code failed. --- ...prism.props => exportvector.prism.1.props} | 0 .../vector/exportvector.prism.1.props.args | 1 + ...ops.txt => exportvector.prism.1.props.txt} | 0 .../export/vector/exportvector.prism.2.props | 2 ++ .../vector/exportvector.prism.2.props.args | 1 + .../vector/exportvector.prism.2.props.txt | 7 ++++ .../export/vector/exportvector.prism.3.props | 2 ++ .../vector/exportvector.prism.3.props.args | 1 + .../vector/exportvector.prism.3.props.txt | 7 ++++ .../vector/exportvector.prism.props.args | 1 - prism/src/explicit/StateModelChecker.java | 35 ++++++++++++------ prism/src/parser/ast/Expression.java | 6 ++++ prism/src/parser/ast/ExpressionFilter.java | 20 +++-------- prism/src/parser/visitor/TypeCheck.java | 2 ++ prism/src/prism/StateModelChecker.java | 36 +++++++++++++------ 15 files changed, 82 insertions(+), 39 deletions(-) rename prism-tests/functionality/export/vector/{exportvector.prism.props => exportvector.prism.1.props} (100%) create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.1.props.args rename prism-tests/functionality/export/vector/{exportvector.prism.props.txt => exportvector.prism.1.props.txt} (100%) create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.2.props create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.2.props.args create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.2.props.txt create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.3.props create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.3.props.args create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.3.props.txt delete mode 100644 prism-tests/functionality/export/vector/exportvector.prism.props.args diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props b/prism-tests/functionality/export/vector/exportvector.prism.1.props similarity index 100% rename from prism-tests/functionality/export/vector/exportvector.prism.props rename to prism-tests/functionality/export/vector/exportvector.prism.1.props diff --git a/prism-tests/functionality/export/vector/exportvector.prism.1.props.args b/prism-tests/functionality/export/vector/exportvector.prism.1.props.args new file mode 100644 index 00000000..553f08f8 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.1.props.args @@ -0,0 +1 @@ +-const N=3 -exportvector exportvector.prism.1.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props.txt b/prism-tests/functionality/export/vector/exportvector.prism.1.props.txt similarity index 100% rename from prism-tests/functionality/export/vector/exportvector.prism.props.txt rename to prism-tests/functionality/export/vector/exportvector.prism.1.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism.2.props b/prism-tests/functionality/export/vector/exportvector.prism.2.props new file mode 100644 index 00000000..0eb4d49b --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.2.props @@ -0,0 +1,2 @@ +// RESULT: 0.0 +P=? [ X X X x=0 ]; diff --git a/prism-tests/functionality/export/vector/exportvector.prism.2.props.args b/prism-tests/functionality/export/vector/exportvector.prism.2.props.args new file mode 100644 index 00000000..3a72dfd4 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.2.props.args @@ -0,0 +1 @@ +-const N=3 -exportvector exportvector.prism.2.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism.2.props.txt b/prism-tests/functionality/export/vector/exportvector.prism.2.props.txt new file mode 100644 index 00000000..d3482892 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.2.props.txt @@ -0,0 +1,7 @@ +0.125 +0.0 +0.375 +0.0 +0.375 +0.0 +0.125 diff --git a/prism-tests/functionality/export/vector/exportvector.prism.3.props b/prism-tests/functionality/export/vector/exportvector.prism.3.props new file mode 100644 index 00000000..5a8bd078 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.3.props @@ -0,0 +1,2 @@ +// RESULT: 1.0 +filter(sum, P=? [ X X X x=0 ]); diff --git a/prism-tests/functionality/export/vector/exportvector.prism.3.props.args b/prism-tests/functionality/export/vector/exportvector.prism.3.props.args new file mode 100644 index 00000000..84ecab1d --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.3.props.args @@ -0,0 +1 @@ +-const N=3 -exportvector exportvector.prism.3.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism.3.props.txt b/prism-tests/functionality/export/vector/exportvector.prism.3.props.txt new file mode 100644 index 00000000..28dc9381 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.3.props.txt @@ -0,0 +1,7 @@ +1.0 +1.0 +1.0 +1.0 +1.0 +1.0 +1.0 diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props.args b/prism-tests/functionality/export/vector/exportvector.prism.props.args deleted file mode 100644 index f1342bd8..00000000 --- a/prism-tests/functionality/export/vector/exportvector.prism.props.args +++ /dev/null @@ -1 +0,0 @@ --const N=3 -exportvector exportvector.prism.props.txt diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index dbc727f4..d68fd167 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -535,14 +535,16 @@ public class StateModelChecker extends PrismComponent // Remove any existing filter info currentFilter = null; - // Wrap a filter round the property, if needed - // (in order to extract the final result of model checking) - ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1); - // And if we need to store a copy of the results vector, make a note of this + // If we need to store a copy of the results vector, add a "store" filter to represent this if (storeVector) { - exprFilter.setStoreVector(true); + ExpressionFilter exprFilter = new ExpressionFilter("store", expr); + exprFilter.setInvisible(true); + exprFilter.typeCheck(); + expr = exprFilter; } - expr = exprFilter; + // Wrap a filter round the property, if needed + // (in order to extract the final result of model checking) + expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumInitialStates() == 1); // If required, do bisimulation minimisation if (doBisim) { @@ -970,7 +972,7 @@ public class StateModelChecker extends PrismComponent boolean filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).isInitLabel()); boolean filterInitSingle = filterInit & model.getNumInitialStates() == 1; // Print out number of states satisfying filter - if (!filterInit) { + if (!filterInit && !expr.isInvisible()) { mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); } // Possibly optimise filter @@ -1028,6 +1030,14 @@ public class StateModelChecker extends PrismComponent // Set vals to null to stop it being cleared below vals = null; break; + case STORE: + // Not much to do here - will be handled below when we store in the Result object + // Result vector is unchanged; like PRINT/PRINTALL, don't store a single value (in resObj) + // Also, don't bother with explanation string + resVals = vals; + // Set vals to null to stop it being cleared below + vals = null; + break; case MIN: // Compute min // Store as object/vector @@ -1223,10 +1233,13 @@ public class StateModelChecker extends PrismComponent } else { result.setExplanation(null); } - // Store vector if requested (and if not, clear it) - if (storeVector) { - result.setVector(vals); - } else if (vals != null) { + // Store vector if requested + if (op == FilterOperator.STORE) { + result.setVector(resVals); + } + // Clear old vector if present + // (and if the vector was not stored previously) + if (vals != null && !(Expression.isFilter(expr.getOperand(), FilterOperator.STORE))) { vals.clear(); } diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index c72df81e..22e4010b 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -29,6 +29,7 @@ package parser.ast; import jltl2ba.SimpleLTL; import param.BigRational; import parser.*; +import parser.ast.ExpressionFilter.FilterOperator; import parser.visitor.*; import prism.ModelType; import prism.PrismException; @@ -780,6 +781,11 @@ public abstract class Expression extends ASTElement && ExpressionBinaryOp.isRelOp(((ExpressionBinaryOp) expr).getOperator()); } + public static boolean isFilter(Expression expr, ExpressionFilter.FilterOperator opType) + { + return expr instanceof ExpressionFilter && ((ExpressionFilter) expr).getOperatorType() == opType; + } + /** * Test if an expression is a function of type {@code nameCode}. */ diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 32ccb3b2..8040a47e 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -66,7 +66,9 @@ public class ExpressionFilter extends Expression /** Print all (including zero) values to the log */ PRINTALL ("printall"), /** Value for the single filter state (if there is more than one, this is an error) */ - STATE ("state"); + STATE ("state"), + /** Store the results vector (used internally) */ + STORE ("store"); public final String keyword; FilterOperator(final String keyword) { this.keyword = keyword; @@ -89,8 +91,6 @@ public class ExpressionFilter extends Expression private boolean invisible = false; // Whether or not an explanation should be displayed when model checking private boolean explanationEnabled = true; - // Do we need to store a copy of the results vector when model checking this? - private boolean storeVector = false; // whether this is a filter over parameters private boolean param = false; @@ -152,11 +152,6 @@ public class ExpressionFilter extends Expression this.explanationEnabled = explanationEnabled; } - public void setStoreVector(boolean storeVector) - { - this.storeVector = storeVector; - } - public void setParam() { param = true; @@ -194,11 +189,6 @@ public class ExpressionFilter extends Expression return explanationEnabled; } - public boolean getStoreVector() - { - return storeVector; - } - public boolean isParam() { return param; @@ -241,6 +231,7 @@ public class ExpressionFilter extends Expression else if (opType == FilterOperator.PRINTALL) return false; else if (opType == FilterOperator.ARGMIN) return false; else if (opType == FilterOperator.ARGMAX) return false; + else if (opType == FilterOperator.STORE) return false; else if (param) return false; else return true; } @@ -293,7 +284,6 @@ public class ExpressionFilter extends Expression result = prime * result + ((opType == null) ? 0 : opType.hashCode()); result = prime * result + ((operand == null) ? 0 : operand.hashCode()); result = prime * result + (param ? 1231 : 1237); - result = prime * result + (storeVector ? 1231 : 1237); return result; } @@ -330,8 +320,6 @@ public class ExpressionFilter extends Expression return false; if (param != other.param) return false; - if (storeVector != other.storeVector) - return false; return true; } diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 4b8eb9d3..8d43fd9e 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -642,6 +642,7 @@ public class TypeCheck extends ASTTraverse case FIRST: case PRINT: case PRINTALL: + case STORE: if (t instanceof TypeVoid) { throw new PrismLangException("Type error: Void/complex arguments not allowed as operand for filter of type \"" + e.getOperatorName() + "\"", e.getOperand()); @@ -662,6 +663,7 @@ public class TypeCheck extends ASTTraverse case FIRST: case PRINT: case PRINTALL: + case STORE: case STATE: e.setType(t); break; diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index b8b1e577..b19bee4f 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -220,14 +220,16 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Remove any existing filter info currentFilter = null; - // Wrap a filter round the property, if needed - // (in order to extract the final result of model checking) - ExpressionFilter exprFilter = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1); - // And if we need to store a copy of the results vector, make a note of this + // If we need to store a copy of the results vector, add a "store" filter to represent this if (storeVector) { - exprFilter.setStoreVector(true); + ExpressionFilter exprFilter = new ExpressionFilter("store", expr); + exprFilter.setInvisible(true); + exprFilter.typeCheck(); + expr = exprFilter; } - expr = exprFilter; + // Wrap a filter round the property, if needed + // (in order to extract the final result of model checking) + expr = ExpressionFilter.addDefaultFilterIfNeeded(expr, model.getNumStartStates() == 1); // Do model checking and store result vector timer = System.currentTimeMillis(); @@ -1177,8 +1179,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker } // Print out number of states satisfying filter - if (!filterInit) + if (!filterInit && !expr.isInvisible()) { mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString()); + } // Compute result according to filter type op = expr.getOperatorType(); @@ -1218,6 +1221,14 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Set vals to null to stop it being cleared below vals = null; break; + case STORE: + // Not much to do here - will be handled below when we store in the Result object + // Result vector is unchanged; like PRINT/PRINTALL, don't store a single value (in resObj) + // Also, don't bother with explanation string + resVals = vals; + // Set vals to null to stop it being cleared below + vals = null; + break; case MIN: // Compute min d = vals.minOverBDD(ddFilter); @@ -1468,10 +1479,13 @@ public class StateModelChecker extends PrismComponent implements ModelChecker } else { result.setExplanation(null); } - // Store vector if requested (and if not, clear it) - if (storeVector) { - result.setVector(vals); - } else if (vals != null) { + // Store vector if requested + if (op == FilterOperator.STORE) { + result.setVector(resVals); + } + // Clear old vector if present + // (and if the vector was not stored previously) + if (vals != null && !(Expression.isFilter(expr.getOperand(), FilterOperator.STORE))) { vals.clear(); } // Other derefs