Bug fix in new R=?[C<=k] code for DTMCs.

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

prism/src/hybrid/PH_ProbCumulReward.cc

@@ -76,6 +76,8 @@ jint bound			// time bound
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 
+	// mtbdds
+	DdNode *all_rewards;
 	// model stats
 	int n;
 	long nnz;
@@ -124,18 +126,17 @@ jint bound			// time bound
 	PH_PrintToMainLog(env, "[levels=%d, num=%d%s] [%.1f KB]\n", hddm->l_sm, hddm->num_sm, compact_sm?", compact":"", kb);
 	
 	// multiply transition rewards by transition probs and sum rows
-	// (note also filters out unwanted states at the same time)
-	Cudd_Ref(trans);
-	trans_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
-	trans_rewards = DD_SumAbstract(ddman, trans_rewards, cvars, num_cvars);
-	
-	// combine state and transition rewards and put in a vector
+	// then combine state and transition rewards and put in a vector
 	Cudd_Ref(trans_rewards);
-	state_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, trans_rewards);
+	Cudd_Ref(trans);
+	all_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
+	all_rewards = DD_SumAbstract(ddman, all_rewards, cvars, num_cvars);
+	Cudd_Ref(state_rewards);
+	all_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, all_rewards);
 
 	// get vector of rewards
 	PH_PrintToMainLog(env, "Creating vector for rewards... ");
-	rew_vec = mtbdd_to_double_vector(ddman, state_rewards, rvars, num_rvars, odd);
+	rew_vec = mtbdd_to_double_vector(ddman, all_rewards, rvars, num_rvars, odd);
 	// try and convert to compact form if required
 	compact_r = false;
 	if (compact) {
@@ -204,6 +205,7 @@ jint bound			// time bound
 	PH_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
 	
 	// free memory
+	Cudd_RecursiveDeref(ddman, all_rewards);
 	free_hdd_matrix(hddm);
 	if (compact_r) free_dist_vector(rew_dist); else free(rew_vec);
 	delete soln2;

prism/src/mtbdd/PM_ProbCumulReward.cc

@@ -60,7 +60,7 @@ jint bound				// time bound
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 
 	// mtbdds
-	DdNode *sol, *tmp;
+	DdNode *all_rewards, *sol, *tmp;
 	// timing stuff
 	long start1, start2, start3, stop;
 	double time_taken, time_for_setup, time_for_iters;
@@ -71,14 +71,13 @@ jint bound				// time bound
 	start1 = start2 = util_cpu_time();
 
 	// multiply transition rewards by transition probs and sum rows
-	// (note also filters out unwanted states at the same time)
-	Cudd_Ref(trans);
-	trans_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
-	trans_rewards = DD_SumAbstract(ddman, trans_rewards, cvars, num_cvars);
-	
-	// combine state and transition rewards and put in a vector
+	// then combine state and transition rewards and put in a vector
 	Cudd_Ref(trans_rewards);
-	state_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, trans_rewards);
+	Cudd_Ref(trans);
+	all_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
+	all_rewards = DD_SumAbstract(ddman, all_rewards, cvars, num_cvars);
+	Cudd_Ref(state_rewards);
+	all_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, all_rewards);
 
 	// initial solution is zero
 	sol = DD_Constant(ddman, 0);
@@ -103,8 +102,8 @@ jint bound				// time bound
 		Cudd_Ref(trans);
 		tmp = DD_MatrixMultiply(ddman, trans, tmp, cvars, num_cvars, MM_BOULDER);
 		// add in (combined state and transition) rewards
-		Cudd_Ref(state_rewards);
-		tmp = DD_Apply(ddman, APPLY_PLUS, tmp, state_rewards);
+		Cudd_Ref(all_rewards);
+		tmp = DD_Apply(ddman, APPLY_PLUS, tmp, all_rewards);
 		
 		// prepare for next iteration
 		Cudd_RecursiveDeref(ddman, sol);
@@ -121,6 +120,9 @@ jint bound				// time bound
 	// print iterations/timing info
 	PM_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
 	
+	// free memory
+	Cudd_RecursiveDeref(ddman, all_rewards);
+	
 	return ptr_to_jlong(sol);
 }
 

prism/src/sparse/PS_ProbCumulReward.cc

@@ -61,6 +61,8 @@ jint bound			// time bound
 	DdNode **rvars = jlong_to_DdNode_array(rv);	// row vars
 	DdNode **cvars = jlong_to_DdNode_array(cv);	// col vars
 
+	// mtbdds
+	DdNode *all_rewards;
 	// model stats
 	int n;
 	long nnz;
@@ -108,18 +110,17 @@ jint bound			// time bound
 	PS_PrintToMainLog(env, "[%.1f KB]\n", kb);
 	
 	// multiply transition rewards by transition probs and sum rows
-	// (note also filters out unwanted states at the same time)
-	Cudd_Ref(trans);
-	trans_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
-	trans_rewards = DD_SumAbstract(ddman, trans_rewards, cvars, num_cvars);
-	
-	// combine state and transition rewards and put in a vector
+	// then combine state and transition rewards and put in a vector
 	Cudd_Ref(trans_rewards);
-	state_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, trans_rewards);
+	Cudd_Ref(trans);
+	all_rewards = DD_Apply(ddman, APPLY_TIMES, trans_rewards, trans);
+	all_rewards = DD_SumAbstract(ddman, all_rewards, cvars, num_cvars);
+	Cudd_Ref(state_rewards);
+	all_rewards = DD_Apply(ddman, APPLY_PLUS, state_rewards, all_rewards);
 
 	// get vector of rewards
 	PS_PrintToMainLog(env, "Creating vector for rewards... ");
-	rew_vec = mtbdd_to_double_vector(ddman, state_rewards, rvars, num_rvars, odd);
+	rew_vec = mtbdd_to_double_vector(ddman, all_rewards, rvars, num_rvars, odd);
 	// try and convert to compact form if required
 	compact_r = false;
 	if (compact) {
@@ -226,6 +227,7 @@ jint bound			// time bound
 	PS_PrintToMainLog(env, "\nIterative method: %d iterations in %.2f seconds (average %.6f, setup %.2f)\n", iters, time_taken, time_for_iters/iters, time_for_setup);
 	
 	// free memory
+	Cudd_RecursiveDeref(ddman, all_rewards);
 	if (compact_tr) free_cmsr_sparse_matrix(cmsrsm); else free_rm_sparse_matrix(rmsm);
 	if (compact_r) free_dist_vector(rew_dist); else free(rew_vec);
 	delete soln2;