From 6e1cf75a8ea00ed5cb8e9df4ac0206e62c302f81 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 3 Jun 2015 22:02:26 +0000 Subject: [PATCH] Some re-factoring of LTL model checking in the explicit engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9921 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 117 ++++++++++-------------- 1 file changed, 48 insertions(+), 69 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index e8cd704d..f4509a5d 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -65,7 +65,8 @@ import common.IterableStateSet; public class LTLModelChecker extends PrismComponent { /** Make LTL product accessible as a Product */ - public class LTLProduct extends Product { + public class LTLProduct extends Product + { private int daSize; private int invMap[]; private AcceptanceOmega acceptance; @@ -99,7 +100,6 @@ public class LTLModelChecker extends PrismComponent } } - /** * Create a new LTLModelChecker, inherit basic state from parent (unless null). */ @@ -186,31 +186,32 @@ public class LTLModelChecker extends PrismComponent } /** - * Generate a deterministic automaton for the given LTL expression and construct the product. + * 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. BitSets 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 ProbModelChecker, used for checking maximal state formulas - * @param dtmc the model - * @param expr a path expression - * @param statesOfInterest the set of states for which values should be calculated (null = all states) + * @param model the model + * @param expr a path expression, i.e. the LTL formula + * @param labelBS empty vector to be filled with BitSets for subformulas * @param allowedAcceptance the allowed acceptance types - * @return the product with the DA + * @return the DA */ - public LTLProduct constructProductMC(ProbModelChecker mc, DTMC dtmc, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException + public DA constructDAForLTLFormula(ProbModelChecker mc, Model model, Expression expr, Vector labelBS, AcceptanceType... allowedAcceptance) throws PrismException { Expression ltl; DA da; - LTLProduct product; long time; if (Expression.containsTemporalTimeBounds(expr)) { - if (dtmc.getModelType().continuousTime()) { - throw new PrismException("DRA construction for time-bounded operators not supported for " + dtmc.getModelType()+"."); + if (model.getModelType().continuousTime()) { + throw new PrismException("Automaton 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. - // + // 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 @@ -222,8 +223,7 @@ public class LTLModelChecker extends PrismComponent } // Model check maximal state formulas - Vector labelBS = new Vector(); - ltl = checkMaximalStateFormulas(mc, dtmc, expr.deepCopy(), labelBS); + ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS); // Convert LTL formula to deterministic automaton mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); @@ -233,20 +233,39 @@ public class LTLModelChecker extends PrismComponent mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + "."); time = System.currentTimeMillis() - time; mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds."); - // If required, export DRA + // If required, export DA if (settings.getExportPropAut()) { - mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); + mainLog.println("Exporting " + da.getAutomataType() + " to file \"" + settings.getExportPropAutFilename() + "\"..."); PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); out.println(da); out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); + //dra.printDot(new java.io.PrintStream("da.dot")); } + + return da; + } + + /** + * Generate a deterministic automaton for the given LTL formula + * and construct the product of this automaton with a Markov chain. + * + * @param mc a ProbModelChecker, used for checking maximal state formulas + * @param model the model + * @param expr a path expression + * @param statesOfInterest the set of states for which values should be calculated (null = all states) + * @param allowedAcceptance the allowed acceptance types + * @return the product with the DA + */ + public LTLProduct constructProductMC(ProbModelChecker mc, DTMC model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException + { + // Convert LTL formula to automaton + Vector labelBS = new Vector(); + DA da; + da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance); - - // Build product of Markov chain and automaton + // Build product of model and automaton mainLog.println("\nConstructing MC-"+da.getAutomataType()+" product..."); - product = constructProductMC(da, dtmc, labelBS, statesOfInterest); - + LTLProduct product = constructProductMC(da, model, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); return product; @@ -371,7 +390,8 @@ public class LTLModelChecker extends PrismComponent return product; } /** - * Generate the DA for the given LTL expression and construct the product. + * Generate a deterministic automaton for the given LTL formula + * and construct the product of this automaton with an MDP. * * @param mc a ProbModelChecker, used for checking maximal state formulas * @param model the model @@ -383,55 +403,14 @@ public class LTLModelChecker extends PrismComponent */ public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest, AcceptanceType... allowedAcceptance) throws PrismException { - Expression ltl; - DA da; - LTLProduct product; - long time; - - if (Expression.containsTemporalTimeBounds(expr)) { - if (model.getModelType().continuousTime()) { - throw new PrismException("DRA 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 + // Convert LTL formula to automaton Vector labelBS = new Vector(); - ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS); - - // Convert LTL formula to deterministic automaton - mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")..."); - time = System.currentTimeMillis(); - LTL2DA ltl2da = new LTL2DA(this); - da = ltl2da.convertLTLFormulaToDA(ltl, mc.getConstantValues(), allowedAcceptance); - mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics() + "."); - time = System.currentTimeMillis() - time; - mainLog.println("Time for "+da.getAutomataType()+" translation: " + time / 1000.0 + " seconds."); - // If required, export DA - if (settings.getExportPropAut()) { - mainLog.println("Exporting "+da.getAutomataType()+" to file \"" + settings.getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); - out.println(da); - out.close(); - //da.printDot(new java.io.PrintStream("da.dot")); - } + DA da; + da = constructDAForLTLFormula(mc, model, expr, labelBS, allowedAcceptance); - // Build product of MDP and automaton + // Build product of model and automaton mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product..."); - product = constructProductMDP(da, model, labelBS, statesOfInterest); - + LTLProduct product = constructProductMDP(da, model, labelBS, statesOfInterest); mainLog.print("\n" + product.getProductModel().infoStringTable()); return product;