From c5deedebbba7e64d125098da39ec8d02f004dbc7 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 19 Jul 2017 12:35:17 +0000 Subject: [PATCH] prism.StochModelChecker: handle co-safe LTL reward computation for CTMCs git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12068 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/StochModelChecker.java | 32 ++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index edd5ddec..d7fd13d8 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -315,6 +315,38 @@ public class StochModelChecker extends ProbModelChecker return rewards; } + + @Override + protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, JDDNode statesOfInterest) throws PrismException + { + // compute state sets for the maximal state formulas, + // attach as fresh labels which replace the state formulas in + // expr + expr = handleMaximalStateFormulas(expr); + + // Compute embedded Markov chain, don't convert reward structures of the + // model, as we use the rewards given as parameters + ProbModel embeddedDTMC = ((StochModel)model).getEmbeddedDTMC(mainLog, false); + + JDDNode stateRewardsDTMC = null; + try { + // state rewards are scaled, nothing to do for transition rewards + JDDNode diags = JDD.SumAbstract(trans.copy(), allDDColVars); + stateRewardsDTMC = JDD.Apply(JDD.DIVIDE, stateRewards.copy(), diags); + + ProbModelChecker embeddedMC = (ProbModelChecker) createModelChecker(embeddedDTMC); + StateValues sv = embeddedMC.checkRewardCoSafeLTL(expr, stateRewardsDTMC, transRewards, statesOfInterest); + + // update the model in the StateValues object back to the CTMC + sv.switchModel(model); + return sv; + } finally { + embeddedDTMC.clear(); + if (stateRewardsDTMC != null) + JDD.Deref(stateRewardsDTMC); + } + } + // ----------------------------------------------------------------------------------- // do transient computation // -----------------------------------------------------------------------------------