Proper DD cleanup after MTBDD engine's Gauss-Seidel exception

Due to the change in 98c019b175,
the C-level 'Gauss-Seidel not supported' checks of the MTBDD engine
get triggered now more often. Before, they would just return, now we
actually do the usual DD cleanup there to avoid DD reference leaks.

(plus: put breaks in switch statements on separate lines to better see code-flow)

prism/src/mtbdd/PM_ProbReachReward.cc

@@ -105,13 +105,18 @@ jlong __jlongpointer m	// 'maybe' states
 	sol = NULL;
 	switch (lin_eq_method) {
 		case LIN_EQ_METHOD_POWER:
-			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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)); break;
+			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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));
+			break;
 		case LIN_EQ_METHOD_JACOBI:
-			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;
+			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;
+			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 error message and return NULL pointer after cleanup, below
+			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine");
+			break;
 	}
 	
 	// set reward for infinity states to infinity

prism/src/mtbdd/PM_ProbReachRewardInterval.cc

@@ -120,13 +120,18 @@ jint flags
 	sol = NULL;
 	switch (lin_eq_method) {
 		case LIN_EQ_METHOD_POWER:
-			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(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(lower), ptr_to_jlong(upper), false, flags)); break;
+			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(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(lower), ptr_to_jlong(upper), false, flags));
+			break;
 		case LIN_EQ_METHOD_JACOBI:
-			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, 1.0, flags)); break;
+			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, 1.0, flags));
+			break;
 		case LIN_EQ_METHOD_JOR:
-			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); break;
+			sol = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags));
+			break;
 		default:
-			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0;
+			// set error message and return NULL pointer after cleanup, below
+			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine");
+			break;
 	}
 	
 	// set reward for infinity states to infinity

prism/src/mtbdd/PM_ProbUntil.cc

@@ -85,13 +85,18 @@ jlong __jlongpointer m	// 'maybe' states
 	soln = NULL;
 	switch (lin_eq_method) {
 		case LIN_EQ_METHOD_POWER:
-			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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)); break;
+			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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));
+			break;
 		case LIN_EQ_METHOD_JACOBI:
-			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;
+			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;
+			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;
+			// set error message and return NULL pointer after cleanup, below
+			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine");
+			break;
 	}
 	
 	// free memory

prism/src/mtbdd/PM_ProbUntilInterval.cc

@@ -104,13 +104,18 @@ jint flags
 	soln = NULL;
 	switch (lin_eq_method) {
 		case LIN_EQ_METHOD_POWER:
-			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(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(lower), ptr_to_jlong(upper), false, flags)); break;
+			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1PowerInterval(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(lower), ptr_to_jlong(upper), false, flags));
+			break;
 		case LIN_EQ_METHOD_JACOBI:
-			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, 1.0, flags)); break;
+			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, 1.0, flags));
+			break;
 		case LIN_EQ_METHOD_JOR:
-			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags)); break;
+			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1JORInterval(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(lower), ptr_to_jlong(upper), false, lin_eq_method_param, flags));
+			break;
 		default:
-			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine"); return 0;
+			// set error message and return NULL pointer after cleanup, below
+			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine");
+			break;
 	}
 	
 	// free memory

prism/src/mtbdd/PM_StochSteadyState.cc

@@ -101,13 +101,18 @@ jint num_cvars
 	soln = NULL;
 	switch (lin_eq_method) {
 		case LIN_EQ_METHOD_POWER:
-			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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)); break;
+			soln = jlong_to_DdNode(Java_mtbdd_PrismMTBDD_PM_1Power(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));
+			break;
 		case LIN_EQ_METHOD_JACOBI:
-			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;
+			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;
+			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;
+			// set error message and return NULL pointer after cleanup, below
+			PM_SetErrorMessage("Gauss-Seidel and its variants are currently not supported by the MTBDD engine");
+			break;
 	}
 	
 	// normalise