From 3e9a240b711ce67c261b82fb9ffdc169ea12d060 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 15 Dec 2009 09:36:57 +0000 Subject: [PATCH] LTL model checking code: code tidy and clean-up and some output. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1650 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 50 +++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 8 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 0fc8e71e..caf5fcb8 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -110,8 +110,24 @@ public class LTLModelChecker /** * 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) */ public ProbModel constructProductMC(DRA dra,ProbModel model, Vector labelDDs) throws PrismException + { + return constructProductMC(dra, model, labelDDs, 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) + */ + public ProbModel constructProductMC(DRA dra,ProbModel model, Vector labelDDs, boolean allInit) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -219,14 +235,15 @@ public class LTLModelChecker 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. + // Note, by default, we take product of *all* states of the original model, 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) + // states of the original model (because we compute probabilities for all of them) // but some of these may not be reachable from the initial state of the product model. + // Optionally (if allInit is false), we don't do this - maybe because we only care about result for the initial state newStart = buildStartMask(dra, labelDDs, draDDRowVars); - JDD.Ref(model.getReach()); - newStart = JDD.And(model.getReach(), newStart); + JDD.Ref(allInit ? model.getReach() : model.getStart()); + newStart = JDD.And(allInit ? model.getReach() : model.getStart(), newStart); // Create a new model model object to store the product model ProbModel modelProd = new ProbModel( @@ -258,8 +275,23 @@ public class LTLModelChecker /** * 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 */ public NondetModel constructProductMDP(DRA dra, NondetModel model, Vector labelDDs) throws PrismException + { + return constructProductMDP(dra, model, labelDDs, 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 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 { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -371,14 +403,15 @@ public class LTLModelChecker 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. + // Note, by default, we take product of *all* states of the original model, 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) + // states of the original model (because we compute probabilities for all of them) // but some of these may not be reachable from the initial state of the product model. + // Optionally (if allInit is false), we don't do this - maybe because we only care about result for the initial state newStart = buildStartMask(dra, labelDDs, draDDRowVars); - JDD.Ref(model.getReach()); - newStart = JDD.And(model.getReach(), newStart); + JDD.Ref(allInit ? model.getReach() : model.getStart()); + newStart = JDD.And(allInit ? model.getReach() : model.getStart(), newStart); // Create a new model model object to store the product model NondetModel modelProd = new NondetModel( @@ -769,6 +802,7 @@ public class LTLModelChecker JDD.Deref(stableSet); JDD.Deref(stableSetTrans); sccs = sccComputer.getVectSCCs(); + mainLog.println("SCC computer found " + sccs.size() + " SCCs"); JDD.Deref(sccComputer.getNotInSCCs()); candidates.addAll(sccs); }