diff --git a/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args b/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args index 90261950..fecd1a44 100644 --- a/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args +++ b/prism-tests/functionality/verify/mdps/reach/mdp_simple.nm.props.args @@ -5,3 +5,8 @@ -ex -gs -ex -politer -ex -modpoliter +-s -ii +-m -ii +-h -ii +-ex -valiter -ii +-ex -gs -ii diff --git a/prism/src/sparse/PS_NondetReachRewardInterval.cc b/prism/src/sparse/PS_NondetReachRewardInterval.cc index e0d0124c..bc6e6875 100644 --- a/prism/src/sparse/PS_NondetReachRewardInterval.cc +++ b/prism/src/sparse/PS_NondetReachRewardInterval.cc @@ -395,7 +395,7 @@ jint flags } // set vector element // (if there were no choices from this state, reward is zero/infinity) - helper.updateValueFromBelow(soln_above2[i], soln_above[i], (h1 > l1) ? d1 : inf_vec[i] > 0 ? HUGE_VAL : 0); + helper.updateValueFromAbove(soln_above2[i], soln_above[i], (h1 > l1) ? d1 : inf_vec[i] > 0 ? HUGE_VAL : 0); } if (iterationExport) {