From 7178fdd937b1b71b7b94f76849f2dcd9b37e1a6a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 26 Jan 2010 10:16:58 +0000 Subject: [PATCH] Bugfix: action info storage for MDPs. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1715 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/sparse/sparse.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/prism/src/sparse/sparse.cc b/prism/src/sparse/sparse.cc index 4fd5a80e..a39cf4b2 100644 --- a/prism/src/sparse/sparse.cc +++ b/prism/src/sparse/sparse.cc @@ -889,11 +889,14 @@ int *build_nd_action_vector(DdManager *ddman, DdNode *mdp, DdNode *trans_actions starts[i] += starts[i-1]; } - // initialise (unnecessarily) the 'actions' array + // initialise the 'actions' array + // (necessary because tau actions, with index 0, are not discovered + // by the call to traverse_mtbdd_vect_rec(..., 3) below) for (i = 0; i < nc; i++) actions[i] = 0; // now traverse the mtbdd to get the actual entries (action indices) for (i = 0; i < nm; i++) { traverse_mtbdd_vect_rec(ddman, submatrices[i], rvars, num_vars, 0, odd, 0, 3); + traverse_mtbdd_vect_rec(ddman, matrices_bdds[i], rvars, num_vars, 0, odd, 0, 2); } // try/catch for memory allocation/deallocation @@ -1157,7 +1160,6 @@ void traverse_mtbdd_vect_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int nu // mdp action vector - single pass case 3: actions[starts[i]] = (int)Cudd_V(dd); - starts[i]++; break; }