From 45b837567b97999f40139a04332a12dfce7f395d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 10 Feb 2016 10:31:24 +0000 Subject: [PATCH] explicit.CTMCModelChecker: fix handling of PCTL* subformulas Previously, subformulas were computed by a DTMCModelChecker in the embedded DTMC, yielding wrong results. Now, maximal state subformulas are checked via the CTMCModelChecker and replaced by labels before calling the LTL model checking routine on the embedded DTMC. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11168 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 27 ++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 639558fe..ccdacd7c 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -54,16 +54,35 @@ public class CTMCModelChecker extends ProbModelChecker @Override protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException { - // Construct embedded DTMC and do computation on that + if (!(model instanceof ModelExplicit)) { + // needs a ModelExplicit to allow attaching labels in the handleMaximalStateFormulas step + throw new PrismNotSupportedException("Need CTMC with ModelExplicit for LTL checking"); + } + // we first handle the sub-formulas by computing their satisfaction sets, + // attaching them as labels to the model and modifying the formula + // appropriately + expr = handleMaximalStateFormulas((ModelExplicit) model, expr); + + // Now, we construct embedded DTMC and do the plain LTL computation on that mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); return createDTMCModelChecker().checkProbPathFormulaLTL(dtmcEmb, expr, qual, minMax, statesOfInterest); } - + @Override protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { - // Construct embedded DTMC (and convert rewards for it) and do computation on that + if (!(model instanceof ModelExplicit)) { + // needs a ModelExplicit to allow attaching labels in the handleMaximalStateFormulas step + throw new PrismNotSupportedException("Need CTMC with ModelExplicit for cosafety LTL reward checking"); + } + // we first handle the sub-formulas by computing their satisfaction sets, + // attaching them as labels to the model and modifying the formula + // appropriately + expr = handleMaximalStateFormulas((ModelExplicit) model, expr); + + // Construct embedded DTMC (and convert rewards for it) and do remaining computation + // on that with the "pure" cosafety LTL formula mainLog.println("Building embedded DTMC..."); DTMC dtmcEmb = ((CTMC)model).getImplicitEmbeddedDTMC(); int n = model.getNumStates(); @@ -73,7 +92,7 @@ public class CTMCModelChecker extends ProbModelChecker } return createDTMCModelChecker().checkRewardCoSafeLTL(dtmcEmb, rewEmb, expr, minMax, statesOfInterest); } - + @Override protected StateValues checkProbBoundedUntil(Model model, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException {