Changed handling of multiple reward structures so is 1-indexed from properties, etc.

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

prism/src/parser/ModulesFile.java

@@ -150,8 +150,14 @@ public class ModulesFile
 	
 	public int getNumRewardStructs() { return rewardStructs.size(); }
 	
+	// Get a reward structure by its index
+	// (indexed from 0, not from 1 like at the user (property language) level)
+	
 	public RewardStruct getRewardStruct(int i) { return (i<rewardStructs.size()) ? (RewardStruct)rewardStructs.get(i) : null; }
 	
+	// Get the index of a module by its name
+	// (indexed from 0, not from 1 like at the user (property language) level)
+	
 	public int getRewardStructIndex(String name)
 	{
 		int i, n;

prism/src/prism/NondetModelChecker.java

@@ -651,8 +651,8 @@ public class NondetModelChecker implements ModelChecker
 		else if (rs instanceof Expression) {
 			i = ((Expression)rs).evaluateInt(constantValues, null);
 			rs = new Integer(i); // for better error reporting below
-			stateRewards = model.getStateRewards(i);
-			transRewards = model.getTransRewards(i);
+			stateRewards = model.getStateRewards(i - 1);
+			transRewards = model.getTransRewards(i - 1);
 		}
 		else if (rs instanceof String) {
 			stateRewards = model.getStateRewards((String)rs);

prism/src/prism/ProbModelChecker.java

@@ -663,8 +663,8 @@ public class ProbModelChecker implements ModelChecker
 		else if (rs instanceof Expression) {
 			i = ((Expression)rs).evaluateInt(constantValues, null);
 			rs = new Integer(i); // for better error reporting below
-			stateRewards = model.getStateRewards(i);
-			transRewards = model.getTransRewards(i);
+			stateRewards = model.getStateRewards(i - 1);
+			transRewards = model.getTransRewards(i - 1);
 		}
 		else if (rs instanceof String) {
 			stateRewards = model.getStateRewards((String)rs);

prism/src/prism/StochModelChecker.java

@@ -687,8 +687,8 @@ public class StochModelChecker implements ModelChecker
 		else if (rs instanceof Expression) {
 			i = ((Expression)rs).evaluateInt(constantValues, null);
 			rs = new Integer(i); // for better error reporting below
-			stateRewards = model.getStateRewards(i);
-			transRewards = model.getTransRewards(i);
+			stateRewards = model.getStateRewards(i - 1);
+			transRewards = model.getTransRewards(i - 1);
 		}
 		else if (rs instanceof String) {
 			stateRewards = model.getStateRewards((String)rs);

prism/src/simulator/SimulatorEngine.java

@@ -1077,7 +1077,7 @@ public class SimulatorEngine
 		if (nr == 1) {
 			log.print(colSep+"state_reward"+colSep+"transition_reward");
 		} else {
-			for(j = 0; j < nr; j++) log.print(colSep+"state_reward"+j+colSep+"transition_reward"+j);
+			for(j = 0; j < nr; j++) log.print(colSep+"state_reward"+(j+1)+colSep+"transition_reward"+(j+1));
 		}
 		log.println();
 		
@@ -1945,7 +1945,7 @@ public class SimulatorEngine
 		}
 		else if (rs instanceof Expression) {
 			try {
-				rsi = ((Expression)rs).evaluateInt(allConstants, null);
+				rsi = ((Expression)rs).evaluateInt(allConstants, null) - 1;
 			} catch(PrismException e) {
 				System.err.println("Property: "+operand.toString()+" could not be used in the simulator because: \n"+ e.toString());
 				return -1;

prism/src/userinterface/simulator/GUISimulator.java

@@ -2515,7 +2515,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 						else if(column > n+1) //rewards
 						{
 							int i = column-(n+2);
-							return "" + ((i%2 == 0)?"Sta.":"Tra.") + " Rew. "+(i/2);
+							return "" + ((i%2 == 0)?"Sta.":"Tra.") + " Rew. "+((i/2)+1);
 						}
 					}
 					else
@@ -2524,7 +2524,7 @@ public class GUISimulator extends GUIPlugin implements MouseListener, ListSelect
 						if(column > n) //rewards
 						{
 							int i = column-(n+1);
-							return "" + ((i%2 == 0)?"Sta.":"Tra.") + " Rew. "+(i/2);
+							return "" + ((i%2 == 0)?"Sta.":"Tra.") + " Rew. "+((i/2)+1);
 						}
 					}
 					return engine.getVariableName(column-1);