From 83152265f56e899a86b7e3f569c5e670509a5935 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 1 Nov 2006 14:41:41 +0000
Subject: [PATCH] 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                   | 6 ++++++
 prism/src/prism/NondetModelChecker.java             | 4 ++--
 prism/src/prism/ProbModelChecker.java               | 4 ++--
 prism/src/prism/StochModelChecker.java              | 4 ++--
 prism/src/simulator/SimulatorEngine.java            | 4 ++--
 prism/src/userinterface/simulator/GUISimulator.java | 4 ++--
 6 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/prism/src/parser/ModulesFile.java b/prism/src/parser/ModulesFile.java
index 018404fb..0237956a 100644
--- a/prism/src/parser/ModulesFile.java
+++ b/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;
diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index decbf7cf..2b06abdf 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/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);
diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java
index 5c6be238..52d08391 100644
--- a/prism/src/prism/ProbModelChecker.java
+++ b/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);
diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java
index 7a3a0f15..cf136da1 100644
--- a/prism/src/prism/StochModelChecker.java
+++ b/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);
diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java
index 3cf0f772..00d1af7e 100644
--- a/prism/src/simulator/SimulatorEngine.java
+++ b/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;
diff --git a/prism/src/userinterface/simulator/GUISimulator.java b/prism/src/userinterface/simulator/GUISimulator.java
index 2073bb27..62b7bba2 100644
--- a/prism/src/userinterface/simulator/GUISimulator.java
+++ b/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);