Fixes and additions for new filters.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1663 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/dv/dv.cc

@@ -225,8 +225,12 @@ void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, DdN
 
 EXPORT double get_first_from_bdd(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd)
 {
-	// should never be called with an empty filter - we trap this case and return -1
-	if (filter == Cudd_ReadZero(ddman)) return -1;
+	// This shouldn't really be called with an empty filter.
+	// But we check for this anyway and return NaN.
+	// This is unfortunately indistinguishable from the case
+	// where the vector does actually contain NaN. Ho hum.
+	if (filter == Cudd_ReadZero(ddman)) return NAN;
+	// Recurse...
 	else return get_first_from_bdd_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
 }
 

prism/src/parser/ast/ExpressionFilter.java

@@ -34,7 +34,7 @@ public class ExpressionFilter extends Expression
 {
 	// Enums for  types of filter
 	public enum FilterOperator {
-		MIN, MAX, COUNT, PRINT;
+		MIN, MAX, COUNT, SUM, AVG, FIRST, PRINT;
 	};
 
 	// Operator used in filter
@@ -77,6 +77,12 @@ public class ExpressionFilter extends Expression
 			opType = FilterOperator.MAX;
 		else if (opName.equals("count"))
 			opType = FilterOperator.COUNT;
+		else if (opName.equals("sum"))
+			opType = FilterOperator.SUM;
+		else if (opName.equals("avg"))
+			opType = FilterOperator.AVG;
+		else if (opName.equals("first"))
+			opType = FilterOperator.FIRST;
 		else if (opName.equals("print"))
 			opType = FilterOperator.PRINT;
 		else opType = null;

prism/src/parser/visitor/TypeCheck.java

@@ -522,13 +522,15 @@ public class TypeCheck extends ASTTraverse
 
 		// Check filter is ok
 		if (e.getFilter() != null && !(e.getFilter().getType() instanceof TypeBool)) {
-			throw new PrismLangException("Type error: First argument of filter is not a Boolean", e.getFilter());
+			throw new PrismLangException("Type error: Second argument of filter is not a Boolean", e.getFilter());
 		}
 
 		// Check type of operands is ok
 		switch (e.getOperatorType()) {
 		case MIN:
 		case MAX:
+		case SUM:
+		case AVG:
 			if (t instanceof TypeBool) {
 				throw new PrismLangException(
 						"Type error: Boolean argument not allowed as operand for filter of type \""
@@ -541,6 +543,7 @@ public class TypeCheck extends ASTTraverse
 						+ "\" must be Boolean", e.getOperand());
 			}
 			break;
+		case FIRST:
 		case PRINT:
 			// Anything goes
 			break;
@@ -552,13 +555,16 @@ public class TypeCheck extends ASTTraverse
 		switch (e.getOperatorType()) {
 		case MIN:
 		case MAX:
+		case SUM:
+		case FIRST:
+		case PRINT:
 			e.setType(t);
 			break;
 		case COUNT:
 			e.setType(TypeInt.getInstance());
 			break;
-		case PRINT:
-			e.setType(t);
+		case AVG:
+			e.setType(TypeDouble.getInstance());
 			break;
 		}
 	}

prism/src/prism/StateModelChecker.java

@@ -1227,6 +1227,7 @@ public class StateModelChecker implements ModelChecker
 		Expression filter;
 		StateProbs vals = null, res = null;
 		JDDNode ddFilter;
+		boolean empty = false;
 		double d = 0.0;
 
 		// Check operand recursively
@@ -1237,9 +1238,12 @@ public class StateModelChecker implements ModelChecker
 			filter = Expression.True();
 		ddFilter = checkExpressionDD(filter);
 		// Check if filter state set is empty
+		// (display warning and optimise/catch below)
 		if (ddFilter.equals(JDD.ZERO)) {
+			empty = true;
 			mainLog.println("\nWarning: Filter " + filter + " satisfies no states");
 		}
+		
 		// Compute result according to filter type
 		switch (expr.getOperatorType()) {
 		case PRINT:
@@ -1248,20 +1252,44 @@ public class StateModelChecker implements ModelChecker
 			res = vals;
 			break;
 		case MIN:
-			d = vals.minOverBDD(ddFilter);
+			d = empty ? Double.POSITIVE_INFINITY : vals.minOverBDD(ddFilter);
 			mainLog.println("\nFilter: minimum value for states satisfying " + filter + ": " + d);
 			res = new StateProbsMTBDD(JDD.Constant(d), model);
 			break;
 		case MAX:
-			d = vals.maxOverBDD(ddFilter);
+			d = empty ? Double.NEGATIVE_INFINITY : vals.maxOverBDD(ddFilter);
 			mainLog.println("\nFilter: maximum value for states satisfying " + filter + ": " + d);
 			res = new StateProbsMTBDD(JDD.Constant(d), model);
 			break;
 		case COUNT:
-			d = vals.getNNZ();
+			if (empty)
+				d = 0;
+			else {
+				vals.filter(ddFilter);
+				d = vals.getNNZ();
+			}
 			mainLog.println("\nFilter: count of states satisfying " + filter + ": " + (int)d);
 			res = new StateProbsMTBDD(JDD.Constant(d), model);
 			break;
+		case SUM:
+			d = empty ? 0 : vals.sumOverBDD(ddFilter);
+			mainLog.println("\nFilter: sum over states satisfying " + filter + ": " + (int)d);
+			res = new StateProbsMTBDD(JDD.Constant(d), model);
+			break;
+		case AVG:
+			if (empty)
+				throw new PrismException("Can't take an average over an empty filter");
+			d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n());
+			mainLog.println("\nFilter: average over states satisfying " + filter + ": " + d);
+			res = new StateProbsMTBDD(JDD.Constant(d), model);
+			break;
+		case FIRST:
+			if (empty)
+				throw new PrismException("Can't select the first value from an empty filter");
+			d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n());
+			mainLog.println("\nFilter: value for first state satisfying " + filter + ": " + d);
+			res = new StateProbsMTBDD(JDD.Constant(d), model);
+			break;
 		default:
 			JDD.Deref(ddFilter);
 			throw new PrismException("Unrecognised filter type \"" + expr.getOperatorName() + "\"");

prism/src/prism/StateProbsDV.java

@@ -223,29 +223,33 @@ public class StateProbsDV implements StateProbs
 		return "" + getNNZ();
 	}
 	
-	// get value of first element in BDD filter
-	
+	/**
+	 * Get the value of first vector element that is in the (BDD) filter.
+	 */
 	public double firstFromBDD(JDDNode filter)
 	{
 		return probs.firstFromBDD(filter, vars, odd);
 	}
 	
-	// get min value over BDD filter
-	
+	/**
+	 * Get the minimum value of those that are in the (BDD) filter.
+	 */
 	public double minOverBDD(JDDNode filter)
 	{
 		return probs.minOverBDD(filter, vars, odd);
 	}
 	
-	// get max value over BDD filter
-	
+	/**
+	 * Get the minimum value of those that are in the (BDD) filter.
+	 */
 	public double maxOverBDD(JDDNode filter)
 	{
 		return probs.maxOverBDD(filter, vars, odd);
 	}
 	
-	// sum elements of vector according to a bdd (used for csl steady state operator)
-	
+	/**
+	 * Get the sum of those elements that are in the (BDD) filter.
+	 */
 	public double sumOverBDD(JDDNode filter)
 	{
 		return probs.sumOverBDD(filter, vars, odd);

prism/src/prism/StateProbsMTBDD.java

@@ -241,8 +241,11 @@ public class StateProbsMTBDD implements StateProbs
 		return "" + getNNZ();
 	}
 	
-	// get value of first element in BDD filter
+	// Filter operations
 	
+	/**
+	 * Get the value of first vector element that is in the (BDD) filter.
+	 */
 	public double firstFromBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -253,9 +256,12 @@ public class StateProbsMTBDD implements StateProbs
 		JDD.Ref(reach);
 		tmp = JDD.And(filter, reach);
 		
-		// should never be called with empty filter, but trap and return -1
-		if (tmp.equals(JDD.ZERO)) return -1;
-		
+		// This shouldn't really be called with an empty filter.
+		// But we check for this anyway and return NaN.
+		// This is unfortunately indistinguishable from the case
+		// where the vector does actually contain NaN. Ho hum.
+		if (tmp.equals(JDD.ZERO)) return Double.NaN;
+				
 		// remove all but first element of filter
 		tmp = JDD.RestrictToFirst(tmp, vars);
 		
@@ -271,8 +277,9 @@ public class StateProbsMTBDD implements StateProbs
 		return d;
 	}
 	
-	// get min value over BDD filter
-	
+	/**
+	 * Get the minimum value of those that are in the (BDD) filter.
+	 */
 	public double minOverBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -308,7 +315,7 @@ public class StateProbsMTBDD implements StateProbs
 		JDD.Ref(reach);
 		tmp = JDD.And(filter, reach);
 		
-		// max of an empty set is +infinity
+		// max of an empty set is -infinity
 		if (tmp.equals(JDD.ZERO)) return Double.NEGATIVE_INFINITY;
 		
 		// set non-reach states to infinity
@@ -321,8 +328,9 @@ public class StateProbsMTBDD implements StateProbs
 		return d;
 	}
 	
-	// sum elements of vector according to a bdd (used for csl steady state operator)
-	
+	/**
+	 * Get the sum of those elements that are in the (BDD) filter.
+	 */
 	public double sumOverBDD(JDDNode filter)
 	{
 		JDDNode tmp;