From cd0ebbde5b2d3bc0ffb6e4c4d3be39274060f906 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 23 Apr 2007 09:19:33 +0000 Subject: [PATCH] =?UTF-8?q?Bug=20fix=20in=20new=20R=3D=3F[C<=3Dk]=20code?= =?UTF-8?q?=20for=20DTMCs.?= git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@291 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/hybrid/PH_ProbCumulReward.cc | 20 +++++++++++--------- prism/src/mtbdd/PM_ProbCumulReward.cc | 24 +++++++++++++----------- prism/src/sparse/PS_ProbCumulReward.cc | 20 +++++++++++--------- 3 files changed, 35 insertions(+), 29 deletions(-) diff --git a/prism/src/hybrid/PH_ProbCumulReward.cc b/prism/src/hybrid/PH_ProbCumulReward.cc index 01642cec..36292a2f 100644 --- a/prism/src/hybrid/PH_ProbCumulReward.cc +++ b/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; diff --git a/prism/src/mtbdd/PM_ProbCumulReward.cc b/prism/src/mtbdd/PM_ProbCumulReward.cc index 911e2369..b5c99a89 100644 --- a/prism/src/mtbdd/PM_ProbCumulReward.cc +++ b/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,15 +71,14 @@ 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); } diff --git a/prism/src/sparse/PS_ProbCumulReward.cc b/prism/src/sparse/PS_ProbCumulReward.cc index c43dce48..7f900ab8 100644 --- a/prism/src/sparse/PS_ProbCumulReward.cc +++ b/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;