From 985e4516a56ff6e32af9efde3b1615f14382fe1d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 29 May 2020 15:18:46 +0100
Subject: [PATCH] Generalise MDPSimple copy constructor from MDPSparse to MDP.

Also requires updating ModelExplicit.copyFrom (to copy from Model).
---
 prism/src/explicit/MDPSimple.java     | 45 ++++++++++-----------------
 prism/src/explicit/ModelExplicit.java | 32 +++++++++----------
 2 files changed, 32 insertions(+), 45 deletions(-)

diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java
index e76f3bfb..26070b1d 100644
--- a/prism/src/explicit/MDPSimple.java
+++ b/prism/src/explicit/MDPSimple.java
@@ -35,6 +35,7 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Iterator;
 import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
 
 import prism.PrismException;
@@ -176,42 +177,28 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 	/**
 	 * Construct an MDPSimple object from an MDPSparse one.
 	 */
-	public MDPSimple(MDPSparse mdp)
+	public MDPSimple(MDP mdp)
 	{
-		this(mdp.numStates);
+		this(mdp.getNumStates());
 		copyFrom(mdp);
-		// Copy storage directly to avoid worrying about duplicate distributions (and for efficiency)
-		for (int s = 0; s < numStates; s++) {
-			for (int c = 0; c < mdp.getNumChoices(s); c++) {
+		int numStates = getNumStates();
+		for (int i = 0; i < numStates; i++) {
+			int numChoices = getNumChoices(i);
+			for (int j = 0; j < numChoices; j++) {
+				Object action = getAction(i, j);
 				Distribution distr = new Distribution();
-				Iterator<Entry<Integer, Double>> it = mdp.getTransitionsIterator(s, c);
-				while (it.hasNext()) {
-					Entry<Integer, Double> entry = it.next();
-					distr.add(entry.getKey(), entry.getValue());
+				Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
+				while (iter.hasNext()) {
+					Map.Entry<Integer, Double> e = iter.next();
+					distr.set(e.getKey(), e.getValue());
 				}
-				this.addChoice(s, distr);
-			}
-		}
-
-		if (mdp.actions != null) {
-			actions = new ArrayList<List<Object>>(numStates);
-			for (int s = 0; s < numStates; s++)
-				actions.add(null);
-			for (int s = 0; s < numStates; s++) {
-				int n = mdp.getNumChoices(s);
-				List<Object> list = new ArrayList<Object>(n);
-				for (int i = 0; i < n; i++) {
-					list.add(mdp.getAction(s, i));
+				if (action == null) {
+					addActionLabelledChoice(i, distr, action);
+				} else {
+					addChoice(i, distr);
 				}
-				actions.set(s, list);
 			}
 		}
-		// Copy flags/stats too
-		allowDupes = false; // TODO check this
-		numDistrs = mdp.numDistrs;
-		numTransitions = mdp.numTransitions;
-		maxNumDistrs = mdp.maxNumDistrs;
-		maxNumDistrsOk = true; // TODO not sure
 	}
 
 	// Mutators (for ModelSimple)
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index 6d5b62f8..58c27878 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -77,47 +77,47 @@ public abstract class ModelExplicit implements Model
 	// Mutators
 
 	/**
-	 * Copy data from another ModelExplicit (used by superclass copy constructors).
+	 * Copy data from another Model (used by superclass copy constructors).
 	 * Assumes that this has already been initialise()ed.
 	 */
-	public void copyFrom(ModelExplicit model)
+	public void copyFrom(Model model)
 	{
-		numStates = model.numStates;
-		for (int in : model.initialStates) {
+		numStates = model.getNumStates();
+		for (int in : model.getInitialStates()) {
 			addInitialState(in);
 		}
-		for (int dl : model.deadlocks) {
+		for (int dl : model.getDeadlockStates()) {
 			addDeadlockState(dl);
 		}
 		// Shallow copy of read-only stuff
-		statesList = model.statesList;
-		constantValues = model.constantValues;
-		labels = model.labels;
-		varList = model.varList;
+		statesList = model.getStatesList();
+		constantValues = model.getConstantValues();
+		labels = model.getLabelToStatesMap();
+		varList = model.getVarList();
 	}
 
 	/**
-	 * Copy data from another ModelExplicit and a state index permutation,
+	 * Copy data from another Model and a state index permutation,
 	 * i.e. state index i becomes index permut[i]
 	 * (used by superclass copy constructors).
 	 * Assumes that this has already been initialise()ed.
 	 * Pointer to states list is NOT copied (since now wrong).
 	 */
-	public void copyFrom(ModelExplicit model, int permut[])
+	public void copyFrom(Model model, int permut[])
 	{
-		numStates = model.numStates;
-		for (int in : model.initialStates) {
+		numStates = model.getNumStates();
+		for (int in : model.getInitialStates()) {
 			addInitialState(permut[in]);
 		}
-		for (int dl : model.deadlocks) {
+		for (int dl : model.getDeadlockStates()) {
 			addDeadlockState(permut[dl]);
 		}
 		// Shallow copy of (some) read-only stuff
 		// (i.e. info that is not broken by permute)
 		statesList = null;
-		constantValues = model.constantValues;
+		constantValues = model.getConstantValues();
 		labels.clear();
-		varList = model.varList;
+		varList = model.getVarList();
 	}
 
 	/**