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

@@ -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);

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) {

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