From 3bdca763eba1a7b7f0cbed6dad0ccade1e206a52 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 15 Dec 2009 12:38:14 +0000 Subject: [PATCH] LTL model checking code: code tidy and clean-up. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1652 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 135 +++++++++++++++++------- prism/src/prism/NondetModelChecker.java | 13 +-- prism/src/prism/ProbModelChecker.java | 13 +-- 3 files changed, 110 insertions(+), 51 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index caf5fcb8..54ff8a81 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -43,9 +43,6 @@ public class LTLModelChecker { protected Prism prism; protected PrismLog mainLog; - // DRA/product stuff - protected JDDVars draDDRowVars; - protected JDDVars draDDColVars; public LTLModelChecker(Prism prism) throws PrismException { @@ -57,7 +54,8 @@ public class LTLModelChecker * 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. + * actual true/false, and duplicate results are given the same label. BDDs giving the states which satisfy each label + * are put into the vector labelDDs, which should be empty when this function is called. */ public Expression checkMaximalStateFormulas(ModelChecker mc, Model model, Expression expr, Vector labelDDs) throws PrismException @@ -113,21 +111,37 @@ public class LTLModelChecker * @param dra: The DRA * @param model: The DTMC/CTMC * @param labelDDs: BDDs giving the set of states for each AP in the DRA - * @param allInit: Do we assume that all states of the original model are initial states (see below) */ - public ProbModel constructProductMC(DRA dra,ProbModel model, Vector labelDDs) throws PrismException + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs) throws PrismException { - return constructProductMC(dra, model, labelDDs, true); + return constructProductMC(dra, model, labelDDs, null, null, true); } - + + /** + * Construct product of DRA and DTMC/CTMC. + * @param dra: The DRA + * @param model: The DTMC/CTMC + * @param labelDDs: BDDs giving the set of states for each AP in the DRA + * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA + * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + */ + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, + JDDVars draDDColVarsCopy) throws PrismException + { + return constructProductMC(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true); + } + /** * Construct product of DRA and DTMC/CTMC. * @param dra: The DRA * @param model: The DTMC/CTMC * @param labelDDs: BDDs giving the set of states for each AP in the DRA - * @param allInit: Do we assume that all states of the original model are initial states (see below) + * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA + * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + * @param allInit: Do we assume that all states of the original model are initial states? (see below) */ - public ProbModel constructProductMC(DRA dra,ProbModel model, Vector labelDDs, boolean allInit) throws PrismException + public ProbModel constructProductMC(DRA dra, ProbModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, + JDDVars draDDColVarsCopy, boolean allInit) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -143,6 +157,8 @@ public class LTLModelChecker Vector newDDVarNames; VarList newVarList; String draVar; + // DRA stuff + JDDVars draDDRowVars, draDDColVars; // Misc int i, j, n; boolean before; @@ -171,9 +187,11 @@ public class LTLModelChecker before = false; } + // If passed in var lists are null, create new lists + // (which won't be accessible later in this case) + draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy; + draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy; // 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; @@ -214,7 +232,8 @@ public class LTLModelChecker } newVarList = (VarList) varList.clone(); // NB: if DRA only has one state, we add an extra dummy state - Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1)))); + Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra + .size() - 1, 1)))); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); // Extra references (because will get derefed when new model is done with) @@ -247,7 +266,7 @@ public class LTLModelChecker // Create a new model model object to store the product model ProbModel modelProd = new ProbModel( - // New transition matrix/start state + // New transition matrix/start state newTrans, newStart, // Don't pass in any rewards info new JDDNode[0], new JDDNode[0], new String[0], @@ -270,6 +289,12 @@ public class LTLModelChecker throw new PrismException("Model-DRA product has deadlock states"); } + // Reference DRA DD vars (if being returned) + if (draDDRowVarsCopy != null) + draDDRowVarsCopy.refAll(); + if (draDDColVarsCopy != null) + draDDColVarsCopy.refAll(); + return modelProd; } @@ -281,7 +306,21 @@ public class LTLModelChecker */ public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs) throws PrismException { - return constructProductMDP(dra, model, labelDDs, true); + return constructProductMDP(dra, model, labelDDs, null, null, true); + } + + /** + * Construct product of DRA and MDP. + * @param dra: The DRA + * @param model: The MDP + * @param labelDDs: BDDs giving the set of states for each AP in the DRA + * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA + * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + */ + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, + JDDVars draDDColVarsCopy) throws PrismException + { + return constructProductMDP(dra, model, labelDDs, draDDRowVarsCopy, draDDColVarsCopy, true); } /** @@ -289,9 +328,12 @@ public class LTLModelChecker * @param dra: The DRA * @param model: The MDP * @param labelDDs: BDDs giving the set of states for each AP in the DRA - * @param allInit: Do we assume that all states of the original model are initial states (see below) + * @param draDDRowVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD row vars for DRA + * @param draDDColVarsCopy: (Optionally) empty JDDVars object to obtain copy of DD col vars for DRA + * @param allInit: Do we assume that all states of the original model are initial states? (see below) */ - public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, boolean allInit) throws PrismException + public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs, JDDVars draDDRowVarsCopy, + JDDVars draDDColVarsCopy, boolean allInit) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -307,6 +349,8 @@ public class LTLModelChecker Vector newDDVarNames; VarList newVarList; String draVar; + // DRA stuff + JDDVars draDDRowVars, draDDColVars; // Misc int i, j, n; boolean before; @@ -335,9 +379,11 @@ public class LTLModelChecker before = false; } + // If passed in var lists are null, create new lists + // (which won't be accessible later in this case) + draDDRowVars = (draDDRowVarsCopy == null) ? new JDDVars() : draDDRowVarsCopy; + draDDColVars = (draDDColVarsCopy == null) ? new JDDVars() : draDDColVarsCopy; // 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; @@ -378,7 +424,8 @@ public class LTLModelChecker } newVarList = (VarList) varList.clone(); // NB: if DRA only has one state, we add an extra dummy state - Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra.size() - 1, 1)))); + Declaration decl = new Declaration(draVar, new DeclarationInt(Expression.Int(0), Expression.Int(Math.max(dra + .size() - 1, 1)))); newVarList.addVar(before ? 0 : varList.getNumVars(), decl, 1, model.getConstantValues()); // Extra references (because will get derefed when new model is done with) @@ -415,14 +462,15 @@ public class LTLModelChecker // Create a new model model object to store the product model NondetModel modelProd = new NondetModel( - // New transition matrix/start state + // 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, // Nondet variables (unchanged) - model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model.getAllDDNondetVars(), + model.getAllDDSchedVars(), model.getAllDDSynchVars(), model.getAllDDChoiceVars(), model + .getAllDDNondetVars(), // New list of var names newDDVarNames, // Module info (unchanged) @@ -440,6 +488,12 @@ public class LTLModelChecker throw new PrismException("Model-DRA product has deadlock states"); } + // Reference DRA DD vars (if being returned) + if (draDDRowVarsCopy != null) + draDDRowVarsCopy.refAll(); + if (draDDColVarsCopy != null) + draDDColVarsCopy.refAll(); + return modelProd; } @@ -449,8 +503,8 @@ public class LTLModelChecker * * @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; @@ -479,8 +533,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 @@ -534,20 +588,21 @@ public class LTLModelChecker * * @returns a referenced BDD of the union of all the accepting sets */ - public JDDNode findAcceptingBSCCs(DRA dra, ProbModel model) throws PrismException + public JDDNode findAcceptingBSCCs(DRA dra, JDDVars draDDRowVars, JDDVars draDDColVars, ProbModel model) + throws PrismException { - SCCComputer sccComputer ; + SCCComputer sccComputer; JDDNode acceptingStates, allAcceptingStates; Vector vectBSCCs, newVectBSCCs; JDDNode tmp, tmp2; 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 @@ -572,7 +627,7 @@ public class LTLModelChecker acceptanceVector_L = JDD.SetVectorElement(acceptanceVector_L, draDDRowVars, j, 1.0); } } - + // Check each BSCC for inclusion in H_i states // i.e. restrict each BSCC to H_i states and test if unchanged n = vectBSCCs.size(); @@ -591,20 +646,20 @@ public class LTLModelChecker JDD.Deref(tmp2); } 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; } @@ -613,11 +668,12 @@ public class LTLModelChecker * * @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 findAcceptingStates(DRA dra, NondetModel model, JDDVars draDDRowVars, JDDVars draDDColVars, + 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 @@ -673,7 +729,7 @@ public class LTLModelChecker // Add states to our destination BDD allAcceptingStates = JDD.Or(allAcceptingStates, acceptingStates); } - + return allAcceptingStates; } @@ -797,7 +853,8 @@ public class LTLModelChecker // now find the maximal SCCs in (stableSet, stableSetTrans) Vector sccs; - sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model.getAllDDColVars()); + sccComputer = prism.getSCCComputer(stableSet, stableSetTrans, model.getAllDDRowVars(), model + .getAllDDColVars()); sccComputer.computeSCCs(); JDD.Deref(stableSet); JDD.Deref(stableSetTrans); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 54f5bc6e..2fb24913 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -382,7 +382,7 @@ public class NondetModelChecker extends NonProbModelChecker NondetModel modelProduct; NondetModelChecker mcProduct; JDDNode startMask; - JDDVars draDDRowVars; + JDDVars draDDRowVars, draDDColVars; int i; long l; @@ -430,7 +430,9 @@ public class NondetModelChecker extends NonProbModelChecker // Build product of MDP and automaton mainLog.println("\nConstructing MDP-DRA product..."); - modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs); + draDDRowVars = new JDDVars(); + draDDColVars = new JDDVars(); + modelProduct = mcLtl.constructProductMDP(dra, model, labelDDs, draDDRowVars, draDDColVars); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null); @@ -438,7 +440,7 @@ public class NondetModelChecker extends NonProbModelChecker // Find accepting maximum end components mainLog.println("\nFinding accepting end components..."); - JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, fairness); + JDDNode acc = mcLtl.findAcceptingStates(dra, modelProduct, draDDRowVars, draDDColVars, fairness); // Compute reachability probabilities mainLog.println("\nComputing reachability probabilities..."); @@ -457,9 +459,6 @@ public class NondetModelChecker extends NonProbModelChecker 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 @@ -469,6 +468,8 @@ public class NondetModelChecker extends NonProbModelChecker JDD.Deref(labelDDs.get(i)); } JDD.Deref(acc); + draDDRowVars.derefAll(); + draDDColVars.derefAll(); return probs; } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 6f7f2852..f96f7ebb 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -589,7 +589,7 @@ public class ProbModelChecker extends NonProbModelChecker ProbModel modelProduct; ProbModelChecker mcProduct; JDDNode startMask; - JDDVars draDDRowVars; + JDDVars draDDRowVars, draDDColVars; int i; long l; @@ -630,7 +630,9 @@ public class ProbModelChecker extends NonProbModelChecker // 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); + draDDRowVars = new JDDVars(); + draDDColVars = new JDDVars(); + modelProduct = mcLtl.constructProductMC(dra, model, labelDDs, draDDRowVars, draDDColVars); mainLog.println(); modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo()); // prism.exportStatesToFile(modelProduct, Prism.EXPORT_PLAIN, null); @@ -638,7 +640,7 @@ public class ProbModelChecker extends NonProbModelChecker // Find accepting maximum end BSCC mainLog.println("\nFinding accepting BSCCs..."); - JDDNode acc = mcLtl.findAcceptingBSCCs(dra, modelProduct); + JDDNode acc = mcLtl.findAcceptingBSCCs(dra, draDDRowVars, draDDColVars, modelProduct); // Compute reachability probabilities mainLog.println("\nComputing reachability probabilities..."); @@ -652,9 +654,6 @@ public class ProbModelChecker extends NonProbModelChecker 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 @@ -664,6 +663,8 @@ public class ProbModelChecker extends NonProbModelChecker JDD.Deref(labelDDs.get(i)); } JDD.Deref(acc); + draDDRowVars.derefAll(); + draDDColVars.derefAll(); return probs; }