From 14025e109d058be23cf74819864e76285eefb9eb Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 5 Sep 2011 22:30:28 +0000 Subject: [PATCH] Improvements to StateValues class + it's use in explicit model checking. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3581 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 4 +- prism/src/explicit/CTMDPModelChecker.java | 4 +- prism/src/explicit/DTMCModelChecker.java | 10 +- prism/src/explicit/MDPModelChecker.java | 10 +- prism/src/explicit/ProbModelChecker.java | 12 +- prism/src/explicit/STPGModelChecker.java | 10 +- prism/src/explicit/StateModelChecker.java | 412 +++++++++++++++++++--- prism/src/explicit/StateValues.java | 84 ++++- prism/src/parser/type/Type.java | 12 + prism/src/parser/type/TypeBool.java | 7 + prism/src/parser/type/TypeClock.java | 7 + prism/src/parser/type/TypeDouble.java | 7 + prism/src/parser/type/TypeInt.java | 7 + 13 files changed, 488 insertions(+), 98 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index a3f5afd2..26ac5f9e 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -93,8 +93,8 @@ public class CTMCModelChecker extends DTMCModelChecker } // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // compute probabilities diff --git a/prism/src/explicit/CTMDPModelChecker.java b/prism/src/explicit/CTMDPModelChecker.java index bb2c8fba..e4657a79 100644 --- a/prism/src/explicit/CTMDPModelChecker.java +++ b/prism/src/explicit/CTMDPModelChecker.java @@ -55,8 +55,8 @@ public class CTMDPModelChecker extends MDPModelChecker } // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // compute probabilities diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 0081d1ea..ebb3261a 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -104,8 +104,8 @@ public class DTMCModelChecker extends ProbModelChecker } // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // compute probabilities @@ -131,8 +131,8 @@ public class DTMCModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1, @@ -180,7 +180,7 @@ public class DTMCModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operand first - b = (BitSet) checkExpression(model, expr.getOperand2()); + b = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index fbe5ddb8..1cd24d45 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -107,8 +107,8 @@ public class MDPModelChecker extends ProbModelChecker } // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1, @@ -140,8 +140,8 @@ public class MDPModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1, @@ -189,7 +189,7 @@ public class MDPModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operand first - b = (BitSet) checkExpression(model, expr.getOperand2()); + b = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb = " + JDD.GetNumMintermsString(b1, diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 23fa2607..a6892d29 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -47,9 +47,9 @@ public class ProbModelChecker extends StateModelChecker // Model checking functions @Override - public Object checkExpression(Model model, Expression expr) throws PrismException + public StateValues checkExpression(Model model, Expression expr) throws PrismException { - Object res; + StateValues res; // P operator if (expr instanceof ExpressionProb) { @@ -74,7 +74,7 @@ public class ProbModelChecker extends StateModelChecker /** * Model check a P operator expression and return the values for all states. */ - protected Object checkExpressionProb(Model model, ExpressionProb expr) throws PrismException + protected StateValues checkExpressionProb(Model model, ExpressionProb expr) throws PrismException { Expression pb; // Probability bound (expression) double p = 0; // Probability bound (actual value) @@ -141,14 +141,14 @@ public class ProbModelChecker extends StateModelChecker else { BitSet sol = probs.getBitSetFromInterval(relOp, p); probs.clear(); - return sol; + return StateValues.createFromBitSet(sol, model.getNumStates()); } } /** * Model check an R operator expression and return the values for all states. */ - protected Object checkExpressionReward(Model model, ExpressionReward expr) throws PrismException + protected StateValues checkExpressionReward(Model model, ExpressionReward expr) throws PrismException { Object rs; // Reward struct index RewardStruct rewStruct = null; // Reward struct object @@ -246,7 +246,7 @@ public class ProbModelChecker extends StateModelChecker else { BitSet sol = rews.getBitSetFromInterval(relOp, r); rews.clear(); - return sol; + return StateValues.createFromBitSet(sol, model.getNumStates()); } } } diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index c7698e45..771b1b02 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/prism/src/explicit/STPGModelChecker.java @@ -105,8 +105,8 @@ public class STPGModelChecker extends ProbModelChecker } // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1, @@ -138,8 +138,8 @@ public class STPGModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operands first - b1 = (BitSet) checkExpression(model, expr.getOperand1()); - b2 = (BitSet) checkExpression(model, expr.getOperand2()); + b1 = checkExpression(model, expr.getOperand1()).getBitSet(); + b2 = checkExpression(model, expr.getOperand2()).getBitSet(); // print out some info about num states // mainLog.print("\nb1 = " + JDD.GetNumMintermsString(b1, @@ -165,7 +165,7 @@ public class STPGModelChecker extends ProbModelChecker ModelCheckerResult res = null; // model check operands first - target = (BitSet) checkExpression(model, expr.getOperand2()); + target = checkExpression(model, expr.getOperand2()).getBitSet(); res = computeReachRewards((STPG) model, rewards, target, min1, min2); rews = StateValues.createFromDoubleArray(res.soln); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 08967139..dfa0789d 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -32,7 +32,9 @@ import java.util.*; import parser.State; import parser.Values; import parser.ast.*; +import parser.ast.ExpressionFilter.FilterOperator; import parser.type.*; +import prism.Prism; import prism.PrismException; import prism.PrismLog; import prism.PrismPrintStreamLog; @@ -336,7 +338,7 @@ public class StateModelChecker // Do model checking and store result vector timer = System.currentTimeMillis(); - vals = checkExpression(model, expr); + valsSV = checkExpression(model, expr); timer = System.currentTimeMillis() - timer; mainLog.println("\nTime for model checking: " + timer / 1000.0 + " seconds."); @@ -344,7 +346,7 @@ public class StateModelChecker if (expr.getType() instanceof TypeBool) { // Cast to Bitset - valsBitSet = (BitSet) vals; + valsBitSet = valsSV.getBitSet(); // And check how many states are satisfying numSat = valsBitSet.cardinality(); @@ -403,9 +405,6 @@ public class StateModelChecker // 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) - // Cast to Bitset - valsSV = (StateValues) vals; - // 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) @@ -442,7 +441,7 @@ public class StateModelChecker // If in "verbose" mode, print out result values to log if (getVerbosity() > 5) { mainLog.println("\nResults (non-zero only) for all states:"); - mainLog.print(vals); + mainLog.print(valsSV); } } } @@ -470,9 +469,9 @@ public class StateModelChecker * {@link #setModulesFile} and {@link #setPropertiesFile} * to attach the original model/properties files. */ - public Object checkExpression(Model model, Expression expr) throws PrismException + public StateValues checkExpression(Model model, Expression expr) throws PrismException { - Object res = null; + StateValues res = null; // Binary ops // (just "and" for now - more to come later) @@ -493,7 +492,7 @@ public class StateModelChecker } // Filter else if (expr instanceof ExpressionFilter) { - throw new PrismException("Explicit engine does not yet handle filters"); + res = checkExpressionFilter(model, (ExpressionFilter) expr); } // Anything else - just evaluate expression repeatedly @@ -501,30 +500,21 @@ public class StateModelChecker // Evaluate/replace any constants first expr = (Expression) expr.replaceConstants(constantValues); + int numStates = model.getNumStates(); + res = new StateValues(expr.getType(), numStates); + List statesList = model.getStatesList(); if (expr.getType() instanceof TypeBool) { - int numStates = model.getNumStates(); - BitSet bs = new BitSet(numStates); - List statesList = model.getStatesList(); for (int i = 0; i < numStates; i++) { - bs.set(i, expr.evaluateBoolean(statesList.get(i))); + res.setBooleanValue(i, expr.evaluateBoolean(statesList.get(i))); } - res = bs; } else if (expr.getType() instanceof TypeInt) { - int numStates = model.getNumStates(); - StateValues sv = new StateValues(expr.getType(), numStates); - List statesList = model.getStatesList(); for (int i = 0; i < numStates; i++) { - sv.setIntValue(i, expr.evaluateInt(statesList.get(i))); + res.setIntValue(i, expr.evaluateInt(statesList.get(i))); } - res = sv; } else if (expr.getType() instanceof TypeDouble) { - int numStates = model.getNumStates(); - StateValues sv = new StateValues(expr.getType(), numStates); - List statesList = model.getStatesList(); for (int i = 0; i < numStates; i++) { - sv.setDoubleValue(i, expr.evaluateDouble(statesList.get(i))); + res.setDoubleValue(i, expr.evaluateDouble(statesList.get(i))); } - res = sv; } } // Anything else - error @@ -538,45 +528,30 @@ public class StateModelChecker /** * Model check a binary operator. */ - protected Object checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException + protected StateValues checkExpressionBinaryOp(Model model, ExpressionBinaryOp expr) throws PrismException { // (just "and" for now - more to come later) - BitSet res1bs = (BitSet) checkExpression(model, expr.getOperand1()); - BitSet res2bs = (BitSet) checkExpression(model, expr.getOperand2()); - res1bs.and(res2bs); - return res1bs; + StateValues res1 = checkExpression(model, expr.getOperand1()); + StateValues res2 = checkExpression(model, expr.getOperand2()); + res1.and(res2); + res2.clear(); + return res1; } /** * Model check a literal. */ - protected Object checkExpressionLiteral(Model model, ExpressionLiteral expr) throws PrismException - { - Type type; - Object res = null; - type = expr.getType(); - if (type instanceof TypeBool) { - BitSet bs = new BitSet(model.getNumStates()); - if (expr.evaluateBoolean()) { - bs.set(0, model.getNumStates()); - } - res = bs; - } else if (type instanceof TypeInt || type instanceof TypeDouble) { - res = new StateValues(expr.getType(), model.getNumStates(), expr.evaluate()); - } else { - throw new PrismException("Couldn't check literal " + expr); - } - - return res; + protected StateValues checkExpressionLiteral(Model model, ExpressionLiteral expr) throws PrismException + { + return new StateValues(expr.getType(), model.getNumStates(), expr.evaluate()); } /** * Model check a label. */ - protected Object checkExpressionLabel(Model model, ExpressionLabel expr) throws PrismException + protected StateValues checkExpressionLabel(Model model, ExpressionLabel expr) throws PrismException { LabelList ll; - Map labels; int i; // treat special cases @@ -586,14 +561,14 @@ public class StateModelChecker for (i = 0; i < numStates; i++) { bs.set(i, model.isFixedDeadlockState(i)); } - return bs; + return StateValues.createFromBitSet(bs, numStates); } else if (expr.getName().equals("init")) { int numStates = model.getNumStates(); BitSet bs = new BitSet(numStates); for (i = 0; i < numStates; i++) { bs.set(i, model.isInitialState(i)); } - return bs; + return StateValues.createFromBitSet(bs, numStates); } else { ll = propertiesFile.getCombinedLabelList(); i = ll.getLabelIndex(expr.getName()); @@ -601,17 +576,12 @@ public class StateModelChecker throw new PrismException("Unknown label \"" + expr.getName() + "\" in property"); // check recursively return checkExpression(model, ll.getLabel(i)); - - // TODO: remove this: - //labels = loadLabelsFile(getLabelsFilename()); - // get expression associated with label - //return labels.get(expr.getName()); } } // Check property ref - protected Object checkExpressionProp(Model model, ExpressionProp expr) throws PrismException + protected StateValues checkExpressionProp(Model model, ExpressionProp expr) throws PrismException { // Look up property and check recursively Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName()); @@ -623,6 +593,334 @@ public class StateModelChecker } } + // Check filter + + protected StateValues checkExpressionFilter(Model model, ExpressionFilter expr) throws PrismException + { + throw new PrismException("Explicit engine does not yet handle filters"); + + /* + // Filter info + Expression filter; + 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; + double d = 0.0, d2 = 0.0; + boolean b = false; + String resultExpl = null; + Object resObj = null; + + // Check operand recursively + vals = checkExpression(model, 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); + statesFilter = new StateListMTBDD(ddFilter, model); + // Check if filter state set is empty; we treat this as an error + if (ddFilter.equals(JDD.ZERO)) { + 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; + // Print out number of states satisfying filter + if (!filterInit) + mainLog.println("\nStates satisfying filter " + filter + ": " + statesFilter.sizeString()); + + // Compute result according to filter type + op = expr.getOperatorType(); + switch (op) { + 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 + mainLog.print("\nSatisfying states"); + 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: either add to print method or store in StateValues + mainLog.println("\nResults (non-zero only) for filter " + filter + ":"); + vals.printFiltered(mainLog, ddFilter); + } + // 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: + // 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: + // 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: + // 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); + // 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: + // 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); + // 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: + // 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: + // 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: + // Compute average + d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, 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; + 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: + // 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(); + // 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); + break; + 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); + 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); + break; + case STATE: + // Check filter satisfied by exactly one state + if (statesFilter.size() != 1) { + String s = "Filter should be satisfied in exactly 1 state"; + s += " (but \"" + filter + "\" is true in " + statesFilter.size() + " 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); + // Create explanation of result and print some details to log + resultExpl = "Value in "; + if (filterInit) { + resultExpl += "the initial state"; + } else { + resultExpl += "the filter state"; + } + 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); + 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 a print filter.\n"); + states.print(mainLog, 10); + } else { + mainLog.print(":\n"); + states.print(mainLog); + } + 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 resVals;*/ + } + /** * Loads labels from a PRISM labels file and stores them in BitSet objects. * (Actually, it returns a map from label name Strings to BitSets.) diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index 6eaaa8a0..adda7cb5 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -29,9 +29,12 @@ package explicit; import java.util.BitSet; import parser.type.Type; +import parser.type.TypeBool; import parser.type.TypeDouble; import parser.type.TypeInt; import prism.PrismException; +import prism.PrismFileLog; +import prism.PrismLangException; import prism.PrismLog; /** @@ -39,13 +42,14 @@ import prism.PrismLog; */ public class StateValues { - // Type (int or double) + // Type (int, double or boolean) protected Type type; // Size protected int size; // Vector (only one used, depending on type) protected int[] valuesI; protected double[] valuesD; + protected BitSet valuesB; // CONSTRUCTORS, etc. @@ -59,44 +63,56 @@ public class StateValues size = 0; valuesI = null; valuesD = null; + valuesB = null; } /** * Construct a new state values vector of the given type and size. * All values are initially set to zero. */ - public StateValues(Type type, int size) + public StateValues(Type type, int size) throws PrismLangException { - // TODO: check this: ? probably always returns Double due to typing - this(type, size, type instanceof TypeInt ? new Integer(0) : new Double(0.0)); + this(type, size, type.defaultValue()); } /** * Construct a new state values vector of the given type and size, - * initialising all values to 'init'. - * @param type Value type (int/double) + * initialising all values to {@code init}. + * Throws an exception of {@code init} is of the wrong type. + * @param type Value type * @param size Vector size - * @param init Initial value for all states (as Integer or Double object) + * @param init Initial value for all states (as an appropriate Object) */ - public StateValues(Type type, int size, Object init) + public StateValues(Type type, int size, Object init) throws PrismLangException { - int i, initI; - double initD; + super(); + int i; this.type = type; this.size = size; - valuesI = null; - valuesD = null; // Create/initialise array of appropriate type if (type instanceof TypeInt) { valuesI = new int[size]; - initI = ((Integer) init).intValue(); + Integer objI = (Integer) type.castValueTo(init); + int initI = objI.intValue(); for (i = 0; i < size; i++) valuesI[i] = initI; } else if (type instanceof TypeDouble) { valuesD = new double[size]; - initD = ((Double) init).doubleValue(); + Double objD = (Double) type.castValueTo(init); + double initD = objD.doubleValue(); for (i = 0; i < size; i++) valuesD[i] = initD; + } else if (type instanceof TypeBool) { + Boolean objB = (Boolean) type.castValueTo(init); + boolean initB = objB.booleanValue(); + if (initB) { + valuesB = new BitSet(size); + valuesB.set(0, size); + } else { + valuesB = new BitSet(); + } + } else { + throw new PrismLangException("Cannot create an vector of type " + type); } } @@ -109,11 +125,23 @@ public class StateValues StateValues sv = new StateValues(); sv.type = TypeDouble.getInstance(); sv.size = array.length; - sv.valuesI = null; sv.valuesD = array; return sv; } + /** + * Create a new (Boolean-valued) state values vector from an existing BitSet. + * The BitSet is stored directly, not copied. + */ + public static StateValues createFromBitSet(BitSet bs, int size) + { + StateValues sv = new StateValues(); + sv.type = TypeBool.getInstance(); + sv.size = size; + sv.valuesB = bs; + return sv; + } + /** * Create a new (double-valued) state values vector from a BitSet, * where each entry is 1.0 if in the bitset, 0.0 otherwise. @@ -206,6 +234,19 @@ public class StateValues valuesD[i] = val; } + public void setBooleanValue(int i, boolean val) + { + valuesB.set(i, val); + } + + public void and(StateValues sv) throws PrismException + { + if (!(type instanceof TypeBool) || !(sv.type instanceof TypeBool)) { + throw new PrismException("Conjunction can only be applied to Boolean vectors"); + } + valuesB.and(sv.valuesB); + } + // ... // clear (free memory) @@ -218,6 +259,7 @@ public class StateValues { valuesI = null; valuesD = null; + valuesB = null; } // METHODS TO ACCESS VECTOR DATA @@ -231,11 +273,21 @@ public class StateValues return valuesI[i]; } else if (type instanceof TypeDouble) { return valuesD[i]; + } else if (type instanceof TypeBool) { + return valuesB.get(i); } else { return null; } } + /** + * For Boolean-valued vectors, get the BitSet storing the data. + */ + public BitSet getBitSet() + { + return valuesB; + } + /* // get num non zeros @@ -274,6 +326,6 @@ public class StateValues public StateValues deepCopy() throws PrismException { // TODO - throw new PrismException("Not impleneted yet"); + throw new PrismException("Not implemented yet"); } } diff --git a/prism/src/parser/type/Type.java b/prism/src/parser/type/Type.java index cf4ca1b9..53158ba3 100644 --- a/prism/src/parser/type/Type.java +++ b/prism/src/parser/type/Type.java @@ -30,8 +30,20 @@ import prism.PrismLangException; public abstract class Type { + /** + * Returns the string denoting this type, e.g. "int", "bool". + */ public abstract String getTypeString(); + /** + * Returns the default value for this type, assuming no initialisation specified. + */ + public Object defaultValue() + { + // Play safe: assume null + return null; + } + /** * Returns true iff a variable of this type can be assigned a value that is of type {@code type}. */ diff --git a/prism/src/parser/type/TypeBool.java b/prism/src/parser/type/TypeBool.java index b325e24e..6496dffd 100644 --- a/prism/src/parser/type/TypeBool.java +++ b/prism/src/parser/type/TypeBool.java @@ -46,11 +46,18 @@ public class TypeBool extends Type return (o instanceof TypeBool); } + @Override public String getTypeString() { return "bool"; } + @Override + public Object defaultValue() + { + return new Boolean(false); + } + public static TypeBool getInstance() { return singleton; diff --git a/prism/src/parser/type/TypeClock.java b/prism/src/parser/type/TypeClock.java index b75ea9c2..1285b1d4 100644 --- a/prism/src/parser/type/TypeClock.java +++ b/prism/src/parser/type/TypeClock.java @@ -46,11 +46,18 @@ public class TypeClock extends Type return (o instanceof TypeClock); } + @Override public String getTypeString() { return "clock"; } + @Override + public Object defaultValue() + { + return new Double(0.0); + } + public static TypeClock getInstance() { return singleton; diff --git a/prism/src/parser/type/TypeDouble.java b/prism/src/parser/type/TypeDouble.java index 122883da..7cc03d73 100644 --- a/prism/src/parser/type/TypeDouble.java +++ b/prism/src/parser/type/TypeDouble.java @@ -46,11 +46,18 @@ public class TypeDouble extends Type return (o instanceof TypeDouble); } + @Override public String getTypeString() { return "double"; } + @Override + public Object defaultValue() + { + return new Double(0.0); + } + public static TypeDouble getInstance() { return singleton; diff --git a/prism/src/parser/type/TypeInt.java b/prism/src/parser/type/TypeInt.java index b464fb95..a33f322a 100644 --- a/prism/src/parser/type/TypeInt.java +++ b/prism/src/parser/type/TypeInt.java @@ -46,11 +46,18 @@ public class TypeInt extends Type return (o instanceof TypeInt); } + @Override public String getTypeString() { return "int"; } + @Override + public Object defaultValue() + { + return new Integer(0); + } + public static TypeInt getInstance() { return singleton;