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

@@ -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

prism/src/prism/Filter.java

@@ -0,0 +1,74 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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;
+	}
+}
+
+// ------------------------------------------------------------------------------

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());