diff --git a/prism/src/mtbdd/PM_ProbReachReward.cc b/prism/src/mtbdd/PM_ProbReachReward.cc index ddace78c..b38f6db6 100644 --- a/prism/src/mtbdd/PM_ProbReachReward.cc +++ b/prism/src/mtbdd/PM_ProbReachReward.cc @@ -110,6 +110,8 @@ jlong __jlongpointer m // 'maybe' states sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, 1.0)); break; case LIN_EQ_METHOD_JOR: sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(state_rewards), ptr_to_jlong(state_rewards), false, lin_eq_method_param)); break; + default: + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; } // set reward for infinity states to infinity diff --git a/prism/src/mtbdd/PM_ProbUntil.cc b/prism/src/mtbdd/PM_ProbUntil.cc index a3e47e19..994ac8df 100644 --- a/prism/src/mtbdd/PM_ProbUntil.cc +++ b/prism/src/mtbdd/PM_ProbUntil.cc @@ -90,6 +90,8 @@ jlong __jlongpointer m // 'maybe' states soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, 1.0)); break; case LIN_EQ_METHOD_JOR: soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(b), false, lin_eq_method_param)); break; + default: + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; } // free memory diff --git a/prism/src/mtbdd/PM_StochSteadyState.cc b/prism/src/mtbdd/PM_StochSteadyState.cc index 5a108c5f..07398770 100644 --- a/prism/src/mtbdd/PM_StochSteadyState.cc +++ b/prism/src/mtbdd/PM_StochSteadyState.cc @@ -102,6 +102,8 @@ jint num_cvars soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, 1.0)); break; case LIN_EQ_METHOD_JOR: soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JOR(env, cls, ptr_to_jlong(odd), ptr_to_jlong(rvars), num_rvars, ptr_to_jlong(cvars), num_cvars, ptr_to_jlong(a), ptr_to_jlong(b), ptr_to_jlong(init), true, lin_eq_method_param)); break; + default: + PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0; } // normalise