From e7b1416ad441446cc37d4a978c94d421093f1251 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 10 Dec 2009 08:03:45 +0000 Subject: [PATCH] Bugfix: errors in actions for adversary generation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1635 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/sparse/PS_NondetUntil.cc | 2 +- prism/src/sparse/sparse.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prism/src/sparse/PS_NondetUntil.cc b/prism/src/sparse/PS_NondetUntil.cc index b32edfdc..35312fe4 100644 --- a/prism/src/sparse/PS_NondetUntil.cc +++ b/prism/src/sparse/PS_NondetUntil.cc @@ -128,7 +128,7 @@ jboolean min // min or max probabilities (true = min, false = max) Cudd_Ref(maybe); tmp = DD_Apply(ddman, APPLY_TIMES, trans_actions, maybe); // then convert to a vector of integer indices - actions = build_nd_action_vector(ddman, trans, tmp, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); + actions = build_nd_action_vector(ddman, a, tmp, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd); Cudd_RecursiveDeref(ddman, tmp); kb = n*4.0/1024.0; kbt += kb; diff --git a/prism/src/sparse/sparse.cc b/prism/src/sparse/sparse.cc index 21e87897..4fd5a80e 100644 --- a/prism/src/sparse/sparse.cc +++ b/prism/src/sparse/sparse.cc @@ -869,7 +869,7 @@ int *build_nd_action_vector(DdManager *ddman, DdNode *mdp, DdNode *trans_actions matrices_bdds = new DdNode*[nm]; for (i = 0; i < nm; i++) { Cudd_Ref(matrices[i]); - matrices_bdds[i] = DD_Not(ddman, DD_Equals(ddman, matrices[i], 0)); + matrices_bdds[i] = DD_ThereExists(ddman, DD_Not(ddman, DD_Equals(ddman, matrices[i], 0)), cvars, num_vars); } // create arrays