From 80f8605a1e8344ac4387561e5b81bd3a7a7b742a Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 10 Feb 2012 23:23:06 +0000
Subject: [PATCH] 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     | 14 +++++---------
 prism/src/explicit/Model.java         |  6 ++++++
 prism/src/explicit/ModelExplicit.java |  6 ++++++
 3 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java
index b2b9dfd2..2a00fa5f 100644
--- a/prism/src/explicit/MDPSparse.java
+++ b/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));
diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java
index 79d815c6..515b59fd 100644
--- a/prism/src/explicit/Model.java
+++ b/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)
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index 2b7333d1..c3ba18ab 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/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)
 	{