From 6166413a204cf88cfa26e834ef441fb17501124b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 22 Jun 2011 11:53:38 +0000 Subject: [PATCH] Bug fixes in explicit expected reward on embedded DTMCs from CTMCs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3134 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/CTMCModelChecker.java | 2 +- prism/src/explicit/ConstructModel.java | 2 +- prism/src/explicit/DTMCEmbeddedSimple.java | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 55080223..f30877ac 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -373,7 +373,7 @@ public class CTMCModelChecker extends DTMCModelChecker n = dtmc.getNumStates(); MCRewardsStateArray rewEmb = new MCRewardsStateArray(n); for (i = 0; i < n; i++) { - rewEmb.setStateReward(i, mcRewards.getStateReward(i) * ((CTMC) dtmc).getExitRate(i)); + rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ((CTMC) dtmc).getExitRate(i)); } // Do computation on DTMC return super.computeReachRewards(dtmcEmb, rewEmb, target); diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 96791c62..a1ff7b8f 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -106,7 +106,7 @@ public class ConstructModel boolean fixdl = false; // For now, don't use sparse (so can use actions) (TODO: fix) - buildSparse = false; + //buildSparse = false; // Don't support multiple initial states if (modulesFile.getInitialStates() != null) { diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 28daee6c..9103c673 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/prism/src/explicit/DTMCEmbeddedSimple.java @@ -368,8 +368,8 @@ public class DTMCEmbeddedSimple implements DTMC Distribution distr; distr = ctmc.getTransitions(s); - d = mcRewards.getStateReward(s); er = exitRates[s]; + d = 0; // Exit rate 0: prob 1 self-loop if (er == 0) { d += vect[s]; @@ -383,6 +383,7 @@ public class DTMCEmbeddedSimple implements DTMC } d /= er; } + d += mcRewards.getStateReward(s); return d; }