diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java
index fc199bf6..51917514 100644
--- a/prism/src/explicit/CTMCModelChecker.java
+++ b/prism/src/explicit/CTMCModelChecker.java
@@ -933,7 +933,8 @@ public class CTMCModelChecker extends ProbModelChecker
 			mc = new CTMCModelChecker(null);
 			ctmc = new CTMCSimple();
 			ctmc.buildFromPrismExplicit(args[0]);
-			//System.out.println(dtmc);
+			ctmc.addInitialState(0);
+			//System.out.println(ctmc);
 			labels = mc.loadLabelsFile(args[1]);
 			//System.out.println(labels);
 			target = labels.get(args[2]);
diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java
index 70e90811..d72741f4 100644
--- a/prism/src/explicit/DTMCModelChecker.java
+++ b/prism/src/explicit/DTMCModelChecker.java
@@ -1622,6 +1622,7 @@ public class DTMCModelChecker extends ProbModelChecker
 				mc = new DTMCModelChecker(null);
 				dtmc = new DTMCSimple();
 				dtmc.buildFromPrismExplicit(args[0]);
+				dtmc.addInitialState(0);
 				//System.out.println(dtmc);
 				Map<String, BitSet> labels = mc.loadLabelsFile(args[1]);
 				//System.out.println(labels);
diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java
index f9516f45..017314b6 100644
--- a/prism/src/explicit/DTMCSimple.java
+++ b/prism/src/explicit/DTMCSimple.java
@@ -172,8 +172,6 @@ public class DTMCSimple extends DTMCExplicit implements ModelSimple
 		} catch (NumberFormatException e) {
 			throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + getModelType());
 		}
-		// Set initial state (assume 0)
-		initialStates.add(0);
 	}
 
 	// Mutators (other)
diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java
index 59e16506..875c9875 100644
--- a/prism/src/explicit/MDPSimple.java
+++ b/prism/src/explicit/MDPSimple.java
@@ -370,8 +370,6 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 		} catch (NumberFormatException e) {
 			throw new PrismException("Problem in .tra file (line " + lineNum + ") for " + getModelType());
 		}
-		// Set initial state (assume 0)
-		initialStates.add(0);
 	}
 
 	// Mutators (other)
diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index 5a4f068b..f44afb7a 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -163,6 +163,8 @@ public abstract class ModelExplicit implements Model
 
 	/**
 	 * Build (anew) from a list of transitions exported explicitly by PRISM (i.e. a .tra file).
+	 * Note that initial states are not configured (since this info is not in the file),
+	 * so this needs to be done separately (using {@link #addInitialState(int)}.
 	 */
 	public abstract void buildFromPrismExplicit(String filename) throws PrismException;
 
diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java
index 7bcf2168..88a3ace6 100644
--- a/prism/src/explicit/PrismSTPGAbstractRefine.java
+++ b/prism/src/explicit/PrismSTPGAbstractRefine.java
@@ -95,6 +95,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 		}
 		modelConcrete.buildFromPrismExplicit(traFile);
+		modelConcrete.addInitialState(0);
 		if (buildEmbeddedDtmc) {
 			// TODO: do more efficiently (straight from tra file?)
 			mainLog.println("Concrete " + "CTMC" + ": " + modelConcrete.infoString());