From 6277e607cdb03e75194a454749dcbf1f7be7566b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 19 Jul 2017 12:25:27 +0000 Subject: [PATCH] symbolic LTLModelChecker: convert LTL product to use statesOfInterest This starts the reachability in the product from the set of states of interest (with the corresponding initial state in the deterministic automaton). Additionally, these statesOfInterest in the product become the initial states of the product model. Deprecated legacy methods for obtaining product models as before (with the initial states in the product model being those that were initial states in the original model) are provided. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12049 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 196 ++++++++++++++++++++++----- 1 file changed, 164 insertions(+), 32 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 95c049f5..2306d216 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -207,12 +207,33 @@ public class LTLModelChecker extends PrismComponent } + /** + * Construct the product of a DA and a DTMC/CTMC, starting from a given set + * of states of interest. The corresponding states in the product become + * the initial states in the product model. + * + *
[ REFS: returned ProbModel, DEREFS: statesOfInterest] + * @param da The DA + * @param model The DTMC/CTMC + * @param labelDDs BDDs giving the set of states for each AP in the DA + * @param statesOfInterest the states in the model that serve as the starting point for the DA product + */ + public ProbModel constructProductMC(DA da, ProbModel model, Vector labelDDs, JDDNode statesOfInterest) throws PrismException + { + return constructProductMC(da, model, labelDDs, null, null, statesOfInterest); + } + /** * Construct the product of a DA and a DTMC/CTMC. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, the initial states of the product model correspond to + * the initial states of the original model, but the product is constructed + * from all states of the original model. * @param da The DA * @param model The DTMC/CTMC - * @param labelDDs BDDs giving the set of states for each AP in the DRA + * @param labelDDs BDDs giving the set of states for each AP in the DA */ + @Deprecated public ProbModel constructProductMC(DA da, ProbModel model, Vector labelDDs) throws PrismException { return constructProductMC(da, model, labelDDs, null, null, true); @@ -220,12 +241,17 @@ public class LTLModelChecker extends PrismComponent /** * Construct the product of a DA and a DTMC/CTMC. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, the initial states of the product model correspond to + * the initial states of the original model, but the product is constructed + * from all states of the original model. * @param da The DA * @param model The DTMC/CTMC * @param labelDDs BDDs giving the set of states for each AP in the DA * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA */ + @Deprecated public ProbModel constructProductMC(DA da, ProbModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy) throws PrismException { @@ -234,6 +260,13 @@ public class LTLModelChecker extends PrismComponent /** * Construct the product of a DA and a DTMC/CTMC. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, if {@code allInit} is {@code true}, + * the initial states of the product model correspond to the initial states + * of the original model, but the product is constructed + * from all states of the original model. + * If {@code allInit} is {@code false}, the product is only constructed + * from the initial states of the original model. * @param da The DA * @param model The DTMC/CTMC * @param labelDDs BDDs giving the set of states for each AP in the DA @@ -242,8 +275,52 @@ public class LTLModelChecker extends PrismComponent * @param allInit Do we assume that all states of the original model are initial states? * (just for the purposes of reachability) */ + @Deprecated public ProbModel constructProductMC(DA da, ProbModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy, boolean allInit) throws PrismException + { + // construct suitable statesOfInterest + JDDNode statesOfInterest = allInit ? model.getReach().copy() : model.getStart().copy(); + + // generate temporary storage for row / col vars if needed + JDDVars daDDRowVars = daDDRowVarsCopy == null ? new JDDVars() : daDDRowVarsCopy; + JDDVars daDDColVars = daDDColVarsCopy == null ? new JDDVars() : daDDColVarsCopy; + + // construct product using statesOfInterest-based method + ProbModel modelProd = constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); + + // Reset initial state (to mimic legacy behavior) + JDDNode newStart = buildStartMask(da, labelDDs, daDDRowVars); + JDD.Ref(model.getStart()); + newStart = JDD.And(model.getStart(), newStart); + modelProd.setStart(newStart); + + // deref temporary storage for row / col vars if needed + if (daDDRowVarsCopy == null) + daDDRowVars.derefAll(); + if (daDDColVarsCopy == null) + daDDColVars.derefAll(); + + return modelProd; + } + + /** + * Construct the product of a DA and a DTMC/CTMC, starting from a given set + * of states of interest. The corresponding states in the product become + * the initial states in the product model. + * + *
[ REFS: returned ProbModel, DEREFS: statesOfInterest] + * @param da The DA + * @param model The DTMC/CTMC + * @param labelDDs BDDs giving the set of states for each AP in the DA + * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA + * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA + * @param statesOfInterest the states in the model that serve as the starting point for the DA product + */ + public ProbModel constructProductMC(DA da, ProbModel model, + Vector labelDDs, + JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy, + JDDNode statesOfInterest) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -327,16 +404,10 @@ public class LTLModelChecker extends PrismComponent newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); // Build set of initial states for product - // 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 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 - // Note that we reset the initial states after reachability, corresponding to just the initial states of the original model. + // We use the product states between the states of interest and the corresponding + // DA states as the initial states of the product model (used for reachability) newStart = buildStartMask(da, labelDDs, daDDRowVars); - JDD.Ref(allInit ? model.getReach() : model.getStart()); - newStart = JDD.And(allInit ? model.getReach() : model.getStart(), newStart); + newStart = JDD.And(model.getReach().copy(), statesOfInterest.copy(), newStart); // Create a new model model object to store the product model ProbModel modelProd = new ProbModel( @@ -367,30 +438,45 @@ public class LTLModelChecker extends PrismComponent throw new PrismException("Model-"+da.getAutomataType()+" product has deadlock states"); } - // Reset initial state - newStart = buildStartMask(da, labelDDs, daDDRowVars); - JDD.Ref(model.getStart()); - newStart = JDD.And(model.getStart(), newStart); - modelProd.setStart(newStart); - // if possible, return copies of the DA DD variables via the method parameters if (daDDRowVarsCopy != null) daDDRowVarsCopy.copyVarsFrom(daDDRowVars); if (daDDColVarsCopy != null) daDDColVarsCopy.copyVarsFrom(daDDColVars); + JDD.Deref(statesOfInterest); daDDRowVars.derefAll(); daDDColVars.derefAll(); return modelProd; } + /** + * Construct the product of a DA and an MDP, starting from a given set + * of states of interest. The corresponding states in the product become + * the initial states in the product model. + * + *
[ REFS: returned NondetModel, DEREFS: statesOfInterest] + * @param da The DA + * @param model The MDP + * @param labelDDs BDDs giving the set of states for each AP in the DA + */ + public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs, JDDNode statesOfInterest) throws PrismException + { + return constructProductMDP(da, model, labelDDs, null, null, statesOfInterest); + } + /** * Construct the product of a DA and an MDP. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, the initial states of the product model correspond to + * the initial states of the original model, but the product is constructed + * from all states of the original model. * @param da The DA * @param model The MDP * @param labelDDs BDDs giving the set of states for each AP in the DA */ + @Deprecated public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs) throws PrismException { return constructProductMDP(da, model, labelDDs, null, null, true, null); @@ -398,20 +484,33 @@ public class LTLModelChecker extends PrismComponent /** * Construct the product of a DA and an MDP. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, the initial states of the product model correspond to + * the initial states of the original model, but the product is constructed + * from all states of the original model. * @param da The DA * @param model The MDP * @param labelDDs BDDs giving the set of states for each AP in the DA * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA */ + @Deprecated public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy) throws PrismException { return constructProductMDP(da, model, labelDDs, daDDRowVarsCopy, daDDColVarsCopy, true, null); } + /** * Construct the product of a DA and an MDP. + *
Deprecated legacy method, use variant with statesOfInterest. + * With this method, if {@code allInit} is {@code true}, + * the initial states of the product model correspond to the initial states + * of the original model, but the product is constructed + * from all the states in {@code init}. + * If {@code allInit} is {@code false}, the product is only constructed + * from the initial states of the original model. * @param da The DA * @param model The MDP * @param labelDDs BDDs giving the set of states for each AP in the DA @@ -422,8 +521,52 @@ public class LTLModelChecker extends PrismComponent * @param init The initial state(s) (of the original model) used to build the product; * if null; we just take the existing initial states from model.getStart(). */ + @Deprecated public NondetModel constructProductMDP(DA da, NondetModel model, Vector labelDDs, JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy, boolean allInit, JDDNode init) throws PrismException + { + // construct suitable statesOfInterest + JDDNode statesOfInterest = allInit ? model.getReach().copy() : init.copy(); + + // generate temporary storage for row / col vars if needed + JDDVars daDDRowVars = daDDRowVarsCopy == null ? new JDDVars() : daDDRowVarsCopy; + JDDVars daDDColVars = daDDColVarsCopy == null ? new JDDVars() : daDDColVarsCopy; + + // construct product using statesOfInterest-based method + NondetModel modelProd = constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); + + // Reset initial state (to mimic legacy behavior) + JDDNode newStart = buildStartMask(da, labelDDs, daDDRowVars); + JDD.Ref(init != null ? init : model.getStart()); + newStart = JDD.And(init != null ? init : model.getStart(), newStart); + modelProd.setStart(newStart); + + // deref temporary storage for row / col vars if needed + if (daDDRowVarsCopy == null) + daDDRowVars.derefAll(); + if (daDDColVarsCopy == null) + daDDColVars.derefAll(); + + return modelProd; + } + + /** + * Construct the product of a DA and an MDP, starting from a given set + * of states of interest. The corresponding states in the product become + * the initial states in the product model. + * + *
[ REFS: returned NondetModel, DEREFS: statesOfInterest] + * @param da The DA + * @param model The MDP + * @param labelDDs BDDs giving the set of states for each AP in the DA + * @param daDDRowVarsCopy (Optionally) empty JDDVars object to obtain copy of DD row vars for DA + * @param daDDColVarsCopy (Optionally) empty JDDVars object to obtain copy of DD col vars for DA + * @param statesOfInterest the states of interest, serving as the starting point for the MPD-DA product + */ + public NondetModel constructProductMDP(DA da, NondetModel model, + Vector labelDDs, + JDDVars daDDRowVarsCopy, JDDVars daDDColVarsCopy, + JDDNode statesOfInterest) throws PrismException { // Existing model - dds, vars, etc. JDDVars varDDRowVars[]; @@ -441,7 +584,7 @@ public class LTLModelChecker extends PrismComponent // DA stuff JDDVars daDDRowVars, daDDColVars; // Misc - int i, j, n; + int i, n; boolean before; // Get details of old model (no copy, does not need to be cleaned up) @@ -508,17 +651,10 @@ public class LTLModelChecker extends PrismComponent newTrans = JDD.Apply(JDD.TIMES, model.getTrans(), newTrans); // Build set of initial states for product - // 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 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 - // Note that we reset the initial states after reachability, corresponding to just the initial states of the original model. - // The initial state of the original model can be overridden by passing in 'init'. + // We use the product states between the states of interest and the corresponding + // DA states as the initial states of the product model (used for reachability) newStart = buildStartMask(da, labelDDs, daDDRowVars); - JDD.Ref(allInit ? model.getReach() : init != null ? init : model.getStart()); - newStart = JDD.And(allInit ? model.getReach() : init != null ? init : model.getStart(), newStart); + newStart = JDD.And(model.getReach().copy(), statesOfInterest.copy(), newStart); // Create a new model model object to store the product model NondetModel modelProd = new NondetModel( @@ -564,11 +700,6 @@ public class LTLModelChecker extends PrismComponent throw new PrismException("Model-DA product has deadlock states"); } - // Reset initial state - newStart = buildStartMask(da, labelDDs, daDDRowVars); - JDD.Ref(init != null ? init : model.getStart()); - newStart = JDD.And(init != null ? init : model.getStart(), newStart); - modelProd.setStart(newStart); //try { prism.exportStatesToFile(modelProd, Prism.EXPORT_PLAIN, new java.io.File("prod.sta")); } //catch (java.io.FileNotFoundException e) {} @@ -579,6 +710,7 @@ public class LTLModelChecker extends PrismComponent if (daDDColVarsCopy != null) daDDColVarsCopy.copyVarsFrom(daDDColVars); + JDD.Deref(statesOfInterest); daDDRowVars.derefAll(); daDDColVars.derefAll();