Small fixes in explicit rewards.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3375 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/CTMCModelChecker.java

@@ -31,7 +31,7 @@ import java.util.*;
 import jdd.JDD;
 
 import explicit.rewards.MCRewards;
-import explicit.rewards.MCRewardsStateArray;
+import explicit.rewards.StateRewardsArray;
 import parser.ast.*;
 import parser.type.*;
 import prism.*;
@@ -374,7 +374,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		DTMC dtmcEmb = ((CTMC) dtmc).buildImplicitEmbeddedDTMC();
 		// Convert rewards
 		n = dtmc.getNumStates();
-		MCRewardsStateArray rewEmb = new MCRewardsStateArray(n);
+		StateRewardsArray rewEmb = new StateRewardsArray(n);
 		for (i = 0; i < n; i++) {
 			rewEmb.setStateReward(i, mcRewards.getStateReward(i) / ((CTMC) dtmc).getExitRate(i));
 		}

prism/src/explicit/ProbModelChecker.java

@@ -196,7 +196,7 @@ public class ProbModelChecker extends StateModelChecker
 		switch (modelType) {
 		case CTMC:
 		case DTMC:
-			mcRewards = constructRewards.buildMCRewardStructure(model, rewStruct, constantValues);
+			mcRewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues);
 			break;
 		case MDP:
 			mdpRewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues);

prism/src/explicit/rewards/ConstructRewards.java

@@ -35,8 +35,7 @@ import parser.ast.RewardStruct;
 import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLog;
-import explicit.MDP;
-import explicit.Model;
+import explicit.*;
 
 public class ConstructRewards
 {
@@ -54,17 +53,18 @@ public class ConstructRewards
 
 	/**
 	 * Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure. 
-	 * @param model The DTMC or CTMC
+	 * @param mc The DTMC or CTMC
 	 * @param rewStr The reward structure
 	 * @param constantValues Values for any undefined constants needed
 	 */
-	public MCRewards buildMCRewardStructure(Model model, RewardStruct rewStr, Values constantValues) throws PrismException
+	public MCRewards buildMCRewardStructure(DTMC mc, RewardStruct rewStr, Values constantValues) throws PrismException
 	{
 		List<State> statesList;
 		Expression guard;
 		int i, j, n, numStates;
 
 		if (rewStr.getNumTransItems() > 0) {
+			// TODO
 			throw new PrismException("Explicit engine does not yet handle transition rewards for D/CTMCs");
 		}
 		// Special case: constant rewards
@@ -73,9 +73,9 @@ public class ConstructRewards
 		}
 		// Normal: state rewards
 		else {
-			numStates = model.getNumStates();
-			statesList = model.getStatesList();
-			MCRewardsStateArray rewSA = new MCRewardsStateArray(numStates);
+			numStates = mc.getNumStates();
+			statesList = mc.getStatesList();
+			StateRewardsArray rewSA = new StateRewardsArray(numStates);
 			n = rewStr.getNumItems();
 			for (i = 0; i < n; i++) {
 				guard = rewStr.getStates(i);
@@ -90,8 +90,8 @@ public class ConstructRewards
 	}
 
 	/**
-	 * Construct the rewards for a Markov chain (DTMC or CTMC) from a model and reward structure. 
-	 * @param model The DTMC or CTMC
+	 * Construct the rewards for an MDP from a model and reward structure. 
+	 * @param model The MDP
 	 * @param rewStr The reward structure
 	 * @param constantValues Values for any undefined constants needed
 	 */

prism/src/explicit/rewards/MCRewardsStateConstant.java

@@ -1,57 +0,0 @@
-//==============================================================================
-//	
-//	Copyright (c) 2002-
-//	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
-//	
-//------------------------------------------------------------------------------
-//	
-//	This file is part of PRISM.
-//	
-//	PRISM is free software; you can redistribute it and/or modify
-//	it under the terms of the GNU General Public License as published by
-//	the Free Software Foundation; either version 2 of the License, or
-//	(at your option) any later version.
-//	
-//	PRISM is distributed in the hope that it will be useful,
-//	but WITHOUT ANY WARRANTY; without even the implied warranty of
-//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-//	GNU General Public License for more details.
-//	
-//	You should have received a copy of the GNU General Public License
-//	along with PRISM; if not, write to the Free Software Foundation,
-//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
-//	
-//==============================================================================
-
-package explicit.rewards;
-
-/**
- * Explicit-state storage of constant state rewards for a DTMC/CTMC.
- */
-public class MCRewardsStateConstant implements MCRewards, MDPRewards
-{
-	protected double stateReward = 0.0;
-	
-	/**
-	 * Constructor: all rewards equal to {@code r}
-	 */
-	public MCRewardsStateConstant(double r)
-	{
-		stateReward = r;
-	}
-	
-	// Accessors
-	
-	@Override
-	public double getStateReward(int s)
-	{
-		return stateReward;
-	}
-	
-	@Override
-	public double getTransitionReward(int s, int i)
-	{
-		return 0.0;
-	}
-}

prism/src/explicit/rewards/MCRewardsStateArray.java → prism/src/explicit/rewards/StateRewardsArray.java

@@ -27,9 +27,9 @@
 package explicit.rewards;
 
 /**
- * Explicit-state storage of just state rewards for a DTMC/CTMC (as an array).
+ * Explicit-state storage of just state rewards (as an array).
  */
-public class MCRewardsStateArray implements MCRewards, MDPRewards
+public class StateRewardsArray implements MCRewards, MDPRewards
 {
 	/** Array of state rewards **/
 	protected double stateRewards[] = null;
@@ -38,7 +38,7 @@ public class MCRewardsStateArray implements MCRewards, MDPRewards
 	 * Constructor: all zero rewards.
 	 * @param numStates Number of states
 	 */
-	public MCRewardsStateArray(int numStates)
+	public StateRewardsArray(int numStates)
 	{
 		stateRewards = new double[numStates];
 		for (int i = 0; i < numStates; i++)