From 423d169552df9f8c6be5dd400e5dacd9306fa146 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 26 Aug 2015 09:53:37 +0000 Subject: [PATCH] Symbolic LTLModelChecker: Provide constructDAForLTLFormula, use in ProbModelChecker and NondetModelChecker Mirrors the recent refactoring in the explicit engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10577 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 61 +++++++++++++++++++++++++ prism/src/prism/NondetModelChecker.java | 45 ++---------------- prism/src/prism/ProbModelChecker.java | 48 ++----------------- 3 files changed, 68 insertions(+), 86 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 86a17c38..97d6ea7d 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -27,6 +27,7 @@ package prism; +import java.io.PrintStream; import java.util.ArrayList; import java.util.BitSet; import java.util.List; @@ -37,7 +38,9 @@ import acceptance.AcceptanceOmega; import acceptance.AcceptanceOmegaDD; import acceptance.AcceptanceRabin; import acceptance.AcceptanceRabinDD; +import acceptance.AcceptanceType; import automata.DA; +import automata.LTL2DA; import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; @@ -154,6 +157,64 @@ public class LTLModelChecker extends PrismComponent return expr; } + /** + * Construct a deterministic automaton (DA) for an LTL formula, having first extracted maximal state formulas + * and model checked them with the passed in model checker. The maximal state formulas are assigned labels + * (L0, L1, etc.) which become the atomic propositions in the resulting DA. JDDNodes giving the states which + * satisfy each label are put into the vector {@code labelBS}, which should be empty when this function is called. + * + * @param mc a ModelChecker, used for checking maximal state formulas + * @param model the model + * @param expr a path expression, i.e. the LTL formula + * @param labelBS empty vector to be filled with JDDNodes for subformulas + * @param allowedAcceptance the allowed acceptance types + * @return the DA + */ + public DA constructDAForLTLFormula(ModelChecker mc, Model model, Expression expr, Vector labelDDs, AcceptanceType... allowedAcceptance) throws PrismException + { + if (Expression.containsTemporalTimeBounds(expr)) { + if (model.getModelType().continuousTime()) { + throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); + } + + if (expr.isSimplePathFormula()) { + // Convert simple path formula to canonical form, + // DRA is then generated by LTL2RabinLibrary. + // + // The conversion to canonical form has to happen here, because once + // checkMaximalStateFormulas has been called, the formula should not be modified + // anymore, as converters may expect that the generated labels for maximal state + // formulas only appear positively + expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); + } else { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); + } + } + + // Model check maximal state formulas + Expression ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelDDs); + + // Convert LTL formula to deterministic automaton (DA) + mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); + long time = System.currentTimeMillis(); + LTL2DA ltl2da = new LTL2DA(this); + DA da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance); + da.checkForCanonicalAPs(labelDDs.size()); + mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + "."); + time = System.currentTimeMillis() - time; + mainLog.println("Time for deterministic automaton translation: " + time / 1000.0 + " seconds."); + // If required, export DA + if (getSettings().getExportPropAut()) { + mainLog.println("Exporting DA to file \"" + getSettings().getExportPropAutFilename() + "\"..."); + PrintStream out = PrismUtils.newPrintStream(getSettings().getExportPropAutFilename()); + da.print(out, getSettings().getExportPropAutType()); + out.close(); + } + + return da; + } + + /** * Construct the product of a DA and a DTMC/CTMC. * @param da The DA diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 72f5d0de..dd6194e1 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1116,8 +1116,7 @@ public class NondetModelChecker extends NonProbModelChecker { LTLModelChecker mcLtl; StateValues probsProduct = null, probs = null; - Expression ltl; - Vector labelDDs; + Vector labelDDs = new Vector(); DA da; NondetModel modelProduct; NondetModelChecker mcProduct; @@ -1133,25 +1132,6 @@ public class NondetModelChecker extends NonProbModelChecker expr = Expression.Not(Expression.Parenth(expr)); } - if (Expression.containsTemporalTimeBounds(expr)) { - if (model.getModelType().continuousTime()) { - throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); - } - - if (expr.isSimplePathFormula()) { - // Convert simple path formula to canonical form, - // DA is then generated by LTL2RabinLibrary. - // - // The conversion to canonical form has to happen here, because once - // checkMaximalStateFormulas has been called, the formula should not be modified - // anymore, as converters may expect that the generated labels for maximal state - // formulas only appear positively - expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); - } else { - throw new PrismException("Time-bounded operators not supported in LTL: " + expr); - } - } - // Can't do "dfa" properties yet if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); @@ -1159,34 +1139,17 @@ public class NondetModelChecker extends NonProbModelChecker // 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 automaton (DA) - mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); - l = System.currentTimeMillis(); - LTL2DA ltl2da = new LTL2DA(prism); AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, AcceptanceType.GENERALIZED_RABIN, AcceptanceType.REACH }; - da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance); - da.checkForCanonicalAPs(labelDDs.size()); - mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+"."); - l = System.currentTimeMillis() - l; - mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds."); - // If required, export DA - if (prism.getSettings().getExportPropAut()) { - mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); - da.print(out, prism.getSettings().getExportPropAutType()); - out.close(); - } + da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance); // Build product of MDP and automaton + l = System.currentTimeMillis(); mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); daDDRowVars = new JDDVars(); daDDColVars = new JDDVars(); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 19fb8c05..4cfbab0c 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -506,63 +506,21 @@ public class ProbModelChecker extends NonProbModelChecker { LTLModelChecker mcLtl; StateValues probsProduct = null, probs = null; - Expression ltl; - Vector labelDDs; + Vector labelDDs = new Vector(); DA da; ProbModel modelProduct; ProbModelChecker mcProduct; JDDNode startMask; JDDVars daDDRowVars, daDDColVars; int i; - long l; - - if (Expression.containsTemporalTimeBounds(expr)) { - if (model.getModelType().continuousTime()) { - throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); - } - - if (expr.isSimplePathFormula()) { - // Convert simple path formula to canonical form, - // DRA is then generated by LTL2RabinLibrary. - // - // The conversion to canonical form has to happen here, because once - // checkMaximalStateFormulas has been called, the formula should not be modified - // anymore, as converters may expect that the generated labels for maximal state - // formulas only appear positively - expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); - } else { - throw new PrismException("Time-bounded operators not supported in LTL: " + expr); - } - } - // 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 automaton (DA) - mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); - l = System.currentTimeMillis(); - LTL2DA ltl2da = new LTL2DA(prism); AcceptanceType[] allowedAcceptance = { AcceptanceType.RABIN, AcceptanceType.REACH, AcceptanceType.GENERIC }; - da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance); - da.checkForCanonicalAPs(labelDDs.size()); - mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + "."); - l = System.currentTimeMillis() - l; - mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds."); - // If required, export DA - if (prism.getSettings().getExportPropAut()) { - mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"..."); - PrintStream out = PrismUtils.newPrintStream(prism.getSettings().getExportPropAutFilename()); - da.print(out, prism.getSettings().getExportPropAutType()); - out.close(); - } + mcLtl = new LTLModelChecker(prism); + da = mcLtl.constructDAForLTLFormula(this, model, expr, labelDDs, allowedAcceptance); // Build product of Markov chain and automaton // (note: might be a CTMC - StochModelChecker extends this class)