Bugfix: errors in actions for adversary generation.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1635 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago · e7b1416ad4
2 changed files with 2 additions and 2 deletions
--- 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;
--- 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