From 34fc80f4b9fd2f2b786a54dc1a11a3d5ec6f7ff1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 6 Sep 2011 08:18:16 +0000 Subject: [PATCH] Partial implementation of filter for explicit engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3584 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/StateModelChecker.java | 322 ++++++++-------------- prism/src/explicit/StateValues.java | 91 ++++++ prism/src/prism/Interval.java | 10 + 3 files changed, 212 insertions(+), 211 deletions(-) diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index dfa0789d..0c1f7562 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -316,15 +316,11 @@ public class StateModelChecker */ public Result check(Model model, Expression expr) throws PrismException { + ExpressionFilter exprFilter = null; long timer = 0; - Object vals; - BitSet valsBitSet; - StateValues valsSV; - String resultExpl, resultString; - double res = 0.0, minRes = 0.0, maxRes = 0.0; - boolean satInit = false; - int numSat = 0; - + StateValues vals; + String resultString; + // Create storage for result result = new Result(); @@ -336,127 +332,64 @@ public class StateModelChecker // Also evaluate/replace any constants //expr = (Expression) expr.replaceConstants(constantValues); - // Do model checking and store result vector - timer = System.currentTimeMillis(); - valsSV = checkExpression(model, expr); - timer = System.currentTimeMillis() - timer; - mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); - - // Boolean results - if (expr.getType() instanceof TypeBool) { - - // Cast to Bitset - valsBitSet = valsSV.getBitSet(); - // And check how many states are satisfying - numSat = valsBitSet.cardinality(); - - // 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 = valsBitSet.get(model.getFirstInitialState()); - result.setResult(new Boolean(satInit)); - result.setExplanation(null); - } - // Case where there is a single initial state - else if (model.getNumInitialStates() == 1) { - // Result is true iff satisfied in single initial state - satInit = valsBitSet.get(model.getFirstInitialState()); - 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 { - throw new PrismException("Not yet supported"); // TODO - /*// 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); - // TODO: mainLog.println(states.includesAll(reach) ? " (all)" : ""); - // If in "verbose" mode, print out satisfying states to log - if (verbosity > 0) { - mainLog.println("\nSatisfying states:"); - //TODO: 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.getNumInitialStates() == 1) { + exprFilter = new ExpressionFilter("state", 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) - Object o = valsSV.getValue(model.getFirstInitialState()); - result.setResult(o); - result.setExplanation(null); - } - // Case where there is a single initial state - else if (model.getNumInitialStates() == 1) { - // Result is the value for the single initial state - Object o = valsSV.getValue(model.getFirstInitialState()); - resultExpl = "value in the initial state"; - result.setResult(o); - result.setExplanation(resultExpl); - } - // Case where there are multiple initial states - else { - // TODO - /*// 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 (getVerbosity() > 5) { - mainLog.println("\nResults (non-zero only) for all states:"); - mainLog.print(valsSV); - } - } + // 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(model, 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(); + vals.clear(); // Return result return result; @@ -597,22 +530,22 @@ public class StateModelChecker protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr) throws PrismException { - throw new PrismException("Explicit engine does not yet handle filters"); + //throw new PrismException("Explicit engine does not yet handle filters"); - /* // Filter info Expression filter; FilterOperator op; String filterStatesString; - StateListMTBDD statesFilter; + /*StateListMTBDD statesFilter;*/ boolean filterInit, filterInitSingle, filterTrue; - JDDNode ddFilter = null; + BitSet bsFilter = null; // Result info StateValues vals = null, resVals = null; - JDDNode ddMatch = null, dd; - StateListMTBDD states; + BitSet bsMatch = null, bs; + /*StateListMTBDD states;*/ double d = 0.0, d2 = 0.0; boolean b = false; + int count = 0; String resultExpl = null; Object resObj = null; @@ -627,23 +560,23 @@ public class StateModelChecker filterTrue = Expression.isTrue(filter); // Store some more info filterStatesString = filterTrue ? "all states" : "states satisfying filter"; - ddFilter = checkExpressionDD(filter); - statesFilter = new StateListMTBDD(ddFilter, model); + bsFilter = checkExpression(model, filter).getBitSet(); + /*statesFilter = new StateListMTBDD(bsFilter, model);*/ // Check if filter state set is empty; we treat this as an error - if (ddFilter.equals(JDD.ZERO)) { + if (bsFilter.isEmpty()) { 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; + filterInitSingle = filterInit & model.getNumInitialStates() == 1; // Print out number of states satisfying filter - if (!filterInit) - mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString()); + /*if (!filterInit) + mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString());*/ // Compute result according to filter type op = expr.getOperatorType(); switch (op) { - case PRINT: + /*case PRINT: // Format of print-out depends on type if (expr.getType() instanceof TypeBool) { // NB: 'usual' case for filter(print,...) on Booleans is to use no filter @@ -655,7 +588,7 @@ public class StateModelChecker } 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); + vals.printFiltered(mainLog, bsFilter); } // Result vector is unchanged; for ARGMIN, don't store a single value (in resObj) // Also, don't bother with explanation string @@ -665,7 +598,7 @@ public class StateModelChecker break; case MIN: // Compute min - d = vals.minOverBDD(ddFilter); + d = vals.minOverBDD(bsFilter); // 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); @@ -674,12 +607,12 @@ public class StateModelChecker 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); + JDD.Ref(bsFilter); + ddMatch = JDD.And(ddMatch, bsFilter); break; case MAX: // Compute max - d = vals.maxOverBDD(ddFilter); + d = vals.maxOverBDD(bsFilter); // 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); @@ -687,19 +620,19 @@ public class StateModelChecker 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); + bsMatch = vals.getBitSetFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE); + JDD.Ref(bsFilter); + bsMatch = JDD.And(bsMatch, bsFilter); break; case ARGMIN: // Compute/display min - d = vals.minOverBDD(ddFilter); + d = vals.minOverBDD(bsFilter); 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); + JDD.Ref(bsFilter); + ddMatch = JDD.And(ddMatch, bsFilter); // 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); @@ -709,34 +642,33 @@ public class StateModelChecker break; case ARGMAX: // Compute/display max - d = vals.maxOverBDD(ddFilter); + d = vals.maxOverBDD(bsFilter); 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); + JDD.Ref(bsFilter); + ddMatch = JDD.And(ddMatch, bsFilter); // 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; + break;*/ case COUNT: // Compute count - vals.filter(ddFilter); - d = vals.getNNZ(); + count = vals.countOverBitSet(bsFilter); // Store as object/vector - resObj = new Integer((int) d); - resVals = new StateValuesMTBDD(JDD.Constant(d), model); + resObj = new Integer(count); + resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); // 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: + /*case SUM: // Compute sum - d = vals.sumOverBDD(ddFilter); + d = vals.sumOverBDD(bsFilter); // 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); @@ -746,26 +678,18 @@ public class StateModelChecker break; case AVG: // Compute average - d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n()); + d = vals.sumOverBDD(bsFilter) / JDD.GetNumMinterms(bsFilter, allDDRowVars.n()); // 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; + 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); + resObj = vals.firstFromBitSet(bsFilter); + resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); // Create explanation of result and print some details to log resultExpl = "Value in "; if (filterInit) { @@ -777,14 +701,7 @@ public class StateModelChecker break; case RANGE: // 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); - } + resObj = new prism.Interval(vals.minOverBitSet(bsFilter), vals.maxOverBitSet(bsFilter)); // 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 @@ -795,51 +712,43 @@ public class StateModelChecker mainLog.println("\n" + resultExpl + ": " + resObj); break; case FORALL: - // Get access to BDD for this - dd = vals.convertToStateValuesMTBDD().getJDDNode(); + // Get access to BitSet for this + bs = vals.getBitSet(); // 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); + mainLog.print(bs.cardinality()); + mainLog.println(bs.cardinality() == model.getNumStates() ? " (all in model)" : ""); + // Check "for all" over filter + b = vals.forallOverBitSet(bsFilter); // 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; + resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); // Create explanation of result and print some details to log resultExpl = "Property " + (b ? "" : "not ") + "satisfied in "; - mainLog.print("\nProperty satisfied in " + states.sizeString()); + mainLog.print("\nProperty satisfied in " + vals.countOverBitSet(bsFilter)); if (filterInit) { if (filterInitSingle) { resultExpl += "the initial state"; } else { resultExpl += "all initial states"; } - mainLog.println(" of " + model.getNumStartStatesString() + " initial states."); + mainLog.println(" of " + model.getNumInitialStates() + " initial states."); } else { if (filterTrue) { resultExpl += "all states"; - mainLog.println(" of all " + model.getNumStatesString() + " states."); + mainLog.println(" of all " + model.getNumStates() + " states."); } else { resultExpl += "all filter states"; - mainLog.println(" of " + statesFilter.sizeString() + " filter states."); + mainLog.println(" of " + bsFilter.cardinality() + " filter states."); } } - // Derefs - JDD.Deref(dd); break; - case EXISTS: + /*case EXISTS: // Get access to BDD for this dd = vals.convertToStateValuesMTBDD().getJDDNode(); // Check "there exists" over filter - JDD.Ref(ddFilter); - dd = JDD.And(dd, ddFilter); + JDD.Ref(bsFilter); + dd = JDD.And(dd, bsFilter); b = !dd.equals(JDD.ZERO); // Store as object/vector resObj = new Boolean(b); @@ -856,25 +765,18 @@ public class StateModelChecker mainLog.println("\n" + resultExpl); // Derefs JDD.Deref(dd); - break; + break;*/ case STATE: // Check filter satisfied by exactly one state - if (statesFilter.size() != 1) { + if (bsFilter.cardinality() != 1) { String s = "Filter should be satisfied in exactly 1 state"; - s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " states)"; + s += " (but \"" + filter + "\" is true in " + bsFilter.cardinality() + " states)"; throw new PrismException(s); } // Find first (only) 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); + resObj = vals.firstFromBitSet(bsFilter); + resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); // Create explanation of result and print some details to log resultExpl = "Value in "; if (filterInit) { @@ -885,13 +787,12 @@ public class StateModelChecker mainLog.println("\n" + resultExpl + ": " + resObj); break; default: - JDD.Deref(ddFilter); throw new PrismException("Unrecognised filter type \"" + expr.getOperatorName() + "\""); } // For some operators, print out some matching states - if (ddMatch != null) { - states = new StateListMTBDD(ddMatch, model); + /*if (bsMatch != null) { + states = new StateListMTBDD(bsMatch, model); 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)) { @@ -901,8 +802,8 @@ public class StateModelChecker mainLog.print(":\n"); states.print(mainLog); } - JDD.Deref(ddMatch); - } + JDD.Deref(bsMatch); + }*/ // Store result result.setResult(resObj); @@ -914,11 +815,10 @@ public class StateModelChecker } // Derefs, clears - JDD.Deref(ddFilter); if (vals != null) vals.clear(); - return resVals;*/ + return resVals; } /** diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index adda7cb5..b76d0aaf 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -28,6 +28,10 @@ package explicit; import java.util.BitSet; +import com.sun.org.apache.xerces.internal.parsers.IntegratedParserConfiguration; + +import jdd.JDDNode; + import parser.type.Type; import parser.type.TypeBool; import parser.type.TypeDouble; @@ -302,6 +306,93 @@ public class StateValues } */ + // Filter operations + + /** + * Get the value of first vector element that is in the (BitSet) filter. + */ + public Object firstFromBitSet(BitSet filter) + { + return getValue(filter.nextSetBit(0)); + } + + /** + * Get the minimum value of those that are in the (BitSet) filter. + */ + public Object minOverBitSet(BitSet filter) throws PrismException + { + if (type instanceof TypeInt) { + int minI = Integer.MAX_VALUE; + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (valuesI[i] < minI) + minI = valuesI[i]; + } + return new Integer(minI); + } else if (type instanceof TypeDouble) { + double minD = Double.POSITIVE_INFINITY; + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (valuesD[i] < minD) + minD = valuesD[i]; + } + return new Double(minD); + } + throw new PrismException("Can't take min over a vector of type " + type); + } + + /** + * Get the maximum value of those that are in the (BitSet) filter. + */ + public Object maxOverBitSet(BitSet filter) throws PrismException + { + if (type instanceof TypeInt) { + int maxI = Integer.MIN_VALUE; + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (valuesI[i] > maxI) + maxI = valuesI[i]; + } + return new Integer(maxI); + } else if (type instanceof TypeDouble) { + double maxD = Double.NEGATIVE_INFINITY; + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (valuesD[i] > maxD) + maxD = valuesD[i]; + } + return new Double(maxD); + } + throw new PrismException("Can't take max over a vector of type " + type); + } + + /** + * Check if true for all states in the (BitSet) filter. + */ + public boolean forallOverBitSet(BitSet filter) throws PrismException + { + if (type instanceof TypeBool) { + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (!valuesB.get(i)) + return new Boolean(false); + } + return new Boolean(true); + } + throw new PrismException("Can't take forall over a vector of type " + type); + } + + /** + * Count the number of states with value true from those in the (BitSet) filter. + */ + public int countOverBitSet(BitSet filter) throws PrismException + { + if (type instanceof TypeBool) { + int count = 0; + for (int i = filter.nextSetBit(0); i >= 0; i = filter.nextSetBit(i + 1)) { + if (valuesB.get(i)) + count++; + } + return new Integer(count); + } + throw new PrismException("Can't take count over a vector of type " + type); + } + // PRINTING STUFF /** diff --git a/prism/src/prism/Interval.java b/prism/src/prism/Interval.java index e86d0bd5..59fc4862 100644 --- a/prism/src/prism/Interval.java +++ b/prism/src/prism/Interval.java @@ -35,6 +35,16 @@ public class Interval public Object lower; public Object upper; + /** + * Construct an Interval. + * (lower and upper should be of the same type: Integer or Double) + */ + public Interval(Object lower, Object upper) + { + this.lower = lower; + this.upper = upper; + } + /** * Construct an integer Interval. */