From 60ecccd9da6037291d535b87cb4865a14ef90cbe Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 31 Jan 2015 10:52:27 +0000 Subject: [PATCH] New setting/switch: -pathviaautomata (all path formulas are handled via the LTL/DRA-engine), defaults to false. Honour in model checkers. [Joachim Klein] git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9601 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 14 ++++++++++++-- prism/src/prism/NondetModelChecker.java | 14 ++++++++++++-- prism/src/prism/PrismSettings.java | 8 ++++++++ prism/src/prism/ProbModelChecker.java | 14 ++++++++++++-- 4 files changed, 44 insertions(+), 6 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index b276e977..dfbcdf16 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -557,8 +557,18 @@ public class ProbModelChecker extends NonProbModelChecker protected StateValues checkProbPathFormula(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) - // and then pass control to appropriate method. - if (expr.isSimplePathFormula()) { + // and whether we want to use the corresponding algorithms + boolean useSimplePathAlgo = expr.isSimplePathFormula(); + + if (useSimplePathAlgo && + settings.getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && + LTLModelChecker.isSupportedLTLFormula(model.getModelType(), expr)) { + // If PRISM_PATH_VIA_AUTOMATA is true, we want to use the LTL engine + // whenever possible + useSimplePathAlgo = false; + } + + if (useSimplePathAlgo) { return checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); } else { return checkProbPathFormulaLTL(model, expr, false, minMax, statesOfInterest); diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 491c8215..d9776710 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -653,8 +653,18 @@ public class NondetModelChecker extends NonProbModelChecker protected StateValues checkProbPathFormula(Expression expr, boolean qual, boolean min) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) - // and then pass control to appropriate method. - if (expr.isSimplePathFormula()) { + // and whether we want to use the corresponding algorithms + boolean useSimplePathAlgo = expr.isSimplePathFormula(); + + if (useSimplePathAlgo && + prism.getSettings().getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && + LTLModelChecker.isSupportedLTLFormula(model.getModelType(), expr)) { + // If PRISM_PATH_VIA_AUTOMATA is true, we want to use the LTL engine + // whenever possible + useSimplePathAlgo = false; + } + + if (useSimplePathAlgo) { return checkProbPathFormulaSimple(expr, qual, min); } else { return checkProbPathFormulaLTL(expr, qual, min); diff --git a/prism/src/prism/PrismSettings.java b/prism/src/prism/PrismSettings.java index d593fb02..fbef2e46 100644 --- a/prism/src/prism/PrismSettings.java +++ b/prism/src/prism/PrismSettings.java @@ -102,6 +102,7 @@ public class PrismSettings implements Observer public static final String PRISM_PTA_METHOD = "prism.ptaMethod"; public static final String PRISM_TRANSIENT_METHOD = "prism.transientMethod"; public static final String PRISM_AR_OPTIONS = "prism.arOptions"; + public static final String PRISM_PATH_VIA_AUTOMATA = "prism.pathViaAutomata"; public static final String PRISM_EXPORT_ADV = "prism.exportAdv"; public static final String PRISM_EXPORT_ADV_FILENAME = "prism.exportAdvFilename"; @@ -260,6 +261,8 @@ public class PrismSettings implements Observer "Parameters for symmetry reduction (format: \"i j\" where i and j are the number of modules before and after the symmetric ones; empty string means symmetry reduction disabled)." }, { STRING_TYPE, PRISM_AR_OPTIONS, "Abstraction refinement options", "3.3", "", "", "Various options passed to the asbtraction-refinement engine (e.g. for PTA model checking)." }, + { BOOLEAN_TYPE, PRISM_PATH_VIA_AUTOMATA, "All path formulas via automata", "4.2.1", new Boolean(false), "", + "Handle all path formulas via automata constructions." }, // MULTI-OBJECTIVE MODEL CHECKING OPTIONS: { INTEGER_TYPE, PRISM_MULTI_MAX_POINTS, "Max. multi-objective corner points", "4.0.3", new Integer(50), "0,", "Maximum number of corner points to explore if (value iteration based) multi-objective model checking does not converge." }, @@ -1073,6 +1076,10 @@ public class PrismSettings implements Observer throw new PrismException("No parameter specified for -" + sw + " switch"); } } + // Handle all path formulas via automata constructions + else if (sw.equals("pathviaautomata")) { + set(PRISM_PATH_VIA_AUTOMATA, true); + } // MULTI-OBJECTIVE MODEL CHECKING OPTIONS: @@ -1505,6 +1512,7 @@ public class PrismSettings implements Observer mainLog.println("-sccmethod .............. Specify (symbolic) SCC computation method (xiebeerel, lockstep, sccfind)"); mainLog.println("-symm ................. Symmetry reduction options string"); mainLog.println("-aroptions ............ Abstraction-refinement engine options string"); + mainLog.println("-pathviaautomata ............... Handle all path formulas via automata constructions"); mainLog.println("-exportadv .............. Export an adversary from MDP model checking (as a DTMC)"); mainLog.println("-exportadvmdp ........... Export an adversary from MDP model checking (as an MDP)"); mainLog.println(); diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 49d5bbca..19fc6503 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -431,8 +431,18 @@ public class ProbModelChecker extends NonProbModelChecker protected StateValues checkProbPathFormula(Expression expr, boolean qual) throws PrismException { // Test whether this is a simple path formula (i.e. PCTL) - // and then pass control to appropriate method. - if (expr.isSimplePathFormula()) { + // and whether we want to use the corresponding algorithms + boolean useSimplePathAlgo = expr.isSimplePathFormula(); + + if (useSimplePathAlgo && + prism.getSettings().getBoolean(PrismSettings.PRISM_PATH_VIA_AUTOMATA) && + LTLModelChecker.isSupportedLTLFormula(model.getModelType(), expr)) { + // If PRISM_PATH_VIA_AUTOMATA is true, we want to use the LTL engine + // whenever possible + useSimplePathAlgo = false; + } + + if (useSimplePathAlgo) { return checkProbPathFormulaSimple(expr, qual); } else { return checkProbPathFormulaLTL(expr, qual);