Added `cumulative reward' information to the simulator engine (the c++ part), untested and not used... yet.

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

prism/include/simengine.h

@@ -101,6 +101,10 @@ double Engine_Get_State_Reward_Of_Path_State(int state_index);
 
 double Engine_Get_Transition_Reward_Of_Path_State(int state_index);
 
+double Engine_Get_Total_State_Reward_Of_Path_State(int state_index);
+
+double Engine_Get_Total_Transition_Reward_Of_Path_State(int state_index);
+
 double Engine_Get_Total_Path_Time();
 
 double Engine_Get_Total_Path_Reward();

prism/include/simpath.h

@@ -182,6 +182,10 @@ double Get_State_Reward_Of_Path_State(int state_index, int i);
  */
 double Get_Transition_Reward_Of_Path_State(int state_index, int i);
 
+double Get_Total_State_Reward_Of_Path_State(int state_index, int i);
+
+double Get_Total_Transition_Reward_Of_Path_State(int state_index, int i);
+
 /*
  *	Returns the total time for the path.
  */

prism/include/simstate.h

@@ -72,8 +72,10 @@ class CPathState
 		bool time_known; 
 		double *state_cost; //The costs accumulated in that state (for real time models)
 		double *state_instant_cost; //The instant state costs of that state
-		double *path_cost_so_far; //The costs of the path so far up until that state
 		double *transition_cost; //The costs of the transition out of that state
+		
+		double *cumulative_state_cost; // Cumulative state_cost upto now.
+		double *cumulative_transition_cost; // Cumulative transition_cost.
 
 	/*
 	 *	Constructs the state according with no_state_variables storage spaces 

prism/src/simulator/SimulatorEngine.cc

@@ -261,6 +261,18 @@ JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTransitionRewardOfPa
 	return Get_Transition_Reward_Of_Path_State(stateIndex, i);
 }
 
+JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalStateRewardOfPathState
+(JNIEnv *env, jclass cls, jint stateIndex, jint i)
+{
+	return Get_Total_State_Reward_Of_Path_State(stateIndex, i);
+}
+
+JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalTransitionRewardOfPathState
+(JNIEnv *env, jclass cls, jint stateIndex, jint i)
+{
+	return Get_Total_Transition_Reward_Of_Path_State(stateIndex, i);
+}
+
 JNIEXPORT jdouble JNICALL Java_simulator_SimulatorEngine_getTotalPathTime
 (JNIEnv *env, jclass cls)
 {

prism/src/simulator/SimulatorEngine.java

@@ -949,6 +949,16 @@ public class SimulatorEngine
 	 */
 	public static native double getTransitionRewardOfPathState(int stateIndex, int i);
 	
+	/**
+	 * Cumulative version of getStateRewardOfPathState.
+	 */
+	public static native double getTotalStateRewardOfPathState(int stateIndex, int i);
+	
+	/**
+	 * Cumulative version of getTransitionRewardOfPathState.
+	 */
+	public static native double getTotalTransitionRewardOfPathState(int stateIndex, int i);	
+	
 	/**
 	 * Returns the total path time.
 	 * @return the total path time.

prism/src/simulator/simengine.cc

@@ -255,6 +255,16 @@ double Engine_Get_Transition_Reward_Of_Path_State(int state_index, int i)
 	return Get_Transition_Reward_Of_Path_State(state_index, i);
 }
 
+double Engine_Get_Total_Transition_Reward_Of_Path_State(int state_index, int i)
+{
+	return Get_Total_Transition_Reward_Of_Path_State(state_index, i);
+}
+
+double Engine_Get_Total_State_Reward_Of_Path_State(int state_index, int i)
+{
+	return Get_Total_State_Reward_Of_Path_State(state_index, i);
+}
+
 double Engine_Get_Total_Path_Time()
 {
 	return Get_Total_Path_Time();

prism/src/simulator/simpath.cc

@@ -583,6 +583,20 @@ double Get_Transition_Reward_Of_Path_State(int state_index, int i)
 		return stored_path[state_index]->transition_cost[i];
 }
 
+double Get_Total_State_Reward_Of_Path_State(int state_index, int i)
+{
+	if(state_index > current_index) return UNDEFINED_DOUBLE;
+	else
+		return stored_path[state_index]->cumulative_state_cost[i];
+}
+
+double Get_Total_Transition_Reward_Of_Path_State(int state_index, int i)
+{
+	if(state_index > current_index) return UNDEFINED_DOUBLE;
+	else
+		return stored_path[state_index]->cumulative_transition_cost[i];
+}
+
 bool Is_Proven_Looping()
 {
 	return loop_detection->Is_Proven_Looping();
@@ -701,7 +715,9 @@ inline void Add_Current_State_To_Path()
 				total_state_cost[i] += last_state->state_instant_cost[i]*time_in_state;
 				total_transition_cost[i] += Get_Transition_Reward(i);
 				path_cost[i] = total_state_cost[i] + total_transition_cost[i];
-				last_state->path_cost_so_far[i] = path_cost[i];
+				
+				last_state->cumulative_state_cost[i] = total_state_cost[i];
+				last_state->cumulative_transition_cost[i] = total_transition_cost[i];				
 			}
 			
 			Notify_Path_Formulae(last_state, state_variables, loop_detection);
@@ -718,7 +734,9 @@ inline void Add_Current_State_To_Path()
 				total_state_cost[i] += last_state->state_instant_cost[i];
 				total_transition_cost[i] += Get_Transition_Reward(i);
 				path_cost[i] = total_state_cost[i] + total_transition_cost[i];
-				last_state->path_cost_so_far[i] = path_cost[i];
+				
+				last_state->cumulative_state_cost[i] = total_state_cost[i];
+				last_state->cumulative_transition_cost[i] = total_transition_cost[i];
 			}
 			
 			Notify_Path_Formulae(last_state, state_variables, loop_detection); 

prism/src/simulator/simpctl.cc

@@ -607,7 +607,10 @@ void CRewardCumulative::Notify_State(CPathState* last_state, int* current_state)
 				//time occured in last state
 				answer_known = true;
 				if (reward_struct_index >= 0 && reward_struct_index < no_reward_structs) {
-					answer_double = last_state->path_cost_so_far[reward_struct_index] - last_state->transition_cost[reward_struct_index] + last_state->state_instant_cost[reward_struct_index] * (time - time_so_far);
+					answer_double = 
+						last_state->cumulative_state_cost[reward_struct_index] + last_state->cumulative_transition_cost[reward_struct_index] - 
+							last_state->transition_cost[reward_struct_index] + 
+							last_state->state_instant_cost[reward_struct_index] * (time - time_so_far);
 				} else {
 					answer_double = 0.0;
 				}
@@ -616,7 +619,8 @@ void CRewardCumulative::Notify_State(CPathState* last_state, int* current_state)
 			{
 				answer_known = true;
 				if (reward_struct_index >= 0 && reward_struct_index < no_reward_structs) {
-					answer_double = last_state->path_cost_so_far[reward_struct_index];
+					answer_double = 
+						last_state->cumulative_state_cost[reward_struct_index] + last_state->cumulative_transition_cost[reward_struct_index];
 				} else {
 					answer_double = 0.0;
 				}
@@ -631,7 +635,7 @@ void CRewardCumulative::Notify_State(CPathState* last_state, int* current_state)
 			{
 				answer_known = true;
 				if (reward_struct_index >= 0 && reward_struct_index < no_reward_structs) {
-					answer_double = last_state->path_cost_so_far[reward_struct_index];
+					answer_double = last_state->cumulative_state_cost[reward_struct_index] + last_state->cumulative_transition_cost[reward_struct_index];
 				} else {
 					answer_double = 0.0;
 				}
@@ -883,7 +887,7 @@ void CRewardReachability::Notify_State(CPathState* last_state, int* current_stat
 	{
 		answer_known = true;
 		if (reward_struct_index >= 0 && reward_struct_index < no_reward_structs) {
-			answer_double = last_state->path_cost_so_far[reward_struct_index];//Get_Path_Cost_No_Path();									
+			answer_double = last_state->cumulative_state_cost[reward_struct_index] + last_state->cumulative_transition_cost[reward_struct_index];//Get_Path_Cost_No_Path();									
 		} else {
 			answer_double = 0.0;
 		}

prism/src/simulator/simsampling.cc

@@ -666,7 +666,9 @@ void Do_Sampling(int path_length)
 					total_state_cost[i] += last_state->state_instant_cost[i]*time_in_state;
 					total_transition_cost[i] += last_state->transition_cost[i];
 					path_cost[i] = total_state_cost[i] + total_transition_cost[i];
-					last_state->path_cost_so_far[i] = path_cost[i];
+					
+					last_state->cumulative_state_cost[i] = total_state_cost[i];
+					last_state->cumulative_transition_cost[i] = total_transition_cost[i];
 				}
 				
 				Notify_Path_Formulae(last_state, state_variables, loop_detection);
@@ -679,7 +681,9 @@ void Do_Sampling(int path_length)
 					total_state_cost[i] += last_state->state_instant_cost[i];
 					total_transition_cost[i] += last_state->transition_cost[i];
 					path_cost[i] = total_state_cost[i] + total_transition_cost[i];
-					last_state->path_cost_so_far[i] = path_cost[i];
+					
+					last_state->cumulative_state_cost[i] = total_state_cost[i];
+					last_state->cumulative_transition_cost[i] = total_transition_cost[i];	
 				}
 				
 				Notify_Path_Formulae(last_state, state_variables, loop_detection); 

prism/src/simulator/simstate.cc

@@ -89,15 +89,22 @@ CPathState::CPathState()
 	this->time_spent_in_state = 0.0;
 	this->time_known = false;
 	this->state_cost = new double[no_reward_structs];
-	this->state_instant_cost = new double[no_reward_structs];
-	this->path_cost_so_far = new double[no_reward_structs];
+	this->state_instant_cost = new double[no_reward_structs];	
 	this->transition_cost = new double[no_reward_structs];
-	for(int i = 0; i < no_reward_structs; i++) {
+	
+	this->cumulative_state_cost = new double[no_reward_structs];
+	this->cumulative_transition_cost = new double[no_reward_structs];
+	
+	for(int i = 0; i < no_reward_structs; i++) 
+	{
 		this->state_cost[i] = 0.0;
-		this->state_instant_cost[i] = 0.0;
-		this->path_cost_so_far[i] = 0.0;
+		this->state_instant_cost[i] = 0.0;		
 		this->transition_cost[i] = 0.0;
+		
+		this->cumulative_state_cost[i] = 0.0;
+		this->cumulative_transition_cost[i] = 0.0;
 	}
+	
 	this->probability = 0.0;
 }
 
@@ -108,9 +115,11 @@ CPathState::~CPathState()
 {
 	if(variables != NULL) delete[] variables;
 	if(state_cost != NULL) delete[] state_cost;
-	if(state_instant_cost != NULL) delete[] state_instant_cost;
-	if(path_cost_so_far != NULL) delete[] path_cost_so_far;
+	if(state_instant_cost != NULL) delete[] state_instant_cost;	
 	if(transition_cost != NULL) delete[] transition_cost;
+	
+	if(cumulative_state_cost != NULL) delete[] cumulative_state_cost;
+	if(cumulative_transition_cost != NULL) delete[] cumulative_transition_cost;	
 }
 
 /*
@@ -123,10 +132,12 @@ void CPathState::Make_This_Current_State()
 		variables[i] = state_variables[i];
 	this->time_spent_in_state = 0.0;
 	this->time_known = false;
+	
 	for(int i = 0; i < no_reward_structs; i++) {
 		this->state_cost[i] = 0.0;
 		this->state_instant_cost[i] = 0.0;
-		this->path_cost_so_far[i] = 0.0;
+		this->cumulative_state_cost[i] = 0.0;
+		this->cumulative_transition_cost[i] = 0.0;
 		this->transition_cost[i] = 0.0;
 	}
 	this->probability = 0.0;