From a18d74e5b67d2fc2e270dc2d2a8d0dbd3f978b83 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 01:05:07 +0000 Subject: [PATCH] provide LTLModelChecker.constructProductMDP(MDP mdp, Expression ltl), encapsulating DA generation and product construction. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9594 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/LTLModelChecker.java | 50 +++++++++++++++++++++++++ prism/src/explicit/MDPModelChecker.java | 43 +++------------------ 2 files changed, 56 insertions(+), 37 deletions(-) diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index 4913c5a8..e765ae70 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/prism/src/explicit/LTLModelChecker.java @@ -337,6 +337,56 @@ public class LTLModelChecker extends PrismComponent return product; } + /** + * Generate the DRA for the given LTL expression and construct the product. + * + * @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) + * @return the product with the DRA + */ + public LTLProduct constructProductMDP(ProbModelChecker mc, MDP model, Expression expr, BitSet statesOfInterest) throws PrismException + { + Expression ltl; + DA dra; + LTLProduct product; + long time; + + // Can't do LTL with time-bounded variants of the temporal operators + if (Expression.containsTemporalTimeBounds(expr)) { + throw new PrismException("Time-bounded operators not supported in LTL: " + expr); + } + + // Model check maximal state formulas + Vector labelBS = new Vector(); + ltl = checkMaximalStateFormulas(mc, model, expr.deepCopy(), labelBS); + + // Convert LTL formula to deterministic Rabin automaton (DRA) + mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); + time = System.currentTimeMillis(); + dra = convertLTLFormulaToDRA(ltl); + mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); + time = System.currentTimeMillis() - time; + mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); + // If required, export DRA + if (settings.getExportPropAut()) { + mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); + PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); + out.println(dra); + out.close(); + //dra.printDot(new java.io.PrintStream("dra.dot")); + } + + // Build product of MDP and automaton + mainLog.println("\nConstructing MDP-DRA product..."); + product = constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest); + + mainLog.print("\n" + product.getProductModel().infoStringTable()); + + return product; + } + /** * Construct the product of a DRA and an MDP. * @param dra The DRA diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 660c4e08..9ab56d02 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -30,11 +30,8 @@ import java.util.BitSet; import java.util.Iterator; import java.util.List; import java.util.Map; -import java.util.Vector; -import acceptance.AcceptanceRabin; import parser.ast.Expression; -import prism.DA; import prism.PrismComponent; import prism.PrismDevNullLog; import prism.PrismException; @@ -66,48 +63,20 @@ public class MDPModelChecker extends ProbModelChecker { LTLModelChecker mcLtl; StateValues probsProduct, probs; - Expression ltl; - DA dra; MDPModelChecker mcProduct; - long time; + LTLModelChecker.LTLProduct product; - // Can't do LTL with time-bounded variants of the temporal operators - if (Expression.containsTemporalTimeBounds(expr)) { - throw new PrismException("Time-bounded operators not supported in LTL: " + expr); - } - - // For LTL model checking routines - mcLtl = new LTLModelChecker(this); - - // Model check maximal state formulas - Vector labelBS = new Vector(); - ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelBS); - - // Convert LTL formula to deterministic Rabin automaton (DRA) // For min probabilities, need to negate the formula // (add parentheses to allow re-parsing if required) if (minMax.isMin()) { - ltl = Expression.Not(Expression.Parenth(ltl)); - } - mainLog.println("\nBuilding deterministic Rabin automaton (for " + ltl + ")..."); - time = System.currentTimeMillis(); - dra = LTLModelChecker.convertLTLFormulaToDRA(ltl); - mainLog.println("DRA has " + dra.size() + " states, " + dra.getAcceptance().getSizeStatistics() + "."); - time = System.currentTimeMillis() - time; - mainLog.println("Time for Rabin translation: " + time / 1000.0 + " seconds."); - // If required, export DRA - if (settings.getExportPropAut()) { - mainLog.println("Exporting DRA to file \"" + settings.getExportPropAutFilename() + "\"..."); - PrismLog out = new PrismFileLog(settings.getExportPropAutFilename()); - out.println(dra); - out.close(); - //dra.printDot(new java.io.PrintStream("dra.dot")); + expr = Expression.Not(Expression.Parenth(expr.deepCopy())); } - // Build product of MDP and automaton - mainLog.println("\nConstructing MDP-DRA product..."); - LTLModelChecker.LTLProduct product = mcLtl.constructProductMDP(dra, (MDP) model, labelBS, statesOfInterest); + // For LTL model checking routines + mcLtl = new LTLModelChecker(this); + product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest); + // Find accepting MECs + compute reachability probabilities mainLog.println("\nFinding accepting MECs..."); BitSet acceptingMECs = mcLtl.findAcceptingECStatesForRabin(product.getProductModel(), product.getAcceptance());