From f85400152d0011544af734d437e5ddada6d5acfb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 3 Jun 2014 12:44:25 +0000 Subject: [PATCH] Re-factoring - push the creation of default filters during model checking into a utility method in ExpressionFilter. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8394 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 48 ++---------------- prism/src/param/ParamModelChecker.java | 46 ++--------------- prism/src/parser/ast/ExpressionFilter.java | 58 ++++++++++++++++++++++ prism/src/prism/StateModelChecker.java | 48 ++---------------- 4 files changed, 69 insertions(+), 131 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 74253eb0..7e419d18 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -259,7 +259,6 @@ public class StateModelChecker extends PrismComponent */ public Result check(Model model, Expression expr) throws PrismException { - ExpressionFilter exprFilter = null; long timer = 0; StateValues vals; String resultString; @@ -269,49 +268,10 @@ public class StateModelChecker extends PrismComponent // Remove any existing filter info currentFilter = null; - - // The final result of model checking will be a single value. If the expression to be checked does not - // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap - // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not - // return single values and have to be treated in this way. - if (!expr.returnsSingleValue()) { - // New filter depends on expression type and number of initial states. - // Boolean expressions... - if (expr.getType() instanceof TypeBool) { - // Result is true iff true for all initial states - exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init")); - } - // Non-Boolean (double or integer) expressions... - else { - // Result is for the initial state, if there is just one, - // or the range over all initial states, if multiple - if (model.getNumInitialStates() == 1) { - exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init")); - } else { - exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init")); - } - } - } - // Even, when the expression does already return a single value, if the the outermost operator - // of the expression is not a filter, we still need to wrap a new filter around it. - // e.g. 2*filter(...) or 1-P=?[...{...}] - // This because the final result of model checking is only stored when we process a filter. - else if (!(expr instanceof ExpressionFilter)) { - // We just pick the first value (they are all the same) - exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); - // We stop any additional explanation being displayed to avoid confusion. - exprFilter.setExplanationEnabled(false); - } - - // For any case where a new filter was created above... - if (exprFilter != null) { - // Make it invisible (not that it will be displayed) - exprFilter.setInvisible(true); - // Compute type of new filter expression (will be same as child) - exprFilter.typeCheck(); - // Store as expression to be model checked - 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) { diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index bda0ce85..413e524e 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -222,7 +222,6 @@ final public class ParamModelChecker extends PrismComponent model.getNumStates(), model.getFirstInitialState(), simplifyRegions, splitMethod); valueComputer = new ValueComputer(paramModel, regionFactory, precision, eliminationOrder, bisimType); - ExpressionFilter exprFilter = null; long timer = 0; // Remove labels from property, using combined label list (on a copy of the expression) @@ -233,48 +232,9 @@ final public class ParamModelChecker extends PrismComponent // Also evaluate/replace any constants //expr = (Expression) expr.replaceConstants(constantValues); - // The final result of model checking will be a single value. If the expression to be checked does not - // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap - // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not - // return single values and have to be treated in this way. - if (!expr.returnsSingleValue()) { - // New filter depends on expression type and number of initial states. - // Boolean expressions... - if (expr.getType() instanceof TypeBool) { - // Result is true iff true for all initial states - exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init")); - } - // Non-Boolean (double or integer) expressions... - else { - // Result is for the initial state, if there is just one, - // or the range over all initial states, if multiple - if (model.getNumInitialStates() == 1) { - exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init")); - } else { - exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init")); - } - } - } - // Even, when the expression does already return a single value, if the the outermost operator - // of the expression is not a filter, we still need to wrap a new filter around it. - // e.g. 2*filter(...) or 1-P=?[...{...}] - // This because the final result of model checking is only stored when we process a filter. - else if (!(expr instanceof ExpressionFilter)) { - // We just pick the first value (they are all the same) - exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); - // We stop any additional explanation being displayed to avoid confusion. - exprFilter.setExplanationEnabled(false); - } - - // For any case where a new filter was created above... - if (exprFilter != null) { - // Make it invisible (not that it will be displayed) - exprFilter.setInvisible(true); - // Compute type of new filter expression (will be same as child) - exprFilter.typeCheck(); - // Store as expression to be model checked - 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); // Do model checking and store result vector timer = System.currentTimeMillis(); diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 84f47263..bf37dfc4 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -27,6 +27,7 @@ package parser.ast; import parser.*; +import parser.type.TypeBool; import parser.visitor.*; import prism.PrismLangException; @@ -246,6 +247,63 @@ public class ExpressionFilter extends Expression return e; } + + /** + * Wrap a "default" ExpressionFilter around an Expression representing a property to be model checked, + * in order to pick out a single value (the final result of model checking) from a vector of values for all states. + * See the PRISM manual (or check the code below) to see the definition of the "default" filter. + * If the expression is already an ExpressionFilter (of the right kind), nothing is done. + * Note that we need to know whether the model has multiple initial states, because this affects the default filter. + * @param expr Expression to be model checked + * @param singleInit Does the model on which it is being checked have a single initial states? + */ + public static Expression addDefaultFilterIfNeeded(Expression expr, boolean singleInit) throws PrismLangException + { + ExpressionFilter exprFilter = null; + + // The final result of model checking will be a single value. If the expression to be checked does not + // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap + // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not + // return single values and have to be treated in this way. + if (!expr.returnsSingleValue()) { + // New filter depends on expression type and number of initial states. + // Boolean expressions... + if (expr.getType() instanceof TypeBool) { + // Result is true iff true for all initial states + exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init")); + } + // Non-Boolean (double or integer) expressions... + else { + // Result is for the initial state, if there is just one, + // or the range over all initial states, if multiple + if (singleInit) { + exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init")); + } else { + exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init")); + } + } + } + // Even, when the expression does already return a single value, if the the outermost operator + // of the expression is not a filter, we still need to wrap a new filter around it. + // e.g. 2*filter(...) or 1-P=?[...{...}] + // This because the final result of model checking is only stored when we process a filter. + else if (!(expr instanceof ExpressionFilter)) { + // We just pick the first value (they are all the same) + exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); + // We stop any additional explanation being displayed to avoid confusion. + exprFilter.setExplanationEnabled(false); + } + // Finalise filter (if created) and return + if (exprFilter != null) { + // Make it invisible (not that it will be displayed) + exprFilter.setInvisible(true); + // Compute type of new filter expression (will be same as child) + exprFilter.typeCheck(); + return exprFilter; + } else { + return expr; + } + } } // ------------------------------------------------------------------------------ diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 28e88094..97ab0754 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -167,7 +167,6 @@ public class StateModelChecker implements ModelChecker */ public Result check(Expression expr) throws PrismException { - ExpressionFilter exprFilter = null; long timer = 0; StateValues vals; String resultString; @@ -178,49 +177,10 @@ public class StateModelChecker implements ModelChecker // Remove any existing filter info currentFilter = null; - // The final result of model checking will be a single value. If the expression to be checked does not - // already yield a single value (e.g. because a filter has not been explicitly included), we need to wrap - // a new (invisible) filter around it. Note that some filters (e.g. print/argmin/argmax) also do not - // return single values and have to be treated in this way. - if (!expr.returnsSingleValue()) { - // New filter depends on expression type and number of initial states. - // Boolean expressions... - if (expr.getType() instanceof TypeBool) { - // Result is true iff true for all initial states - exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init")); - } - // Non-Boolean (double or integer) expressions... - else { - // Result is for the initial state, if there is just one, - // or the range over all initial states, if multiple - if (model.getNumStartStates() == 1) { - exprFilter = new ExpressionFilter("state", expr, new ExpressionLabel("init")); - } else { - exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init")); - } - } - } - // Even, when the expression does already return a single value, if the the outermost operator - // of the expression is not a filter, we still need to wrap a new filter around it. - // e.g. 2*filter(...) or 1-P=?[...{...}] - // This because the final result of model checking is only stored when we process a filter. - else if (!(expr instanceof ExpressionFilter)) { - // We just pick the first value (they are all the same) - exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); - // We stop any additional explanation being displayed to avoid confusion. - exprFilter.setExplanationEnabled(false); - } - - // For any case where a new filter was created above... - if (exprFilter != null) { - // Make it invisible (not that it will be displayed) - exprFilter.setInvisible(true); - // Compute type of new filter expression (will be same as child) - exprFilter.typeCheck(); - // Store as expression to be model checked - 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(); vals = checkExpression(expr);