From 43d52add46acf5aafb2d0ef41e02abf1aadea9b2 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 12:39:09 +0000 Subject: [PATCH] Model checkers (symbolic/explicit) cache some filter info for optimisations/checks during model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4678 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 22 ++++++- prism/src/prism/Filter.java | 74 +++++++++++++++++++++++ prism/src/prism/StateModelChecker.java | 20 +++++- 3 files changed, 111 insertions(+), 5 deletions(-) create mode 100644 prism/src/prism/Filter.java diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 8866a84c..40724ee2 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -58,6 +58,7 @@ import parser.ast.Property; import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypeInt; +import prism.Filter; import prism.PrismException; import prism.PrismLangException; import prism.PrismLog; @@ -85,6 +86,9 @@ public class StateModelChecker // Constants (extracted from model/properties) protected Values constantValues; + // The filter to be applied to the current property + protected Filter currentFilter; + // The result of model checking will be stored here protected Result result; @@ -189,6 +193,9 @@ public class StateModelChecker // Create storage for result result = new Result(); + // 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 @@ -583,8 +590,6 @@ public class StateModelChecker String resultExpl = null; Object resObj = null; - // Check operand recursively - vals = checkExpression(model, expr.getOperand()); // Translate filter filter = expr.getFilter(); // Create default filter (true) if none given @@ -602,12 +607,23 @@ public class StateModelChecker // Remember whether filter is for the initial state and, if so, whether there's just one filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); filterInitSingle = filterInit & model.getNumInitialStates() == 1; + + // For some types of filter, store info that may be used to optimise model checking + op = expr.getOperatorType(); + if (op == FilterOperator.STATE) { + currentFilter = new Filter(Filter.FilterOperator.STATE, bsFilter.nextSetBit(0)); + } else { + currentFilter = null; + } + + // Check operand recursively + vals = checkExpression(model, expr.getOperand()); + // Print out number of states satisfying filter if (!filterInit) mainLog.println("\nStates satisfying filter " + filter + ": " + bsFilter.cardinality()); // Compute result according to filter type - op = expr.getOperatorType(); switch (op) { case PRINT: // Format of print-out depends on type diff --git a/prism/src/prism/Filter.java b/prism/src/prism/Filter.java new file mode 100644 index 00000000..4c2bce2c --- /dev/null +++ b/prism/src/prism/Filter.java @@ -0,0 +1,74 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM 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 2 of the License, or +// (at your option) any later version. +// +// PRISM 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 PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package prism; + +/** + * Class to store basic information about how results of model checking will be filtered. + */ +public class Filter +{ + // Enums for types of filter + public enum FilterOperator { + STATE; + }; + // Filter operator + private FilterOperator op = null; + // State of interest + private int stateIndex = -1; + + // Constructors + + public Filter(FilterOperator op, int stateIndex) + { + setOperator(op); + setStateIndex(stateIndex); + } + + // Getters/setters + + public FilterOperator getOperator() + { + return op; + } + + public int getStateIndex() + { + return stateIndex; + } + + public void setOperator(FilterOperator op) + { + this.op = op; + } + + public void setStateIndex(int stateIndex) + { + this.stateIndex = stateIndex; + } +} + +// ------------------------------------------------------------------------------ diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 5930d6a5..cd67107f 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -62,6 +62,9 @@ public class StateModelChecker implements ModelChecker protected JDDVars allDDColVars; protected JDDVars[] varDDRowVars; + // The filter to be applied to the current property + protected Filter currentFilter; + // The result of model checking will be stored here protected Result result; @@ -147,6 +150,9 @@ public class StateModelChecker implements ModelChecker // Create storage for result result = new Result(); + // 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 @@ -1002,8 +1008,6 @@ public class StateModelChecker implements ModelChecker String resultExpl = null; Object resObj = null; - // Check operand recursively - vals = checkExpression(expr.getOperand()); // Translate filter filter = expr.getFilter(); // Create default filter (true) if none given @@ -1022,6 +1026,18 @@ public class StateModelChecker implements ModelChecker // Remember whether filter is for the initial state and, if so, whether there's just one filterInit = (filter instanceof ExpressionLabel && ((ExpressionLabel) filter).getName().equals("init")); filterInitSingle = filterInit & model.getNumStartStates() == 1; + + // For some types of filter, store info that may be used to optimise model checking + op = expr.getOperatorType(); + if (op == FilterOperator.STATE) { + currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars)); + } else { + currentFilter = null; + } + + // Check operand recursively + vals = checkExpression(expr.getOperand()); + // Print out number of states satisfying filter if (!filterInit) mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString());