diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index cb770cf8..f14e9d29 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -42,30 +42,29 @@ public class LTLModelChecker { protected Prism prism; protected PrismLog mainLog; - protected ModelChecker parent; // DRA/product stuff protected JDDVars draDDRowVars; protected JDDVars draDDColVars; - public LTLModelChecker(Prism prism, ModelChecker parent) throws PrismException + public LTLModelChecker(Prism prism) throws PrismException { this.prism = prism; mainLog = prism.getMainLog(); - this.parent = parent; } - /* Extract maximal state formula from an LTL path formula, model check them (with - * parent model checker) and replace them with ExpressionLabel objects L0, L1, etc. - * As an optimisation, model checking that results in true/false for all states is - * converted to an actual true/false, and duplicate results are given the same label. + /** + * Extract maximal state formula from an LTL path formula, model check them (with passed in model checker) and + * replace them with ExpressionLabel objects L0, L1, etc. Expression passed in is modified directly, but the result + * is also returned. As an optimisation, model checking that results in true/false for all states is converted to an + * actual true/false, and duplicate results are given the same label. */ - public Expression checkMaximalStateFormulas(Model model, Expression expr, Vector labelDDs) + public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector labelDDs) throws PrismException { // A state formula if (expr.getType() == Expression.BOOLEAN) { // Model check - JDDNode dd = parent.checkExpressionDD(expr); + JDDNode dd = mc.checkExpressionDD(expr); // Detect special cases (true, false) for optimisation if (dd.equals(JDD.ZERO)) { JDD.Deref(dd); @@ -82,7 +81,7 @@ public class LTLModelChecker JDD.Deref(dd); return new ExpressionLabel("L" + i); } - // Otherwise, add result to list, return new label + // Otherwise, add result to list, return new label labelDDs.add(dd); return new ExpressionLabel("L" + (labelDDs.size() - 1)); } @@ -90,25 +89,28 @@ public class LTLModelChecker else if (expr.getType() == Expression.PATH_BOOLEAN) { if (expr instanceof ExpressionBinaryOp) { ExpressionBinaryOp exprBinOp = (ExpressionBinaryOp) expr; - exprBinOp.setOperand1(checkMaximalStateFormulas(model, exprBinOp.getOperand1(), labelDDs)); - exprBinOp.setOperand2(checkMaximalStateFormulas(model, exprBinOp.getOperand2(), labelDDs)); + exprBinOp.setOperand1(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand1(), labelDDs)); + exprBinOp.setOperand2(checkMaximalStateFormulas(mc, model, exprBinOp.getOperand2(), labelDDs)); } else if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp exprUnOp = (ExpressionUnaryOp) expr; - exprUnOp.setOperand(checkMaximalStateFormulas(model, exprUnOp.getOperand(), labelDDs)); + exprUnOp.setOperand(checkMaximalStateFormulas(mc, model, exprUnOp.getOperand(), labelDDs)); } else if (expr instanceof ExpressionTemporal) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr; if (exprTemp.getOperand1() != null) { - exprTemp.setOperand1(checkMaximalStateFormulas(model, exprTemp.getOperand1(), labelDDs)); + exprTemp.setOperand1(checkMaximalStateFormulas(mc, model, exprTemp.getOperand1(), labelDDs)); } if (exprTemp.getOperand2() != null) { - exprTemp.setOperand2(checkMaximalStateFormulas(model, exprTemp.getOperand2(), labelDDs)); + exprTemp.setOperand2(checkMaximalStateFormulas(mc, model, exprTemp.getOperand2(), labelDDs)); } } } return expr; } - public NondetModel constructProductModel(DRA dra, Model model, Vector labelDDs) throws PrismException + /** + * Construct product of DRA and DTMC/CTMC. + */ + public ProbModel constructProductMC(DRA dra,ProbModel model, Vector labelDDs) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -143,10 +145,10 @@ public class LTLModelChecker } // See how many new dd vars will be needed for DRA - // and whether there is room to put them before rather than after the existing vars + // and whether there is room to put them before rather than after the existing vars n = (int) Math.ceil(PrismUtils.log2(dra.size())); before = true; - if ((allDDRowVars.getMinVarIndex() - ((NondetModel) model).getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { + if (allDDRowVars.getMinVarIndex() - 1 < 2 * n) { before = false; } @@ -195,7 +197,6 @@ public class LTLModelChecker newVarList.addVar(before ? 0 : varList.getNumVars(), draVar, 0, dra.size() - 1, 0, 1, Expression.INT); // Extra references (because will get derefed when new model is done with) - // TODO: tidy this up, make it corresond to model.clear() allDDRowVars.refAll(); allDDRowVars.refAll(); allDDColVars.refAll(); @@ -206,17 +207,167 @@ public class LTLModelChecker } draDDRowVars.refAll(); draDDColVars.refAll(); - ((NondetModel) model).getAllDDSchedVars().refAll(); - ((NondetModel) model).getAllDDSynchVars().refAll(); - ((NondetModel) model).getAllDDChoiceVars().refAll(); - ((NondetModel) model).getAllDDNondetVars().refAll(); + // Build transition matrix for product newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars); JDD.Ref(model.getTrans()); newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); - - // Note: ... TODO - newStart = buildStartMask(dra, labelDDs); + + // Build set of initial states for product + // Note that we take product of *all* states of the original MDP, not just its initial states. + // Initial states are only used for reachability in this instance. + // We need to ensure that the product model includes states corresponding to all + // states of the original MDP (because we compute probabilities for all of them) + // but some of these may not be reachable from the initial state of the product model. + newStart = buildStartMask(dra, labelDDs, draDDRowVars); + JDD.Ref(model.getReach()); + newStart = JDD.And(model.getReach(), newStart); + + // Create a new model model object to store the product model + ProbModel modelProd = new ProbModel( + // New transition matrix/start state + newTrans, newStart, + // Don't pass in any rewards info + new JDDNode[0], new JDDNode[0], new String[0], + // New list of all row/col vars + newAllDDRowVars, newAllDDColVars, + // New list of var names + newDDVarNames, + // Module info (unchanged) + model.getNumModules(), model.getModuleNames(), model.getModuleDDRowVars(), model.getModuleDDColVars(), + // New var info + model.getNumVars() + 1, newVarList, newVarDDRowVars, newVarDDColVars, + // Constants (no change) + model.getConstantValues()); + + // Do reachability/etc. for the new model + modelProd.doReachability(prism.getExtraReachInfo()); + modelProd.filterReachableStates(); + modelProd.findDeadlocks(); + if (modelProd.getDeadlockStates().size() > 0) { + throw new PrismException("Model-DRA product has deadlock states"); + } + + return modelProd; + } + + /** + * Construct product of DRA and MDP. + */ + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs) throws PrismException + { + // Existing model - dds, vars, etc. + JDDVars varDDRowVars[]; + JDDVars varDDColVars[]; + JDDVars allDDRowVars; + JDDVars allDDColVars; + Vector ddVarNames; + VarList varList; + // New (product) model - dds, vars, etc. + JDDNode newTrans, newStart; + JDDVars newVarDDRowVars[], newVarDDColVars[]; + JDDVars newAllDDRowVars, newAllDDColVars; + Vector newDDVarNames; + VarList newVarList; + String draVar; + // Misc + int i, j, n; + boolean before; + + // Get details of old model + varDDRowVars = model.getVarDDRowVars(); + varDDColVars = model.getVarDDColVars(); + allDDRowVars = model.getAllDDRowVars(); + allDDColVars = model.getAllDDColVars(); + ddVarNames = model.getDDVarNames(); + varList = model.getVarList(); + + // Create a (new, unique) name for the variable that will represent DRA states + draVar = "_dra"; + while (varList.getIndex(draVar) != -1) { + draVar = "_" + draVar; + } + + // See how many new dd vars will be needed for DRA + // and whether there is room to put them before rather than after the existing vars + n = (int) Math.ceil(PrismUtils.log2(dra.size())); + before = true; + if ((allDDRowVars.getMinVarIndex() - model.getAllDDNondetVars().getMaxVarIndex()) - 1 < 2 * n) { + before = false; + } + + // Create the new dd variables + draDDRowVars = new JDDVars(); + draDDColVars = new JDDVars(); + newDDVarNames = new Vector(); + newDDVarNames.addAll(ddVarNames); + j = before ? allDDRowVars.getMinVarIndex() - 2 * n : model.getAllDDColVars().getMaxVarIndex() + 1; + for (i = 0; i < n; i++) { + draDDRowVars.addVar(JDD.Var(j++)); + draDDColVars.addVar(JDD.Var(j++)); + if (!before) { + newDDVarNames.add(""); + newDDVarNames.add(""); + } + newDDVarNames.set(j - 2, draVar + "." + i); + newDDVarNames.set(j - 1, draVar + "'." + i); + } + + // Create/populate new lists + newVarDDRowVars = new JDDVars[varDDRowVars.length + 1]; + newVarDDColVars = new JDDVars[varDDRowVars.length + 1]; + newVarDDRowVars[before ? 0 : varDDRowVars.length] = draDDRowVars; + newVarDDColVars[before ? 0 : varDDColVars.length] = draDDColVars; + for (i = 0; i < varDDRowVars.length; i++) { + newVarDDRowVars[before ? i + 1 : i] = new JDDVars(); + newVarDDColVars[before ? i + 1 : i] = new JDDVars(); + newVarDDRowVars[before ? i + 1 : i].addVars(varDDRowVars[i]); + newVarDDColVars[before ? i + 1 : i].addVars(varDDColVars[i]); + } + newAllDDRowVars = new JDDVars(); + newAllDDColVars = new JDDVars(); + if (before) { + newAllDDRowVars.addVars(draDDRowVars); + newAllDDColVars.addVars(draDDColVars); + newAllDDRowVars.addVars(allDDRowVars); + newAllDDColVars.addVars(allDDColVars); + } else { + newAllDDRowVars.addVars(allDDRowVars); + newAllDDColVars.addVars(allDDColVars); + newAllDDRowVars.addVars(draDDRowVars); + newAllDDColVars.addVars(draDDColVars); + } + newVarList = (VarList) varList.clone(); + newVarList.addVar(before ? 0 : varList.getNumVars(), draVar, 0, dra.size() - 1, 0, 1, Expression.INT); + + // Extra references (because will get derefed when new model is done with) + allDDRowVars.refAll(); + allDDRowVars.refAll(); + allDDColVars.refAll(); + allDDColVars.refAll(); + for (i = 0; i < model.getNumModules(); i++) { + model.getModuleDDRowVars(i).refAll(); + model.getModuleDDColVars(i).refAll(); + } + draDDRowVars.refAll(); + draDDColVars.refAll(); + model.getAllDDSchedVars().refAll(); + model.getAllDDSynchVars().refAll(); + model.getAllDDChoiceVars().refAll(); + model.getAllDDNondetVars().refAll(); + + // Build transition matrix for product + newTrans = buildTransMask(dra, labelDDs, allDDRowVars, allDDColVars, draDDRowVars, draDDColVars); + JDD.Ref(model.getTrans()); + newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); + + // Build set of initial states for product + // Note that we take product of *all* states of the original MDP, not just its initial states. + // Initial states are only used for reachability in this instance. + // We need to ensure that the product model includes states corresponding to all + // states of the original MDP (because we compute probabilities for all of them) + // but some of these may not be reachable from the initial state of the product model. + newStart = buildStartMask(dra, labelDDs, draDDRowVars); JDD.Ref(model.getReach()); newStart = JDD.And(model.getReach(), newStart); @@ -229,8 +380,7 @@ public class LTLModelChecker // New list of all row/col vars newAllDDRowVars, newAllDDColVars, // Nondet variables (unchanged) - ((NondetModel) model).getAllDDSchedVars(), ((NondetModel) model).getAllDDSynchVars(), - ((NondetModel) model).getAllDDChoiceVars(), ((NondetModel) model).getAllDDNondetVars(), + model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model.getAllDDNondetVars(), // New list of var names newDDVarNames, // Module info (unchanged) @@ -251,14 +401,14 @@ public class LTLModelChecker return modelProd; } - /** - * Builds a mask BDD for trans (which contains transitions between every - * DRA state after adding draRow/Colvars) that includes only the transitions - * that exist in the DRA. - * @return a referenced mask BDD over trans + /** + * Builds a mask BDD for trans (which contains transitions between every DRA state after adding draRow/ColVars) that + * includes only the transitions that exist in the DRA. + * + * @return a referenced mask BDD over trans */ - public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, - JDDVars draDDRowVars, JDDVars draDDColVars) + public JDDNode buildTransMask(DRA dra, Vector labelDDs, JDDVars allDDRowVars, JDDVars allDDColVars, JDDVars draDDRowVars, + JDDVars draDDColVars) { Iterator it; DA_State state; @@ -271,7 +421,8 @@ public class LTLModelChecker state = it.next(); for (Map.Entry edge : state.edges().entrySet()) { // Build a transition label BDD for each edge - //System.out.println(state.getName() + " to " + edge.getValue().getName() + " through " + edge.getKey().toString(dra.getAPSet(), false)); + // System.out.println(state.getName() + " to " + edge.getValue().getName() + " through " + + // edge.getKey().toString(dra.getAPSet(), false)); label = JDD.Constant(1); n = dra.getAPSize(); for (i = 0; i < n; i++) { @@ -286,8 +437,8 @@ public class LTLModelChecker // Switch label BDD to col vars label = JDD.PermuteVariables(label, allDDRowVars, allDDColVars); // Build a BDD for the edge - transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge - .getValue().getName(), 1); + transition = JDD.SetMatrixElement(JDD.Constant(0), draDDRowVars, draDDColVars, state.getName(), edge.getValue().getName(), + 1); // Now get the conjunction of the two transition = JDD.And(transition, label); // Add edge BDD to the DRA transition mask @@ -298,20 +449,21 @@ public class LTLModelChecker return draMask; } - /** - * Builds a mask BDD for start (which contains start nodes for every - * DRA state after adding draRow/ColVars) that includes only the start states - * (s, q) such that q = delta(q_in, label(s)) in the DRA. - * @return a referenced mask BDD over start + /** + * Builds a mask BDD for start (which contains start nodes for every DRA state after adding draRowVars) that + * includes only the start states (s, q) such that q = delta(q_in, label(s)) in the DRA. + * + * @return a referenced mask BDD over start */ - public JDDNode buildStartMask(DRA dra, Vector labelDDs) + public JDDNode buildStartMask(DRA dra, Vector labelDDs, JDDVars draDDRowVars) { JDDNode startMask, label, exprBDD, dest, tmp; startMask = JDD.Constant(0); for (Map.Entry edge : dra.getStartState().edges().entrySet()) { // Build a transition label BDD for each edge - //System.out.println("To " + edge.getValue().getName() + " through " + edge.getKey().toString(dra.getAPSet(), false)); + // System.out.println("To " + edge.getValue().getName() + " through " + + // edge.getKey().toString(dra.getAPSet(), false)); label = JDD.Constant(1); for (int i = 0; i < dra.getAPSize(); i++) { exprBDD = labelDDs.get(Integer.parseInt(dra.getAPSet().getAP(i).substring(1))); @@ -334,31 +486,105 @@ public class LTLModelChecker return startMask; } - + /** - * computes sets of accepting states for each Rabin acceptance pair + * Computes sets of accepting states in a DTMC/CTMC for each Rabin acceptance pair * * @returns a referenced BDD of the union of all the accepting sets - */ - public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException { + */ + public JDDNode findAcceptingBSCCs(DRA dra, ProbModel model) throws PrismException + { + SCCComputer sccComputer ; + JDDNode acceptingStates, allAcceptingStates; + Vector vectBSCCs, newVectBSCCs; + JDDNode tmp; + int i, j, n; + + // Compute BSCCs for model + sccComputer = prism.getSCCComputer(model); + sccComputer.computeBSCCs(); + vectBSCCs = sccComputer.getVectBSCCs(); + JDD.Deref(sccComputer.getNotInBSCCs()); + + allAcceptingStates = JDD.Constant(0); + + // for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i + // and compute the BSCCs in H'_i + for (i = 0; i < dra.acceptance().size(); i++) { - JDDNode allAcceptingStates = JDD.Constant(0); + // build the acceptance vectors H_i and L_i + JDDNode acceptanceVector_H = JDD.Constant(0); + JDDNode acceptanceVector_L = JDD.Constant(0); + for (j = 0; j < dra.size(); j++) { + /* + * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that H_i contains Inf(ρ) The intersection of + * Inf(ρ) and L_i is non-empty + * + * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and + * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty + */ + if (!dra.acceptance().isStateInAcceptance_U(i, j)) { + acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0); + } + if (dra.acceptance().isStateInAcceptance_L(i, j)) { + acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); + } + } + + // Restrict each BSCC to H_i states + n = vectBSCCs.size(); + newVectBSCCs = new Vector(); + for (j = 0; j < n; j++) { + tmp = vectBSCCs.get(j); + JDD.Ref(tmp); + JDD.Ref(acceptanceVector_H); + tmp = JDD.And(tmp, acceptanceVector_H); + newVectBSCCs.add(tmp); + } + JDD.Deref(acceptanceVector_H); + + // Compute union of BSCCs which overlap with acceptanceVector_L + acceptingStates = filteredUnion(newVectBSCCs, acceptanceVector_L); + + // Add states to our destination BDD + allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); + } + + // Deref BSCCs + n = vectBSCCs.size(); + for (j = 0; j < n; j++) { + JDD.Deref(vectBSCCs.get(j)); + } + + return allAcceptingStates; + } + + /** + * Computes sets of accepting states in an MDP for each Rabin acceptance pair + * + * @returns a referenced BDD of the union of all the accepting sets + */ + public JDDNode findAcceptingStates(DRA dra, NondetModel model, boolean fairness) throws PrismException + { + JDDNode acceptingStates, allAcceptingStates; + int i, j; + + allAcceptingStates = JDD.Constant(0); // for each acceptance pair (H_i, L_i) in the DRA, build H'_i = S x H_i // and compute the maximal ECs in H'_i - for (int i = 0; i < dra.acceptance().size(); i++) { + for (i = 0; i < dra.acceptance().size(); i++) { // build the acceptance vectors H_i and L_i JDDNode acceptanceVector_H = JDD.Constant(0); JDDNode acceptanceVector_L = JDD.Constant(0); - for (int j = 0; j < dra.size(); j++) { - /* [dA97] uses Rabin acceptance pairs (H_i, L_i) such that - * H_i contains Inf(ρ) - * The intersection of Inf(ρ) and L_i is non-empty - * - * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that - * The intersection of U_i and Inf(ρ) is empty (H_i = S - U_i) - * The intersection of L_i and Inf(ρ) is non-empty + for (j = 0; j < dra.size(); j++) { + /* + * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that H_i contains Inf(ρ) The intersection of + * Inf(ρ) and L_i is non-empty + * + * OTOH ltl2dstar (and our port to java) uses pairs (L_i, U_i) such that The intersection of U_i and + * Inf(ρ) is empty (H_i = S - U_i) The intersection of L_i and Inf(ρ) is non-empty */ if (!dra.acceptance().isStateInAcceptance_U(i, j)) { acceptanceVector_H = JDD.SetVectorElement(acceptanceVector_H, draDDRowVars, j, 1.0); @@ -367,7 +593,7 @@ public class LTLModelChecker acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); } } - + // build bdd of accepting states (under H_i) in the product model JDD.Ref(model.getTrans01()); JDD.Ref(acceptanceVector_H); @@ -376,8 +602,7 @@ public class LTLModelChecker candidateStates = JDD.Apply(JDD.TIMES, candidateStates, acceptanceVector_H); candidateStates = JDD.ThereExists(candidateStates, model.getAllDDColVars()); candidateStates = JDD.ThereExists(candidateStates, model.getAllDDNondetVars()); - - JDDNode acceptingStates; + if (fairness) { // compute the backward set of S x L_i JDD.Ref(candidateStates); @@ -385,40 +610,42 @@ public class LTLModelChecker JDD.Ref(model.getTrans01()); JDDNode edges = JDD.ThereExists(model.getTrans01(), model.getAllDDNondetVars()); JDDNode filterStates = backwardSet(model, tmp, edges); - + // Filter out states that can't reach a state in L'_i candidateStates = JDD.And(candidateStates, filterStates); - + // Find accepting states in S x H_i - acceptingStates = findFairECs(model, candidateStates); - } - else { + acceptingStates = findFairECs(model, candidateStates); + } else { // find ECs in acceptingStates that are accepting under L_i acceptingStates = filteredUnion(findEndComponents(model, candidateStates), acceptanceVector_L); } - + // Add states to our destination BDD allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); } + return allAcceptingStates; } - - /** + + /** * Returns all end components in candidateStates under fairness assumptions - * @param candidateStates set of candidate states S x H_i - * (dereferenced after calling this function) - * @return a referenced BDD with the maximal stable set in c + * + * @param candidateStates + * set of candidate states S x H_i (dereferenced after calling this function) + * @return a referenced BDD with the maximal stable set in c */ - private JDDNode findFairECs(NondetModel model, JDDNode candidateStates) { - + private JDDNode findFairECs(NondetModel model, JDDNode candidateStates) + { + JDDNode old = JDD.Constant(0); JDDNode current = candidateStates; - + while (!current.equals(old)) { JDD.Deref(old); JDD.Ref(current); old = current; - + JDD.Ref(current); JDD.Ref(model.getTrans01()); // Select transitions starting in current @@ -436,11 +663,9 @@ public class LTLModelChecker JDD.Deref(old); return current; } - - /** - * Return the set of states that reach nodes through edges - * Refs: result - * Derefs: nodes, edges + + /** + * Return the set of states that reach nodes through edges Refs: result Derefs: nodes, edges */ private JDDNode backwardSet(NondetModel model, JDDNode nodes, JDDNode edges) { @@ -458,11 +683,9 @@ public class LTLModelChecker JDD.Deref(old); return current; } - - /** - * Return the preimage of nodes in edges - * Refs: result - * Derefs: edges, nodes + + /** + * Return the preimage of nodes in edges Refs: result Derefs: edges, nodes */ // FIXME: Refactor this out (duplicated in SCCComputers) private JDDNode preimage(NondetModel model, JDDNode nodes, JDDNode edges) @@ -476,34 +699,37 @@ public class LTLModelChecker tmp = JDD.ThereExists(tmp, model.getAllDDColVars()); return tmp; } - + /** * Computes maximal accepting end components in states - * @param states BDD of a set of states (dereferenced after calling this function) - * @return a vector of referenced BDDs containing all the ECs in states + * + * @param states + * BDD of a set of states (dereferenced after calling this function) + * @return a vector of referenced BDDs containing all the ECs in states */ - private Vector findEndComponents(NondetModel model, JDDNode states) throws PrismException { - + private Vector findEndComponents(NondetModel model, JDDNode states) throws PrismException + { + boolean initialCandidate = true; Stack candidates = new Stack(); candidates.push(states); Vector ecs = new Vector(); SCCComputer sccComputer; - + while (!candidates.isEmpty()) { JDDNode candidate = candidates.pop(); - + // Compute the stable set JDD.Ref(candidate); JDDNode stableSet = findMaximalStableSet(model, candidate); - + // Drop empty sets if (stableSet.equals(JDD.ZERO)) { JDD.Deref(stableSet); JDD.Deref(candidate); continue; } - + if (!initialCandidate) { // candidate is an SCC, check if it's stable if (stableSet.equals(candidate)) { @@ -511,45 +737,46 @@ public class LTLModelChecker JDD.Deref(stableSet); continue; } - } - else { + } else { initialCandidate = false; } JDD.Deref(candidate); - + // Filter bad transitions JDD.Ref(stableSet); JDDNode stableSetTrans = maxStableSetTrans(model, stableSet); - + // now find the maximal SCCs in (stableSet, stableSetTrans) Vector sccs; sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars()); - sccComputer.computeBSCCs(); + sccComputer.computeSCCs(); JDD.Deref(stableSet); JDD.Deref(stableSetTrans); - sccs = sccComputer.getVectBSCCs(); - JDD.Deref(sccComputer.getNotInBSCCs()); + sccs = sccComputer.getVectSCCs(); + JDD.Deref(sccComputer.getNotInSCCs()); candidates.addAll(sccs); } return ecs; } - - /** + + /** * Returns a stable set of states contained in candidateStates - * @param candidateStates set of candidate states S x H_i - * (dereferenced after calling this function) - * @return a referenced BDD with the maximal stable set in c + * + * @param candidateStates + * set of candidate states S x H_i (dereferenced after calling this function) + * @return a referenced BDD with the maximal stable set in c */ - private JDDNode findMaximalStableSet(NondetModel model, JDDNode candidateStates) { - + private JDDNode findMaximalStableSet(NondetModel model, JDDNode candidateStates) + { + JDDNode old = JDD.Constant(0); JDDNode current = candidateStates; - + while (!current.equals(old)) { JDD.Deref(old); JDD.Ref(current); old = current; - + JDD.Ref(current); JDD.Ref(model.getTrans()); // Select transitions starting in current @@ -568,13 +795,16 @@ public class LTLModelChecker JDD.Deref(old); return current; } - + /** * Returns the transition relation of a stable set - * @param b BDD of a stable set (dereferenced after calling this function) - * @return referenced BDD of the transition relation restricted to the stable set + * + * @param b + * BDD of a stable set (dereferenced after calling this function) + * @return referenced BDD of the transition relation restricted to the stable set */ - private JDDNode maxStableSetTrans(NondetModel model, JDDNode b) { + private JDDNode maxStableSetTrans(NondetModel model, JDDNode b) + { JDD.Ref(b); JDD.Ref(model.getTrans()); @@ -596,12 +826,14 @@ public class LTLModelChecker } /** - * Returns the union of each set in the vector that has nonempty intersection - * with the filter BDD. - * @param sets Vector with sets which are dereferenced after calling this function - * @param filter filter BDD against which each set is checked for nonempty intersection - * also dereferenced after calling this function - * @return Referenced BDD with the filtered union + * Returns the union of each set in the vector that has nonempty intersection with the filter BDD. + * + * @param sets + * Vector with sets which are dereferenced after calling this function + * @param filter + * filter BDD against which each set is checked for nonempty intersection also dereferenced after calling + * this function + * @return Referenced BDD with the filtered union */ private JDDNode filteredUnion(Vector sets, JDDNode filter) { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 60a022a5..0ccd2779 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -400,13 +400,15 @@ public class NondetModelChecker extends NonProbModelChecker } // For LTL model checking routines - mcLtl = new LTLModelChecker(prism, this); + mcLtl = new LTLModelChecker(prism); // Model check maximal state formulas labelDDs = new Vector(); - ltl = mcLtl.checkMaximalStateFormulas(model, expr.deepCopy(), labelDDs); + 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) mainLog.println("\nBuilding deterministic Rabin automaton (for " + (min && !fairness ? "!" : "") + ltl + ")..."); l = System.currentTimeMillis(); if (min && !fairness) { @@ -414,22 +416,24 @@ public class NondetModelChecker extends NonProbModelChecker } else { dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); } - mainLog.println("\nDRA has " + dra.size() + " states."); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs."); // dra.print(System.out); l = System.currentTimeMillis() - l; mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); // Build product of MDP and automaton - mainLog.println("\nConstructing Model-DRA product..."); - modelProduct = mcLtl.constructProductModel(dra, model, labelDDs); + mainLog.println("\nConstructing MDP-DRA product..."); + modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null); // prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null); + // Find accepting maximum end components mainLog.println("\nFinding accepting end components..."); JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness); + // Compute reachability probabilities mainLog.println("\nComputing reachability probabilities..."); mcProduct = new NondetModelChecker(prism, modelProduct, null); probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual, min && fairness); @@ -441,9 +445,10 @@ public class NondetModelChecker extends NonProbModelChecker // Convert probability vector to original model // First, filter over DRA start states - startMask = mcLtl.buildStartMask(dra, labelDDs); + // (which we can get from initial states of product model, + // because of the way it is constructed) + startMask = modelProduct.getStart(); probsProduct.filter(startMask); - JDD.Deref(startMask); // Then sum over DD vars for the DRA state draDDRowVars = new JDDVars(); draDDRowVars.addVars(modelProduct.getAllDDRowVars()); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index f90deaf0..55aba0ad 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -29,19 +29,22 @@ package prism; import java.util.Vector; import jdd.*; +import jltl2dstar.DRA; +import jltl2dstar.LTL2Rabin; import dv.*; import mtbdd.*; import sparse.*; import hybrid.*; import parser.ast.*; +import parser.visitor.ASTTraverse; /* * Model checker for DTMCs. */ public class ProbModelChecker extends NonProbModelChecker { - // SCC computer - protected SCCComputer sccComputer; + // Model (DTMC or CTMC) + protected ProbModel model; // Options (in addition to those inherited from StateModelChecker): @@ -56,9 +59,10 @@ public class ProbModelChecker extends NonProbModelChecker { // Initialise super(prism, m, pf); - - // Create SCCComputer object - sccComputer = prism.getSCCComputer(m); + if (!(m instanceof ProbModel)) { + throw new PrismException("Wrong model type passed to ProbModelChecker."); + } + model = (ProbModel) m; // Inherit some options from parent Prism object. // Store locally and/or pass onto engines. @@ -96,6 +100,13 @@ public class ProbModelChecker extends NonProbModelChecker } } + // Override-able "Constructor" + + public ProbModelChecker createNewModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismException + { + return new ProbModelChecker(prism, m, pf); + } + // ----------------------------------------------------------------------------------- // Check a property, i.e. an expression // ----------------------------------------------------------------------------------- @@ -350,6 +361,7 @@ public class ProbModelChecker extends NonProbModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { + SCCComputer sccComputer = prism.getSCCComputer(model); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); @@ -512,7 +524,8 @@ public class ProbModelChecker extends NonProbModelChecker if (expr.isSimplePathFormula()) { return checkProbPathFormulaSimple(expr, qual); } else { - throw new PrismException("LTL-style path formulas are not yet supported"); + return checkProbPathFormulaLTL(expr, qual); + //throw new PrismException("LTL-style path formulas are not yet supported"); } } @@ -562,6 +575,97 @@ public class ProbModelChecker extends NonProbModelChecker return probs; } + // LTL-like path formula for P operator + + protected StateProbs checkProbPathFormulaLTL(Expression expr, boolean qual) throws PrismException + { + LTLModelChecker mcLtl; + StateProbs probsProduct = null, probs = null; + Expression ltl; + Vector labelDDs; + DRA dra; + ProbModel modelProduct; + ProbModelChecker mcProduct; + JDDNode startMask; + JDDVars draDDRowVars; + 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); + } + + // 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) + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + l = System.currentTimeMillis(); + dra = LTL2Rabin.ltl2rabin(ltl.convertForJltl2ba()); + mainLog.println("\nDRA has " + dra.size() + " states, " + dra.acceptance().size() + " pairs."); + // dra.print(System.out); + l = System.currentTimeMillis() - l; + mainLog.println("\nTime for Rabin translation: " + l / 1000.0 + " seconds."); + + // Build product of Markov chain and automaton + // (note: might be a CTMC - StochModelChecker extends this class) + mainLog.println("\nConstructing MC-DRA product..."); + modelProduct = mcLtl.constructProductMC(dra, model, labelDDs); + mainLog.println(); + modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); + // prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null); + // prism.exportTransToFile(modelProduct, true, Prism.EXPORT_PLAIN, null); + + // Find accepting maximum end BSCC + mainLog.println("\nFinding accepting BSCCs..."); + JDDNode acc = mcLtl.findAcceptingBSCCs(dra, modelProduct); + + // Compute reachability probabilities + mainLog.println("\nComputing reachability probabilities..."); + mcProduct = createNewModelChecker(prism, modelProduct, null); + probsProduct = mcProduct.checkProbUntil(modelProduct.getReach(), acc, qual); + + // Convert probability vector to original model + // First, filter over DRA start states + // (which we can get from initial states of product model, + // because of the way it is constructed) + startMask = modelProduct.getStart(); + probsProduct.filter(startMask); + // Then sum over DD vars for the DRA state + draDDRowVars = new JDDVars(); + draDDRowVars.addVars(modelProduct.getAllDDRowVars()); + draDDRowVars.removeVars(allDDRowVars); + 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); + + return probs; + } + // next protected StateProbs checkProbNext(ExpressionTemporal expr) throws PrismException @@ -640,6 +744,8 @@ public class ProbModelChecker extends NonProbModelChecker // until (unbounded) + // this method is split into two steps so that the LTL model checker can use the second part directly + protected StateProbs checkProbUntil(ExpressionTemporal expr, boolean qual) throws PrismException { JDDNode b1, b2; @@ -660,6 +766,27 @@ public class ProbModelChecker extends NonProbModelChecker // mainLog.print(" states, b2 = " + JDD.GetNumMintermsString(b2, // allDDRowVars.n()) + " states\n"); + try { + probs = checkProbUntil(b1, b2, qual); + } catch (PrismException e) { + JDD.Deref(b1); + JDD.Deref(b2); + throw e; + } + + // derefs + JDD.Deref(b1); + JDD.Deref(b2); + + return probs; + } + + // until (unbounded): b1/b2 are bdds for until operands + + protected StateProbs checkProbUntil(JDDNode b1, JDDNode b2, boolean qual) throws PrismException + { + StateProbs probs = null; + // compute probabilities // if requested (i.e. when prob bound is 0 or 1 and precomputation algorithms are enabled), @@ -671,19 +798,9 @@ public class ProbModelChecker extends NonProbModelChecker } // otherwise actually compute probabilities else { - try { - probs = computeUntilProbs(trans, trans01, b1, b2); - } catch (PrismException e) { - JDD.Deref(b1); - JDD.Deref(b2); - throw e; - } + probs = computeUntilProbs(trans, trans01, b1, b2); } - // derefs - JDD.Deref(b1); - JDD.Deref(b2); - return probs; } @@ -795,6 +912,7 @@ public class ProbModelChecker extends NonProbModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { + SCCComputer sccComputer = prism.getSCCComputer(model); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); @@ -940,6 +1058,7 @@ public class ProbModelChecker extends NonProbModelChecker // compute bottom strongly connected components (bsccs) if (bsccComp) { + SCCComputer sccComputer = prism.getSCCComputer(model); sccComputer.computeBSCCs(); vectBSCCs = sccComputer.getVectBSCCs(); notInBSCCs = sccComputer.getNotInBSCCs(); diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index ca8201c2..f4e78aff 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -63,6 +63,13 @@ public class StochModelChecker extends ProbModelChecker super(prism, m, pf); } + // Override-able "Constructor" + + public ProbModelChecker createNewModelChecker(Prism prism, Model m, PropertiesFile pf) throws PrismException + { + return new StochModelChecker(prism, m, pf); + } + // ----------------------------------------------------------------------------------- // Check method for each operator // -----------------------------------------------------------------------------------