diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index a38c9f8c..33a9bfe5 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -556,7 +556,7 @@ public class NondetModelChecker extends NonProbModelChecker Vector tmptargetDDs = new Vector(); List tmpmultitargetDDs = new ArrayList(); List tmpmultitargetIDs = new ArrayList(); - ArrayList tmpdra = new ArrayList(); + ArrayList> tmpdra = new ArrayList>(); ArrayList tmpdraDDRowVars = new ArrayList(); ArrayList tmpdraDDColVars = new ArrayList(); int count = 0; @@ -685,7 +685,7 @@ public class NondetModelChecker extends NonProbModelChecker * @param expr A multi objective * @throws PrismException */ - protected void ensureNoTimeBounded(ExpressionFunc expr) throws PrismException + private void ensureNoTimeBounded(ExpressionFunc expr) throws PrismException { try { expr.accept(new ASTTraverse() @@ -1216,8 +1216,11 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(ec); } - // Contents of a P operator, i.e. a path formula - + // Model checking functions + + /** + * Compute probabilities for the contents of a P operator. + */ protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) @@ -1229,8 +1232,9 @@ public class NondetModelChecker extends NonProbModelChecker } } - // Simple path formula for P operator (one temporal op, possibly negated) - + /** + * Compute probabilities for a simple, non-LTL path operator. + */ protected StateValues checkProbPathFormulaSimple(Expression expr, boolean qual, boolean min) throws PrismException { StateValues probs = null; @@ -1277,128 +1281,9 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // LTL-like path formula for P operator - - protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException - { - LTLModelChecker mcLtl; - StateValues probsProduct = null, probs = null; - Expression ltl; - Vector labelDDs; - DRA dra; - NondetModel modelProduct; - NondetModelChecker mcProduct; - JDDNode startMask; - JDDVars draDDRowVars, draDDColVars; - int i; - long l; - - // Can't do LTL with time-bounded variants of the temporal operators - try { - expr.accept(new ASTTraverse() - { - public void visitPre(ExpressionTemporal e) throws PrismLangException - { - if (e.getLowerBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - if (e.getUpperBound() != null) - throw new PrismLangException(e.getOperatorSymbol()); - } - }); - } catch (PrismLangException e) { - String s = "Temporal operators (like " + e.getMessage() + ")"; - s += " cannot have time bounds for LTL properties"; - throw new PrismException(s); - } - - // Can't do "dfa" properties yet - if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { - throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); - } - - // For LTL model checking routines - mcLtl = new LTLModelChecker(prism); - - // Model check maximal state formulas - labelDDs = new Vector(); - ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs); - - // Convert LTL formula to deterministic Rabin automaton (DRA) - // For min probabilities, need to negate the formula - // (But check fairness setting since this may affect min/max) - // (add parentheses to allow re-parsing if required) - if (min && !fairness) { - ltl = Expression.Not(Expression.Parenth(ltl)); - } - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); - l = System.currentTimeMillis(); - dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); - /*try { - mainLog.print(dra); - dra.printDot(new java.io.PrintStream("dra.dot")); - } catch(Exception e) {}*/ - l = System.currentTimeMillis() - l; - mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); - - // Build product of MDP and automaton - mainLog.println("\nConstructing MDP-DRA product..."); - draDDRowVars = new JDDVars(); - draDDColVars = new JDDVars(); - modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars); - mainLog.println(); - modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); - // Output product, if required - if (prism.getExportProductTrans()) { - try { - mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); - modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename())); - } catch (FileNotFoundException e) { - mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); - } - } - if (prism.getExportProductStates()) { - mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); - modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename())); - } - - // Find accepting MECs + compute reachability probabilities - mainLog.println("\nFinding accepting end components..."); - JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness); - mainLog.println("\nComputing reachability probabilities..."); - mcProduct = new NondetModelChecker(prism, modelProduct, null); - probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); - - // subtract from 1 if we're model checking a negated formula for regular Pmin - if (min && !fairness) { - probsProduct.subtractFromOne(); - } - - // Convert probability vector to original model - // First, filter over DRA start states - startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars); - JDD.Ref(model.getReach()); - startMask = JDD.And(model.getReach(), startMask); - probsProduct.filter(startMask); - // Then sum over DD vars for the DRA state - probs = probsProduct.sumOverDDVars(draDDRowVars, model); - - // Deref, clean up - probsProduct.clear(); - modelProduct.clear(); - for (i = 0; i < labelDDs.size(); i++) { - JDD.Deref(labelDDs.get(i)); - } - JDD.Deref(acc); - JDD.Deref(startMask); - draDDRowVars.derefAll(); - draDDColVars.derefAll(); - - return probs; - } - - // next - + /** + * Compute probabilities for a next operator. + */ protected StateValues checkProbNext(ExpressionTemporal expr, boolean min) throws PrismException { JDDNode b; @@ -1420,8 +1305,9 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // bounded until - + /** + * Compute probabilities for a bounded until operator. + */ protected StateValues checkProbBoundedUntil(ExpressionTemporal expr, boolean min) throws PrismException { int time; @@ -1476,10 +1362,10 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // until (unbounded) - - // this method is split into two steps so that the LTL model checker can use the second part directly - + /** + * Compute probabilities for an (unbounded) until operator. + * Note: This method is split into two steps so that the LTL model checker can use the second part directly. + */ protected StateValues checkProbUntil(ExpressionTemporal expr, boolean qual, boolean min) throws PrismException { JDDNode b1, b2; @@ -1515,8 +1401,13 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // until (unbounded): b1/b2 are bdds for until operands - + /** + * Compute probabilities for an (unbounded) until operator. + * @param b1 Remain in these states + * @param b2 Target states + * @param qual True if only qualititative (0/1) results are needed + * @param min Min or max probabilities (true=min, false=max) + */ protected StateValues checkProbUntil(JDDNode b1, JDDNode b2, boolean qual, boolean min) throws PrismException { JDDNode splus, newb1, newb2; @@ -1591,8 +1482,130 @@ public class NondetModelChecker extends NonProbModelChecker return probs; } - // cumulative reward + /** + * Compute probabilities for an LTL path formula + */ + protected StateValues checkProbPathFormulaLTL(Expression expr, boolean qual, boolean min) throws PrismException + { + LTLModelChecker mcLtl; + StateValues probsProduct = null, probs = null; + Expression ltl; + Vector labelDDs; + DRA dra; + NondetModel modelProduct; + NondetModelChecker mcProduct; + JDDNode startMask; + JDDVars draDDRowVars, draDDColVars; + int i; + long l; + + // Can't do LTL with time-bounded variants of the temporal operators + try { + expr.accept(new ASTTraverse() + { + public void visitPre(ExpressionTemporal e) throws PrismLangException + { + if (e.getLowerBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + if (e.getUpperBound() != null) + throw new PrismLangException(e.getOperatorSymbol()); + } + }); + } catch (PrismLangException e) { + String s = "Temporal operators (like " + e.getMessage() + ")"; + s += " cannot have time bounds for LTL properties"; + throw new PrismException(s); + } + + // Can't do "dfa" properties yet + if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { + throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); + } + + // For LTL model checking routines + mcLtl = new LTLModelChecker(prism); + + // Model check maximal state formulas + labelDDs = new Vector(); + ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs); + + // Convert LTL formula to deterministic Rabin automaton (DRA) + // For min probabilities, need to negate the formula + // (But check fairness setting since this may affect min/max) + // (add parentheses to allow re-parsing if required) + if (min && !fairness) { + ltl = Expression.Not(Expression.Parenth(ltl)); + } + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + l = System.currentTimeMillis(); + dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.getNumAcceptancePairs() + " pairs."); + /*try { + mainLog.print(dra); + dra.printDot(new java.io.PrintStream("dra.dot")); + } catch(Exception e) {}*/ + l = System.currentTimeMillis() - l; + mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); + + // Build product of MDP and automaton + mainLog.println("\nConstructing MDP-DRA product..."); + draDDRowVars = new JDDVars(); + draDDColVars = new JDDVars(); + modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars); + mainLog.println(); + modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); + // Output product, if required + if (prism.getExportProductTrans()) { + try { + mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"..."); + modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename())); + } catch (FileNotFoundException e) { + mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\""); + } + } + if (prism.getExportProductStates()) { + mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"..."); + modelProduct.exportStates(Prism.EXPORT_PLAIN, new PrismFileLog(prism.getExportProductStatesFilename())); + } + + // Find accepting MECs + compute reachability probabilities + mainLog.println("\nFinding accepting end components..."); + JDDNode acc = mcLtl.findAcceptingECStatesForRabin(dra, modelProduct, draDDRowVars, draDDColVars, fairness); + mainLog.println("\nComputing reachability probabilities..."); + mcProduct = new NondetModelChecker(prism, modelProduct, null); + probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); + + // subtract from 1 if we're model checking a negated formula for regular Pmin + if (min && !fairness) { + probsProduct.subtractFromOne(); + } + + // Convert probability vector to original model + // First, filter over DRA start states + startMask = mcLtl.buildStartMask(dra, labelDDs, draDDRowVars); + JDD.Ref(model.getReach()); + startMask = JDD.And(model.getReach(), startMask); + probsProduct.filter(startMask); + // Then sum over DD vars for the DRA state + probs = probsProduct.sumOverDDVars(draDDRowVars, model); + // Deref, clean up + probsProduct.clear(); + modelProduct.clear(); + for (i = 0; i < labelDDs.size(); i++) { + JDD.Deref(labelDDs.get(i)); + } + JDD.Deref(acc); + JDD.Deref(startMask); + draDDRowVars.derefAll(); + draDDColVars.derefAll(); + + return probs; + } + + /** + * Compute rewards for a cumulative reward operator. + */ protected StateValues checkRewardCumul(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException { int time; // time @@ -1624,8 +1637,9 @@ public class NondetModelChecker extends NonProbModelChecker return rewards; } - // inst reward - + /** + * Compute rewards for an instantaneous reward operator. + */ protected StateValues checkRewardInst(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException { int time; // time bound @@ -1643,8 +1657,9 @@ public class NondetModelChecker extends NonProbModelChecker return rewards; } - // reach reward - + /** + * Compute rewards for a reachability reward operator. + */ protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException { JDDNode b;