From cf4dafcc4186a8566cbfe3da77decba9814071b7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 25 Nov 2008 14:00:52 +0000 Subject: [PATCH] Bug fix (CTMC cumulative rewards with rewards on self-loops) (MTBDD engine). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@828 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/mtbdd/PM_StochCumulReward.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/prism/src/mtbdd/PM_StochCumulReward.cc b/prism/src/mtbdd/PM_StochCumulReward.cc index 31f359b5..8a6b5514 100644 --- a/prism/src/mtbdd/PM_StochCumulReward.cc +++ b/prism/src/mtbdd/PM_StochCumulReward.cc @@ -115,11 +115,10 @@ jdouble time // time bound PM_PrintToMainLog(env, "[nodes=%d] [%.1f Kb]\n", i, i*20.0/1024.0); // combine state/transition rewards into a single vector - this is the initial solution vector - Cudd_Ref(q); + Cudd_Ref(trans); Cudd_Ref(trans_rewards); - sol = DD_Apply(ddman, APPLY_TIMES, q, trans_rewards); + sol = DD_Apply(ddman, APPLY_TIMES, trans, trans_rewards); sol = DD_SumAbstract(ddman, sol, cvars, num_cvars); - sol = DD_Apply(ddman, APPLY_TIMES, sol, DD_Constant(ddman, unif)); Cudd_Ref(state_rewards); sol = DD_Apply(ddman, APPLY_PLUS, sol, state_rewards);