From 3b68b5e0a949d293be2691d99f2d241f28a4855a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Aug 2016 17:59:10 +0000 Subject: [PATCH] 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 --- prism/src/sparse/PS_NondetMultiReachReward.cc | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/prism/src/sparse/PS_NondetMultiReachReward.cc b/prism/src/sparse/PS_NondetMultiReachReward.cc index 3bc51c96..a44a923e 100644 --- a/prism/src/sparse/PS_NondetMultiReachReward.cc +++ b/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);