From b7864791dc1bd9bab4b4bc2d44b91654c7868057 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 3 Jun 2014 14:10:40 +0000
Subject: [PATCH] Store vector in Result during model checking if requested.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8402 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/StateModelChecker.java | 13 +++++++++----
 prism/src/prism/StateModelChecker.java    | 11 +++++++----
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 120dc5f5..a7c4fc8e 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -36,6 +36,8 @@ import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
+import jdd.JDD;
+
 import parser.State;
 import parser.Values;
 import parser.ast.Expression;
@@ -323,7 +325,8 @@ public class StateModelChecker extends PrismComponent
 		mainLog.print("\n" + resultString + "\n");
 
 		// Clean up
-		vals.clear();
+		//vals.clear();
+		result.setVector(vals);
 
 		// Return result
 		return result;
@@ -967,10 +970,12 @@ public class StateModelChecker extends PrismComponent
 		} else {
 			result.setExplanation(null);
 		}
-
-		// Clear up
-		if (vals != null)
+		// Store vector if requested (and if not, clear it)
+		if (storeVector) {
+			result.setVector(vals);
+		} else if (vals != null) {
 			vals.clear();
+		}
 
 		return resVals;
 	}
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index f8b096d6..4f4c3077 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -1332,11 +1332,14 @@ public class StateModelChecker implements ModelChecker
 		} else {
 			result.setExplanation(null);
 		}
-
-		// Derefs, clears
-		JDD.Deref(ddFilter);
-		if (vals != null)
+		// Store vector if requested (and if not, clear it)
+		if (storeVector) {
+			result.setVector(vals);
+		} else if (vals != null) {
 			vals.clear();
+		}
+		// Other derefs
+		JDD.Deref(ddFilter);
 
 		return resVals;
 	}