From 248981743c835e1fd63d65de911dbd7931d0827a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 14 Nov 2010 22:00:58 +0000 Subject: [PATCH] Better handling of filters, including ranges returned for multiple initial states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2240 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ExpressionFilter.java | 12 + prism/src/parser/type/TypeArray.java | 7 +- prism/src/parser/type/TypeInterval.java | 54 +++ prism/src/parser/visitor/TypeCheck.java | 4 +- prism/src/prism/Interval.java | 61 +++ prism/src/prism/StateModelChecker.java | 420 ++++++++++++--------- 6 files changed, 369 insertions(+), 189 deletions(-) create mode 100644 prism/src/parser/type/TypeInterval.java create mode 100644 prism/src/prism/Interval.java diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 7515fc29..73e94eca 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -51,6 +51,8 @@ public class ExpressionFilter extends Expression // by toString(). This is used to add filters to P/R/S operators that // were created with old-style filter syntax. private boolean invisible = false; + // Whether or not an explanation should be displayed when model checking + private boolean explanationEnabled = true; // Constructors @@ -113,6 +115,11 @@ public class ExpressionFilter extends Expression this.invisible = invisible; } + public void setExplanationEnabled(boolean explanationEnabled) + { + this.explanationEnabled = explanationEnabled; + } + // Get methods public FilterOperator getOperatorType() @@ -140,6 +147,11 @@ public class ExpressionFilter extends Expression return invisible; } + public boolean getExplanationEnabled() + { + return explanationEnabled; + } + // Methods required for Expression: /** diff --git a/prism/src/parser/type/TypeArray.java b/prism/src/parser/type/TypeArray.java index 4d8b128b..a5bcefd1 100644 --- a/prism/src/parser/type/TypeArray.java +++ b/prism/src/parser/type/TypeArray.java @@ -13,11 +13,6 @@ public class TypeArray extends Type private Type subType; - private TypeArray() - { - this.subType = null; - } - public TypeArray(Type subType) { this.subType = subType; @@ -51,7 +46,7 @@ public class TypeArray extends Type public static TypeArray getInstance(Type subType) { - if (singletons.containsKey(subType)) + if (!singletons.containsKey(subType)) singletons.put(subType, new TypeArray(subType)); return singletons.get(subType); diff --git a/prism/src/parser/type/TypeInterval.java b/prism/src/parser/type/TypeInterval.java new file mode 100644 index 00000000..a0ee353a --- /dev/null +++ b/prism/src/parser/type/TypeInterval.java @@ -0,0 +1,54 @@ +package parser.type; + +import java.util.*; + +public class TypeInterval extends Type +{ + private static Map singletons; + + static + { + singletons = new HashMap(); + } + + private Type subType; + + public TypeInterval(Type subType) + { + this.subType = subType; + } + + public Type getSubType() + { + return subType; + } + + public void setSubType(Type subType) + { + this.subType = subType; + } + + public boolean equals(Object o) + { + if (o instanceof TypeInterval) + { + TypeInterval oi = (TypeInterval)o; + return (subType.equals(oi.getSubType())); + } + + return false; + } + + public String getTypeString() + { + return "interval of " + subType.getTypeString(); + } + + public static TypeInterval getInstance(Type subType) + { + if (!singletons.containsKey(subType)) + singletons.put(subType, new TypeInterval(subType)); + + return singletons.get(subType); + } +} diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 11dbba21..b78edbe2 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -589,10 +589,12 @@ public class TypeCheck extends ASTTraverse case MAX: case SUM: case FIRST: - case RANGE: case PRINT: e.setType(t); break; + case RANGE: + e.setType(TypeInterval.getInstance(t)); + break; case COUNT: e.setType(TypeInt.getInstance()); break; diff --git a/prism/src/prism/Interval.java b/prism/src/prism/Interval.java new file mode 100644 index 00000000..e86d0bd5 --- /dev/null +++ b/prism/src/prism/Interval.java @@ -0,0 +1,61 @@ +//============================================================================== +// +// 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; + +/** + * This class stores an interval of numerical values. + */ +public class Interval +{ + // Lower/upper value + public Object lower; + public Object upper; + + /** + * Construct an integer Interval. + */ + public Interval(Integer lower, Integer upper) + { + this.lower = lower; + this.upper = upper; + } + + /** + * Construct a double Interval. + */ + public Interval(Double lower, Double upper) + { + this.lower = lower; + this.upper = upper; + } + + @Override + public String toString() + { + return "[" + lower + "," + upper + "]"; + } +} diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 53e07083..383300bf 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -110,8 +110,7 @@ public class StateModelChecker implements ModelChecker * Additional constructor for creating stripped down StateModelChecker for * expression to MTBDD conversions. */ - public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, - Values constantValues) throws PrismException + public StateModelChecker(Prism prism, VarList varList, JDDVars allDDRowVars, JDDVars[] varDDRowVars, Values constantValues) throws PrismException { // Initialise this.prism = prism; @@ -123,8 +122,8 @@ public class StateModelChecker implements ModelChecker // Create dummy model reach = null; allDDRowVars.refAll(); - model = new ProbModel(JDD.Constant(0), JDD.Constant(0), new JDDNode[] {}, new JDDNode[] {}, null, allDDRowVars, - new JDDVars(), null, 0, null, null, null, 0, varList, varDDRowVars, null, constantValues); + model = new ProbModel(JDD.Constant(0), JDD.Constant(0), new JDDNode[] {}, new JDDNode[] {}, null, allDDRowVars, new JDDVars(), null, 0, null, null, + null, 0, varList, varDDRowVars, null, constantValues); } /** @@ -140,137 +139,70 @@ public class StateModelChecker implements ModelChecker */ public Result check(Expression expr) throws PrismException { + ExpressionFilter exprFilter = null; long timer = 0; - StateListMTBDD states; StateValues vals; - String resultExpl, resultString; - double res = 0.0, minRes = 0.0, maxRes = 0.0; - boolean satInit = false; - int numSat = 0; + String resultString; // Create storage for result result = new Result(); - - // Do model checking and store result vector - timer = System.currentTimeMillis(); - vals = checkExpression(expr); - timer = System.currentTimeMillis() - timer; - mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); - - // Boolean results - if (expr.getType() instanceof TypeBool) { - - // Convert to StateList object - vals = vals.convertToStateValuesMTBDD(); - states = new StateListMTBDD(((StateValuesMTBDD) vals).getJDDNode(), model); - JDD.Ref(((StateValuesMTBDD) vals).getJDDNode()); - // And check how many states are satisfying - numSat = states.size(); - - // Result returned depends on the number of initial states - // and whether it is just a single value (e.g. if the top-level operator is a filter) - - // Case where this is a single value (e.g. filter) - if (expr.returnsSingleValue()) { - // Get result for initial state (although it is the same for all states) - satInit = states.includesAll(start); - result.setResult(new Boolean(satInit)); - result.setExplanation(null); - } - // Case where there is a single initial state - else if (model.getNumStartStates() == 1) { - // Result is true iff satisfied in single initial state - satInit = states.includesAll(start); - resultExpl = "property " + (satInit ? "" : "not ") + "satisfied in the initial state"; - result.setResult(new Boolean(satInit)); - result.setExplanation(resultExpl); + + // 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 + // return single values and have to be treated in this way. + if (!expr.returnsSingleValue()) { + // New filter depends on expression type and number of initial states. + // Boolean expressions... + if (expr.getType() instanceof TypeBool) { + // Result is true iff true for all initial states + exprFilter = new ExpressionFilter("forall", expr, new ExpressionLabel("init")); } - // Case where there are multiple initial states + // Non-Boolean (double or integer) expressions... else { - // Result is true iff satisfied in all initial states - satInit = states.includesAll(start); - resultExpl = "property "; - if (satInit) - resultExpl += "satisfied in all " + model.getNumStartStatesString(); - else - resultExpl += "only satisifed in " + numSat + " of " + model.getNumStartStatesString(); - resultExpl += " initial states"; - result.setResult(new Boolean(satInit)); - result.setExplanation(resultExpl); - } - - // Print extra info to log - if (!expr.returnsSingleValue()) { - // Print number of satisfying states to log - mainLog.print("\nNumber of satisfying states: "); - mainLog.print(numSat == -1 ? ">" + Integer.MAX_VALUE : "" + numSat); - mainLog.println(states.includesAll(reach) ? " (all)" : ""); - // If in "verbose" mode, print out satisfying states to log - if (verbose) { - mainLog.println("\nSatisfying states:"); - states.print(mainLog); + // Result is for the initial state, if there is just one, + // or the range over all initial states, if multiple + if (model.getNumStartStates() == 1) { + exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); + } else { + exprFilter = new ExpressionFilter("range", expr, new ExpressionLabel("init")); } } - - // Clean up - states.clear(); } - - // Non-Boolean (double or integer) results - else { - // Result returned depends on the number of initial states - // and whether it is just a single value (e.g. from if the top-level operator is a filter) - - // Case where this is a single value (e.g. filter) - if (expr.returnsSingleValue()) { - // Get result for initial state (although it is the same for all states) - res = vals.firstFromBDD(start); - result.setResult(new Double(res)); - result.setExplanation(null); - } - // Case where there is a single initial state - else if (model.getNumStartStates() == 1) { - // Result is the value for the single initial state - res = vals.firstFromBDD(start); - // TODO: Object resX = (expr.getType() instanceof TypeInt) ? new Integer((int) res) - resultExpl = "value in the initial state"; - result.setResult(new Double(res)); - result.setExplanation(resultExpl); - } - // Case where there are multiple initial states - else { - // Result is the interval of values from all initial states - minRes = vals.minOverBDD(start); - maxRes = vals.maxOverBDD(start); - // TODO: This will be a range, eventually - // (for now just do first val, as before) - // TODO: also need to handle integer-typed case - // resultExpl = "range over " + model.getNumStartStatesString() + " initial states"; - res = vals.firstFromBDD(start); - resultExpl = "value for first of " + model.getNumStartStatesString() + " initial states"; - result.setResult(new Double(res)); - result.setExplanation(resultExpl); - } - - // Print extra info to log - if (!expr.returnsSingleValue()) { - // If in "verbose" mode, print out result values to log - if (verbose) { - mainLog.println("\nResults (non-zero only) for all states:"); - vals.print(mainLog); - } - } + // Even, when the expression does already return a single value, if the the outermost operator + // of the expression is not a filter, we still need to wrap a new filter around it. + // e.g. 2*filter(...) or 1-P=?[...{...}] + // This because the final result of model checking is only stored when we process a filter. + else if (!(expr instanceof ExpressionFilter)) { + // We just pick the first value (they are all the same) + exprFilter = new ExpressionFilter("first", expr, new ExpressionLabel("init")); + // We stop any additional explanation being displayed to avoid confusion. + exprFilter.setExplanationEnabled(false); + } + + // For any case where a new filter was created above... + if (exprFilter != null) { + // Make it invisible (not that it will be displayed) + exprFilter.setInvisible(true); + // Compute type of new filter expression (will be same as child) + exprFilter.typeCheck(); + // Store as expression to be model checked + expr = exprFilter; } + // Do model checking and store result vector + timer = System.currentTimeMillis(); + vals = checkExpression(expr); + timer = System.currentTimeMillis() - timer; + mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); + // Print result to log resultString = "Result"; if (!("Result".equals(expr.getResultName()))) resultString += " (" + expr.getResultName().toLowerCase() + ")"; - resultString += ": " + result; - if (result.getExplanation() != null) - resultString += " (" + result.getExplanation() + ")"; + resultString += ": " + result.getResultString(); mainLog.print("\n" + resultString + "\n"); - + // Clean up vals.clear(); @@ -845,10 +777,10 @@ public class StateModelChecker implements ModelChecker if (expr.getType() instanceof TypeInt) { // Negative exponent not allowed for integer power JDD.Ref(dd2); - dd = JDD.ITE(JDD.LessThan(dd2, 0), JDD.Constant(0.0/0.0), dd); + dd = JDD.ITE(JDD.LessThan(dd2, 0), JDD.Constant(0.0 / 0.0), dd); // Check for integer overflow JDD.Ref(dd); - dd = JDD.ITE(JDD.GreaterThan(dd, Integer.MAX_VALUE), JDD.Constant(0.0/0.0), dd); + dd = JDD.ITE(JDD.GreaterThan(dd, Integer.MAX_VALUE), JDD.Constant(0.0 / 0.0), dd); } // Late deref of dd1/dd2 because needed above JDD.Deref(dd1); @@ -877,7 +809,7 @@ public class StateModelChecker implements ModelChecker base = dv1.getElement(i); exp = dv2.getElement(i); pow = Math.pow(base, exp); - dv1.setElement(i, (exp < 0 || pow > Integer.MAX_VALUE) ? 0.0/0.0: pow); + dv1.setElement(i, (exp < 0 || pow > Integer.MAX_VALUE) ? 0.0 / 0.0 : pow); } } else { for (i = 0; i < n; i++) @@ -1059,28 +991,42 @@ public class StateModelChecker implements ModelChecker protected StateValues checkExpressionFilter(ExpressionFilter expr) throws PrismException { - FilterOperator op; + // Filter info Expression filter; - StateValues vals = null, res = null; - JDDNode ddFilter = null, ddMatch = null, dd; + FilterOperator op; + String filterStatesString; + StateListMTBDD statesFilter; + boolean filterInit, filterInitSingle, filterTrue; + JDDNode ddFilter = null; + // Result info + StateValues vals = null, resVals = null; + JDDNode ddMatch = null, dd; StateListMTBDD states; - boolean empty = false; - double d = 0.0; + double d = 0.0, d2 = 0.0; boolean b = false; + 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 if (filter == null) filter = Expression.True(); + // Remember whether filter is "true" + filterTrue = Expression.isTrue(filter); + // Store some more info + filterStatesString = filterTrue ? "all states" : "states satisfying filter"; ddFilter = checkExpressionDD(filter); - // Check if filter state set is empty - // (display warning and optimise/catch below) + statesFilter = new StateListMTBDD(ddFilter, model); + // Check if filter state set is empty; we treat this as an error if (ddFilter.equals(JDD.ZERO)) { - empty = true; - mainLog.println("\nWarning: Filter " + filter + " satisfies no states"); + throw new PrismException("Filter satisfies no states"); } + // 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; // Compute result according to filter type op = expr.getOperatorType(); @@ -1090,111 +1036,214 @@ public class StateModelChecker implements ModelChecker if (expr.getType() instanceof TypeBool) { // NB: 'usual' case for filter(print,...) on Booleans is to use no filter mainLog.print("\nSatisfying states"); - mainLog.println(Expression.isTrue(filter) ? ":" : " that are also in filter " + filter + ":"); + mainLog.println(filterTrue ? ":" : " that are also in filter " + filter + ":"); dd = vals.deepCopy().convertToStateValuesMTBDD().getJDDNode(); new StateListMTBDD(dd, model).print(mainLog); JDD.Deref(dd); - } else { // TODO: integer-typed case + } else { + // TODO: integer-typed case: either add to print method or store in StateValues mainLog.println("\nResults (non-zero only) for filter " + filter + ":"); vals.printFiltered(mainLog, ddFilter); } - // Result is unchanged - res = vals; + // Result vector is unchanged; for ARGMIN, 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: - d = empty ? Double.POSITIVE_INFINITY : vals.minOverBDD(ddFilter); - mainLog.println("\nFilter: minimum value for states satisfying " + filter + ": " + d); - res = new StateValuesMTBDD(JDD.Constant(d), model); + // Compute min + d = vals.minOverBDD(ddFilter); + // Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion) + resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)); + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = "Minimum value over " + filterStatesString; + mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); break; case MAX: - d = empty ? Double.NEGATIVE_INFINITY : vals.maxOverBDD(ddFilter); - mainLog.println("\nFilter: maximum value for states satisfying " + filter + ": " + d); - res = new StateValuesMTBDD(JDD.Constant(d), model); + // Compute max + d = vals.maxOverBDD(ddFilter); + // Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion) + resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)); + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = "Maximum value over " + filterStatesString; + mainLog.println("\n" + resultExpl + ": " + resObj); // Also find states that (are close to) selected value for display to log ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); break; case ARGMIN: - d = empty ? Double.POSITIVE_INFINITY : vals.minOverBDD(ddFilter); - mainLog.println("\nFilter: minimum value for states satisfying " + filter + ": " + d); + // Compute/display min + d = vals.minOverBDD(ddFilter); + mainLog.print("\nMinimum value over " + filterStatesString + ": "); + mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d))); + // Find states that (are close to) selected value ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); - res = new StateValuesMTBDD(ddMatch, model); - mainLog.println("Filter: number of states with minimum value: " + res.getNNZString()); + // Store states in vector; for ARGMIN, don't store a single value (in resObj) + // Also, don't bother with explanation string + resVals = new StateValuesMTBDD(ddMatch, model); + // Print out number of matching states, but not the actual states + mainLog.println("\nNumber of states with minimum value: " + resVals.getNNZString()); ddMatch = null; break; case ARGMAX: - d = empty ? Double.NEGATIVE_INFINITY : vals.maxOverBDD(ddFilter); - mainLog.println("\nFilter: maximum value for states satisfying " + filter + ": " + d); + // Compute/display max + d = vals.maxOverBDD(ddFilter); + mainLog.print("\nMaximum value over " + filterStatesString + ": "); + mainLog.println((expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d))); + // Find states that (are close to) selected value ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); JDD.Ref(ddFilter); ddMatch = JDD.And(ddMatch, ddFilter); - res = new StateValuesMTBDD(ddMatch, model); - mainLog.println("Filter: number of states with maximum value: " + res.getNNZString()); + // Store states in vector; for ARGMAX, don't store a single value (in resObj) + // Also, don't bother with explanation string + resVals = new StateValuesMTBDD(ddMatch, model); + // Print out number of matching states, but not the actual states + mainLog.println("\nNumber of states with maximum value: " + resVals.getNNZString()); ddMatch = null; break; case COUNT: - if (empty) - d = 0; - else { - vals.filter(ddFilter); - d = vals.getNNZ(); - } - mainLog.println("\nFilter: count of states satisfying " + filter + ": " + (int) d); - res = new StateValuesMTBDD(JDD.Constant(d), model); + // Compute count + vals.filter(ddFilter); + d = vals.getNNZ(); + // Store as object/vector + resObj = new Integer((int) d); + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = filterTrue ? "Count of satisfying states" : "Count of satisfying states also in filter"; + mainLog.println("\n" + resultExpl + ": " + resObj); break; case SUM: - d = empty ? 0 : vals.sumOverBDD(ddFilter); - mainLog.println("\nFilter: sum over states satisfying " + filter + ": " + (int) d); - res = new StateValuesMTBDD(JDD.Constant(d), model); + // Compute sum + d = vals.sumOverBDD(ddFilter); + // Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion) + resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d)); + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = "Sum over " + filterStatesString; + mainLog.println("\n" + resultExpl + ": " + resObj); break; case AVG: - if (empty) - throw new PrismException("Can't take an average over an empty filter"); + // Compute average d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n()); - mainLog.println("\nFilter: average over states satisfying " + filter + ": " + d); - res = new StateValuesMTBDD(JDD.Constant(d), model); + // Store as object/vector + resObj = new Double(d); + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = "Average over " + filterStatesString; + mainLog.println("\n" + resultExpl + ": " + resObj); break; case FIRST: + // Find first value + d = vals.firstFromBDD(ddFilter); + // Store as object/vector + if (expr.getType() instanceof TypeInt) { + resObj = new Integer((int) d); + } else if (expr.getType() instanceof TypeDouble) { + resObj = new Double(d); + } else { + resObj = new Boolean(d > 0); + } + resVals = new StateValuesMTBDD(JDD.Constant(d), model); + // Create explanation of result and print some details to log + resultExpl = "Value in "; + if (filterInit) { + resultExpl += filterInitSingle ? "the initial state" : "first initial state"; + } else { + resultExpl += filterTrue ? "the first state" : "first state satisfying filter"; + } + mainLog.println("\n" + resultExpl + ": " + resObj); + break; case RANGE: - // TODO: Treat ranges properly - 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 StateValuesMTBDD(JDD.Constant(d), model); + // Find range of values + d = vals.minOverBDD(ddFilter); + d2 = vals.maxOverBDD(ddFilter); + // Store as object + if (expr.getOperand().getType() instanceof TypeInt) { + resObj = new prism.Interval((int) d, (int) d2); + } else { + resObj = new prism.Interval(d, d2); + } + // Leave result vector unchanged: for a range, result is only available from Result object + resVals = vals; + // Set vals to null to stop it being cleared below + vals = null; + // Create explanation of result and print some details to log + resultExpl = "Range of values over "; + resultExpl += filterInit ? "initial states" : filterStatesString; + mainLog.println("\n" + resultExpl + ": " + resObj); break; case FORALL: // Get access to BDD for this dd = vals.convertToStateValuesMTBDD().getJDDNode(); - // Set vals to null so that is not clear()-ed twice - vals = null; - // Check "for all" over filter + // Print some info to log + mainLog.print("\nNumber of states satisfying " + expr.getOperand() + ": "); + states = new StateListMTBDD(dd, model); + mainLog.print(states.sizeString()); + mainLog.println(states.includesAll(reach) ? " (all in model)" : ""); + // Check "for all" over filter, store result JDD.Ref(ddFilter); dd = JDD.And(dd, ddFilter); + states = new StateListMTBDD(dd, model); b = dd.equals(ddFilter); + // Store as object/vector + resObj = new Boolean(b); + resVals = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model); + // Set vals to null so that is not clear()-ed twice + vals = null; + // Create explanation of result and print some details to log + resultExpl = "Property " + (b ? "" : "not ") + "satisfied in "; + mainLog.print("\nProperty satisfied in " + states.sizeString()); + if (filterInit) { + if (filterInitSingle) { + resultExpl += "the initial state"; + } else { + resultExpl += "all initial states"; + } + mainLog.println(" of " + model.getNumStartStatesString() + " initial states."); + } else { + if (filterTrue) { + resultExpl += "all states"; + mainLog.println(" of all " + model.getNumStatesString() + " states."); + } else { + resultExpl += "all filter states"; + mainLog.println(" of " + statesFilter.sizeString() + " filter states."); + } + } + // Derefs JDD.Deref(dd); - res = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model); break; case EXISTS: // Get access to BDD for this dd = vals.convertToStateValuesMTBDD().getJDDNode(); - // Set vals to null so that is not clear()-ed twice - vals = null; // Check "there exists" over filter JDD.Ref(ddFilter); dd = JDD.And(dd, ddFilter); b = !dd.equals(JDD.ZERO); + // Store as object/vector + resObj = new Boolean(b); + resVals = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model); + // Set vals to null so that is not clear()-ed twice + vals = null; + // Create explanation of result and print some details to log + resultExpl = "Property satisfied in "; + if (filterTrue) { + resultExpl += b ? "at least one state" : "no states"; + } else { + resultExpl += b ? "at least one filter state" : "no filter states"; + } + mainLog.println("\n" + resultExpl); + // Derefs JDD.Deref(dd); - res = new StateValuesMTBDD(JDD.Constant(b ? 1.0 : 0.0), model); break; default: JDD.Deref(ddFilter); @@ -1204,11 +1253,9 @@ public class StateModelChecker implements ModelChecker // For some operators, print out some matching states if (ddMatch != null) { states = new StateListMTBDD(ddMatch, model); - int numSat = states.size(); - mainLog.print("\nThere are "); - mainLog.print(numSat == -1 ? ">" + Integer.MAX_VALUE : "" + numSat); - mainLog.print(" states with (approximately) this value"); - if (!verbose && (numSat == -1 || numSat > 10)) { + mainLog.print("\nThere are " + states.sizeString() + " states with "); + mainLog.print(expr.getType() instanceof TypeDouble ? "(approximately) " : "" + "this value"); + if (!verbose && (states.size() == -1 || states.size() > 10)) { mainLog.print(".\nThe first 10 states are displayed below. To view them all, enable verbose mode or use filters.\n"); states.print(mainLog, 10); } else { @@ -1218,12 +1265,21 @@ public class StateModelChecker implements ModelChecker JDD.Deref(ddMatch); } + // Store result + result.setResult(resObj); + // Set result explanation (if none or disabled, clear) + if (expr.getExplanationEnabled() && resultExpl != null) { + result.setExplanation(resultExpl.toLowerCase()); + } else { + result.setExplanation(null); + } + // Derefs, clears JDD.Deref(ddFilter); if (vals != null) vals.clear(); - return res; + return resVals; } }