Move CTL cex class storage into new cex package.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3453 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/cex/CexPathAsBDDs.java

@@ -0,0 +1,86 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package cex;
+
+import java.util.ArrayList;
+
+import jdd.JDD;
+import jdd.JDDNode;
+import parser.State;
+
+/**
+ * Class to store a single-path counterexample, as a list of BDDs.
+ */
+public class CexPathAsBDDs
+{
+	protected prism.Model model;
+	protected ArrayList<JDDNode> states;
+
+	/**
+	 * Construct empty path.
+	 */
+	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);
+	}
+
+	/**
+	 * Clear the counterexample.
+	 */
+	public void clear()
+	{
+		for (JDDNode dd : states) {
+			JDD.Deref(dd);
+		}
+	}
+
+	@Override
+	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;
+	}
+}

prism/src/prism/NonProbModelChecker.java

@@ -29,8 +29,8 @@ package prism;
 import java.util.*;
 
 import jdd.*;
-import parser.*;
 import parser.ast.*;
+import cex.CexPathAsBDDs;
 
 /*
  * Non probabilistic model checker, initially for CTL.
@@ -342,49 +342,6 @@ 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;
-		}
-	}
 }
 
 // ------------------------------------------------------------------------------

prism/src/prism/PrismCL.java

@@ -446,8 +446,8 @@ public class PrismCL
 							if (cex != null) {
 								mainLog.println("\nCounterexample/witness:");
 								mainLog.println(cex);
-								if (cex instanceof NonProbModelChecker.CexPathAsBDDs){
-									((NonProbModelChecker.CexPathAsBDDs) cex).clear();
+								if (cex instanceof cex.CexPathAsBDDs){
+									((cex.CexPathAsBDDs) cex).clear();
 								}
 							}
 						} catch (PrismException e) {