diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 2306d216..01d5e8e9 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -42,6 +42,7 @@ import acceptance.AcceptanceRabinDD; import acceptance.AcceptanceType; import automata.DA; import automata.LTL2DA; +import common.StopWatch; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; @@ -61,6 +62,94 @@ import parser.type.TypePathBool; */ public class LTLModelChecker extends PrismComponent { + /** + * A wrapper for the product of a model (DTMC, MDP) and + * a deterministic omega-automaton for some linear-temporal property. + *
+ * Provides methods to obtain the product model, the acceptance condition and + * for translating a result in the product back to the original model. + * @param the underlying model type (ProbModel, NondetModel) + */ + public static class LTLProduct extends Product { + /** + * The omega-regular acceptance condition, lifted to the product model, + * but not necessarily restricted to the product model's reachable states. + */ + private AcceptanceOmegaDD acceptance; + + /** + * The omega-regular acceptance condition, lifted to the product model, + * restricted to the product model's reachable states. + *
+ * Computed on demand. + */ + private AcceptanceOmegaDD prodAcceptance = null; + + /** + * Constructor. + *
+ * Takes ownership of the product model, the acceptance condition, + * the productStatesOfInterest and the automatonRowVars. + * clears those when clear() is called. + *
[ STORES: productModel, acceptance, productStatesOfInterest, automatonRowVars ] + */ + public LTLProduct(M productModel, M originalModel, AcceptanceOmegaDD acceptance, JDDNode productStatesOfInterest, JDDVars automatonRowVars) + { + super(productModel, originalModel, productStatesOfInterest, automatonRowVars); + this.acceptance = acceptance; + } + + /** + * Get the acceptance condition for the product (not a copy). + *
+ * The acceptance sets are not necessarily restricted to the + * reachable part of the state space of the product model. + *
[ REFS: none, DEREFS: none ] + */ + public AcceptanceOmegaDD getAcceptance() { + return acceptance; + } + + + /** + * Get the acceptance condition for the product, restricted + * to the reachable state space of the product model (not a copy). + *
[ REFS: none, DEREFS: none ] + */ + public AcceptanceOmegaDD getProductAcceptance() { + if (prodAcceptance == null) { + // compute on demand, intersect with getReach() from product model + prodAcceptance = acceptance.clone(); + prodAcceptance.intersect(getProductModel().getReach()); + } + return prodAcceptance; + } + + /** + * Set the acceptance condition for the product (takes + * ownership of the provided acceptance object, clears + * previously stored acceptance condition). + *
[ STORES: acceptance ] + */ + public void setAcceptance(AcceptanceOmegaDD acceptance) { + if (this.acceptance != null) { + this.acceptance.clear(); + } + this.acceptance = acceptance; + } + + @Override + public void clear() { + super.clear(); + acceptance.clear(); + acceptance = null; + if (prodAcceptance != null) { + prodAcceptance.clear(); + prodAcceptance = null; + } + } + } + /** * Create a new LTLModelChecker, inherit basic state from parent (unless null). */ @@ -482,6 +571,51 @@ public class LTLModelChecker extends PrismComponent return constructProductMDP(da, model, labelDDs, null, null, true, null); } + /** + * Construct the product of a DTMC with a deterministic automaton for the given LTL expression. + *
[ REFS: returned LTLProduct, DEREFS: statesOfInterest] + */ + public LTLProduct constructProductMC(ProbModelChecker mc, ProbModel model, Expression expr, JDDNode statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException + { + Vector labelDDs = new Vector(); + DA da; + + da = constructDAForLTLFormula(mc, model, expr, labelDDs, allowedAcceptance); + + return constructProductMC(model, da, labelDDs, statesOfInterest); + } + + /** + * Construct the product of a DTMC with the given deterministic automaton (with AP set L0,L1,...), + * returning an LTLProduct. + *
+ * The state sets corresponding to each AP label are given via the labelDDs vector, + * which will be dereferenced after this method call. + *
[ REFS: returned LTLProduct, DEREFS: statesOfInterest, labelDDs] + */ + public LTLProduct constructProductMC(ProbModel model, DA da, Vector labelDDs, JDDNode statesOfInterest) throws PrismException + { + // Build product of Markov chain and automaton + mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); + JDDVars daDDRowVars = new JDDVars(); + JDDVars daDDColVars = new JDDVars(); + StopWatch timer = new StopWatch(getLog()); + timer.start("product construction"); + ProbModel modelProduct = constructProductMC(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); + timer.stop(); + mainLog.println(); + modelProduct.printTransInfo(mainLog, false); + + AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars); + + daDDColVars.derefAll(); + for (int i = 0; i < labelDDs.size(); i++) { + JDD.Deref(labelDDs.get(i)); + } + + return new LTLProduct(modelProduct, model, acceptance, modelProduct.getStart().copy(), daDDRowVars); + } + /** * Construct the product of a DA and an MDP. *
Deprecated legacy method, use variant with statesOfInterest. @@ -717,6 +851,48 @@ public class LTLModelChecker extends PrismComponent return modelProd; } + /** + * Construct the product of an MDP with a deterministic automaton for the given LTL expression. + */ + public LTLProduct constructProductMDP(NondetModelChecker mc, NondetModel model, Expression expr, JDDNode statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { + Vector labelDDs = new Vector(); + DA da; + + da = constructDAForLTLFormula(mc, model, expr, labelDDs, allowedAcceptance); + + return constructProductMDP(model, da, labelDDs, statesOfInterest); + } + + /** + * Construct the product of an MDP with the given deterministic automaton (with AP set L0,L1,...), + * returning an LTLProduct. + *
+ * The state sets corresponding to each AP label are given via the labelDDs vector, + * which will be dereferenced after this method call. + */ + public LTLProduct constructProductMDP(NondetModel model, DA da, Vector labelDDs, JDDNode statesOfInterest) throws PrismException + { + // Build product of MDP and automaton + mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); + JDDVars daDDRowVars = new JDDVars(); + JDDVars daDDColVars = new JDDVars(); + StopWatch timer = new StopWatch(getLog()); + timer.start("product construction"); + NondetModel modelProduct = constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars, statesOfInterest); + timer.stop(); + mainLog.println(); + modelProduct.printTransInfo(mainLog, getSettings().getBoolean(PrismSettings.PRISM_EXTRA_DD_INFO)); + + AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars); + + daDDColVars.derefAll(); + for (int i = 0; i < labelDDs.size(); i++) { + JDD.Deref(labelDDs.get(i)); + } + + return new LTLProduct(modelProduct, model, acceptance, modelProduct.getStart().copy(), daDDRowVars); + } + /** * Builds a (referenced) mask BDD representing all possible transitions in a product built with * DA {@code da}, i.e. all the transitions ((s,q),(s',q')) where q' = delta(q, label(s')) in the DA.