Browse Source

Bug fix: respect disable_selfloop setting during adversary generation in LP-based multi-objective model checking.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11761 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 10 years ago
parent
commit
3b68b5e0a9
  1. 6
      prism/src/sparse/PS_NondetMultiReachReward.cc

6
prism/src/sparse/PS_NondetMultiReachReward.cc

@ -225,8 +225,10 @@ JNIEXPORT jdouble __jlongpointer JNICALL Java_sparse_PrismSparse_PS_1NondetMulti
Cudd_Ref(trans_actions);
Cudd_Ref(maybe_yes);
tmp = DD_Apply(ddman, APPLY_TIMES, trans_actions, maybe_yes);
Cudd_Ref(loops);
tmp = DD_ITE(ddman, loops, DD_Constant(ddman, 0), tmp);
if (!disable_selfloop) {
Cudd_Ref(loops);
tmp = DD_ITE(ddman, loops, DD_Constant(ddman, 0), tmp);
}
// then convert to a vector of integer indices
build_nd_action_vector(ddman, a, tmp, ndsm, rvars, cvars, num_rvars, ndvars, num_ndvars, odd);
Cudd_RecursiveDeref(ddman, tmp);

Loading…
Cancel
Save