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; }