Deadlock info preserved in explicit model copies.

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

prism/src/explicit/MDPSparse.java

@@ -86,10 +86,7 @@ public class MDPSparse extends MDPExplicit
 		int i, j, k, n;
 		TreeMap<Integer, Double> sorted = null;
 		initialise(mdp.getNumStates());
-		for (int in : mdp.getInitialStates()) {
-			addInitialState(in);
-		}
-		statesList = mdp.getStatesList();
+		copyFrom(mdp);
 		// Copy stats
 		numDistrs = mdp.getNumChoices();
 		numTransitions = mdp.getNumTransitions();
@@ -154,11 +151,7 @@ public class MDPSparse extends MDPExplicit
 		TreeMap<Integer, Double> sorted = null;
 		int permutInv[];
 		initialise(mdp.getNumStates());
-		for (int in : mdp.getInitialStates()) {
-			addInitialState(permut[in]);
-		}
-		// Don't copy states list (it will be wrong)
-		statesList = null;
+		copyFrom(mdp, permut);
 		// Copy stats
 		numDistrs = mdp.getNumChoices();
 		numTransitions = mdp.getNumTransitions();
@@ -226,6 +219,9 @@ public class MDPSparse extends MDPExplicit
 		for (int in : mdp.getInitialStates()) {
 			addInitialState(in);
 		}
+		for (int dl : mdp.getDeadlockStates()) {
+			addDeadlockState(dl);
+		}
 		statesList = new ArrayList<State>();
 		for (int s : states) {
 			statesList.add(mdp.getStatesList().get(s));

prism/src/explicit/Model.java

@@ -81,6 +81,12 @@ public interface Model
 	 */
 	public int getNumDeadlockStates();
 
+	/**
+	 * Get iterator over states that are/were deadlocks.
+	 * (Such states may have been fixed at build-time by adding self-loops)
+	 */
+	public Iterable<Integer> getDeadlockStates();
+	
 	/**
 	 * Check whether a state is/was deadlock.
 	 * (Such states may have been fixed at build-time by adding self-loops)

prism/src/explicit/ModelExplicit.java

@@ -188,6 +188,12 @@ public abstract class ModelExplicit implements Model
 		return deadlocks.size();
 	}
 	
+	@Override
+	public Iterable<Integer> getDeadlockStates()
+	{
+		return deadlocks;
+	}
+
 	@Override
 	public boolean isDeadlockState(int i)
 	{