From 2852356135ea0a4535e2de5353bf118e2dfdf55e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 19 Nov 2008 20:47:08 +0000 Subject: [PATCH] Bug fix: Use of MTBDD engine with Gauss-Seidel detected as error in GUI. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@825 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/mtbdd/PM_ProbReachReward.cc | 2 ++ prism/src/mtbdd/PM_ProbUntil.cc | 2 ++ prism/src/mtbdd/PM_StochSteadyState.cc | 2 ++ 3 files changed, 6 insertions(+) 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