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-tests/functionality/export/vector/exportvector.prism.1.props.args

@@ -0,0 +1 @@
+-const N=3 -exportvector exportvector.prism.1.props.txt

prism-tests/functionality/export/vector/exportvector.prism.2.props

@@ -0,0 +1,2 @@
+// RESULT: 0.0
+P=? [ X X X x=0 ];

prism-tests/functionality/export/vector/exportvector.prism.2.props.args

@@ -0,0 +1 @@
+-const N=3 -exportvector exportvector.prism.2.props.txt

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

prism-tests/functionality/export/vector/exportvector.prism.3.props

@@ -0,0 +1,2 @@
+// RESULT: 1.0
+filter(sum, P=? [ X X X x=0 ]);

prism-tests/functionality/export/vector/exportvector.prism.3.props.args

@@ -0,0 +1 @@
+-const N=3 -exportvector exportvector.prism.3.props.txt

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

prism-tests/functionality/export/vector/exportvector.prism.props.args

@@ -1 +0,0 @@
--const N=3 -exportvector exportvector.prism.props.txt

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;
+		}
+		// 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();
 		}
 

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}.
 	 */

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;
 	}
 	

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;

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;
+		}
+		// 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