diff --git a/prism/src/dv/dv.cc b/prism/src/dv/dv.cc index 54f31654..46136719 100644 --- a/prism/src/dv/dv.cc +++ b/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); } diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index c19e67ae..bb7af680 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/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; diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index af940f2c..04049d84 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/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; } } diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 4af392a3..47979eb2 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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() + "\""); diff --git a/prism/src/prism/StateProbsDV.java b/prism/src/prism/StateProbsDV.java index 8b9a9dfd..8bdbf861 100644 --- a/prism/src/prism/StateProbsDV.java +++ b/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); diff --git a/prism/src/prism/StateProbsMTBDD.java b/prism/src/prism/StateProbsMTBDD.java index b554bcdf..4bc119ba 100644 --- a/prism/src/prism/StateProbsMTBDD.java +++ b/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;