From 048017bb24fbd4e492ba99130a462735bc1d21c8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 9 Sep 2016 09:13:40 +0000
Subject: [PATCH] NondetModelChecker.checkExpressionMultiObjective(): BDD
 cleanup when computeMultiReachProbs throws Exception

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11800 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModelChecker.java | 39 +++++++++++++------------
 1 file changed, 21 insertions(+), 18 deletions(-)

diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java
index 36552190..8a20cd78 100644
--- a/prism/src/prism/NondetModelChecker.java
+++ b/prism/src/prism/NondetModelChecker.java
@@ -643,26 +643,29 @@ public class NondetModelChecker extends NonProbModelChecker
 			modelProduct.trans01 = tmptrans01;
 		}
 
-		// Do multi-objective computation
-		Object value = mcMo.computeMultiReachProbs(modelProduct, mcLtl, transRewardsListProduct, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds,
-				conflictformulae > 1);
-		
-		// Deref, clean up
-		if (ddStateIndex != null)
-			JDD.Deref(ddStateIndex);
-		if (modelProduct != null && modelProduct != model)
-			modelProduct.clear();
-		for (int i = 0; i < numObjectives; i++) {
-			if (opsAndBounds.isProbabilityObjective(i)) {
-				draDDRowVars[i].derefAll();
-				draDDColVars[i].derefAll();
+		Object value;
+		try {
+			// Do multi-objective computation
+			value = mcMo.computeMultiReachProbs(modelProduct, mcLtl, transRewardsListProduct, modelProduct.getStart(), targetDDs, multitargetDDs, multitargetIDs, opsAndBounds,
+			                                    conflictformulae > 1);
+		} finally {
+			// Deref, clean up
+			if (ddStateIndex != null)
+				JDD.Deref(ddStateIndex);
+			if (modelProduct != null && modelProduct != model)
+				modelProduct.clear();
+			for (int i = 0; i < numObjectives; i++) {
+				if (opsAndBounds.isProbabilityObjective(i)) {
+					draDDRowVars[i].derefAll();
+					draDDColVars[i].derefAll();
+				}
 			}
-		}
-		for (JDDNode t : targetDDs)
-			JDD.Deref(t);
-		if (multitargetDDs != null)
-			for (JDDNode t : multitargetDDs)
+			for (JDDNode t : targetDDs)
 				JDD.Deref(t);
+			if (multitargetDDs != null)
+				for (JDDNode t : multitargetDDs)
+					JDD.Deref(t);
+		}
 
 		if (value instanceof TileList) {
 			if (opsAndBounds.numberOfNumerical() == 2) {