From d2fcc37136ce10569b76536dfc6fdabb6027f949 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 29 Jun 2011 22:42:37 +0000
Subject: [PATCH] Small tidy of CTL cex generation/storage - aiming towards
 integratino with other cex stuff.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3177 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NonProbModelChecker.java | 50 ++++++++++++++++++++++--
 prism/src/prism/PrismCL.java             |  8 +++-
 2 files changed, 52 insertions(+), 6 deletions(-)

diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java
index 2a85e630..9b2a657b 100644
--- a/prism/src/prism/NonProbModelChecker.java
+++ b/prism/src/prism/NonProbModelChecker.java
@@ -199,7 +199,6 @@ public class NonProbModelChecker extends StateModelChecker
 		JDDNode b1, b2, transRel, tmp, tmp2, tmp3, tmp4, init = null;
 		ArrayList<JDDNode> cexDDs = null;
 		boolean done, cexDone = false;
-		List<State> cexStates;
 		Vector<String> cexActions;
 		int iters, i;
 		long l;
@@ -310,12 +309,12 @@ public class NonProbModelChecker extends StateModelChecker
 			}
 			// Otherwise, convert list of BDDs to list of states
 			else {
-				cexStates = new ArrayList<State>(cexDDs.size());
+				CexPathAsBDDs cex = new CexPathAsBDDs(model);
 				for (i = cexDDs.size() - 1; i >= 0; i--) {
-					cexStates.add(model.convertBddToState(cexDDs.get(i)));
+					cex.addState(cexDDs.get(i));
 					JDD.Deref(cexDDs.get(i));
 				}
-				result.setCounterexample(cexStates);
+				result.setCounterexample(cex);
 			}
 		}
 
@@ -331,6 +330,49 @@ public class NonProbModelChecker extends StateModelChecker
 
 		return new StateValuesMTBDD(tmp, model);
 	}
+
+	class CexPathAsBDDs
+	{
+		protected prism.Model model;
+		protected ArrayList<JDDNode> states;
+
+		public CexPathAsBDDs(prism.Model model)
+		{
+			this.model = model;
+			states = new ArrayList<JDDNode>();
+		}
+
+		/**
+		 * Add a state to the path (as a BDD, which will be stored and Ref'ed.
+		 */
+		public void addState(JDDNode state)
+		{
+			JDD.Ref(state);
+			states.add(state);
+		}
+
+		public void clear()
+		{
+			for (JDDNode dd : states) {
+				JDD.Deref(dd);
+			}
+		}
+
+		public String toString()
+		{
+			State state;
+			int i, n;
+			String s = "";
+			n = states.size();
+			for (i = 0; i < n; i++) { 
+				state = model.convertBddToState(states.get(i));
+				s += state.toString();
+				if (i < n - 1)
+					s += "\n";
+			}
+			return s;
+		}
+	}
 }
 
 // ------------------------------------------------------------------------------
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index f6c0b2b0..2ddc310b 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -415,9 +415,13 @@ public class PrismCL
 						// store result of model checking
 						try {
 							results[j].setResult(definedMFConstants, definedPFConstants, res.getResult());
-							if (res.getCounterexample() != null) {
+							Object cex = res.getCounterexample(); 
+							if (cex != null) {
 								mainLog.println("\nCounterexample/witness:");
-								mainLog.println(res.getCounterexample());
+								mainLog.println(cex);
+								if (cex instanceof NonProbModelChecker.CexPathAsBDDs){
+									((NonProbModelChecker.CexPathAsBDDs) cex).clear();
+								}
 							}
 						} catch (PrismException e) {
 							error("Problem storing results");