Browse Source

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
master
Dave Parker 17 years ago
parent
commit
cf4dafcc41
  1. 5
      prism/src/mtbdd/PM_StochCumulReward.cc

5
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);

Loading…
Cancel
Save