diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java
index 51c18ffe..3a4508be 100644
--- a/prism/src/parser/PrismParser.java
+++ b/prism/src/parser/PrismParser.java
@@ -151,7 +151,7 @@ public class PrismParser implements PrismParserConstants {
                 }
                 // Override type of model if requested
                 if (typeOverride != null) {
-                        mf.setModelType(typeOverride);
+                        mf.setModelTypeInFile(typeOverride);
                 }
 
                 return mf;
@@ -371,7 +371,7 @@ public class PrismParser implements PrismParserConstants {
 
 // Modules file
   static final public 
-ModulesFile ModulesFile() throws ParseException, PrismLangException {ModelType type = ModelType.MDP;
+ModulesFile ModulesFile() throws ParseException, PrismLangException {ModelType type = null;
         int typeCount = 0;
         Token typeDupe = null;
         Declaration global;
@@ -491,8 +491,8 @@ mf.setInitialStates(init); initCount++; if (initCount == 2) initDupe = init;
                         {if (true) throw new PrismLangException("There were multiple init...endinit constructs", initDupe);}
                 }
 
-                // Set model type (note default is MDP)
-                mf.setModelType(type);
+                // Set model type (might be null, i.e., unspecified)
+                mf.setModelTypeInFile(type);
 
                 // Return completed ModulesFile object
                 mf.setPosition(begin != null? begin: getToken(0), getToken(0));
diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj
index e3b5c87e..911bb9e4 100644
--- a/prism/src/parser/PrismParser.jj
+++ b/prism/src/parser/PrismParser.jj
@@ -183,7 +183,7 @@ public class PrismParser
 		}
 		// Override type of model if requested
 		if (typeOverride != null) {
-			mf.setModelType(typeOverride);
+			mf.setModelTypeInFile(typeOverride);
 		}
 		
 		return mf;
@@ -531,7 +531,7 @@ TOKEN :
 
 ModulesFile ModulesFile() throws PrismLangException :
 {
-	ModelType type = ModelType.MDP;
+	ModelType type = null;
 	int typeCount = 0;
 	Token typeDupe = null;
 	Declaration global;
@@ -574,8 +574,8 @@ ModulesFile ModulesFile() throws PrismLangException :
 			throw new PrismLangException("There were multiple init...endinit constructs", initDupe);
 		}
 		
-		// Set model type (note default is MDP)
-		mf.setModelType(type);
+		// Set model type (might be null, i.e., unspecified)
+		mf.setModelTypeInFile(type);
 		
 		// Return completed ModulesFile object
 		mf.setPosition(begin != null? begin: getToken(0), getToken(0));
diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java
index 0d9c33b8..900496f4 100644
--- a/prism/src/parser/ast/ModulesFile.java
+++ b/prism/src/parser/ast/ModulesFile.java
@@ -44,7 +44,9 @@ import parser.type.*;
 
 public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerator
 {
-	// Model type (enum)
+	// Model type, as specified in the model file
+	private ModelType modelTypeInFile;
+	// Model type (actual, may differ)
 	private ModelType modelType;
 
 	// Model components
@@ -84,7 +86,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		formulaList = new FormulaList();
 		labelList = new LabelList();
 		constantList = new ConstantList();
-		modelType = ModelType.MDP; // default type
+		modelTypeInFile = modelType = null; // Unspecified
 		globals = new Vector<Declaration>();
 		modules = new Vector<Object>();
 		systemDefns = new ArrayList<SystemDefn>();
@@ -119,6 +121,22 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		constantList = cl;
 	}
 
+	/**
+	 * Set the model type that is specified in the model file.
+	 * Can be null, denoting that it is unspecified.
+	 */
+	public void setModelTypeInFile(ModelType t)
+	{
+		modelTypeInFile = t;
+		// As a default, set the actual type to be the same
+		modelType = modelTypeInFile;
+	}
+
+	/**
+	 * Set the actual model type,
+	 * which may differ from the type specified in the model file.
+	 * Note: if {@link #tidyUp()} is called, this may be overwritten.
+	 */
 	public void setModelType(ModelType t)
 	{
 		modelType = t;
@@ -273,6 +291,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		return constantList;
 	}
 
+	public ModelType getModelTypeInFile()
+	{
+		return modelTypeInFile;
+	}
+	
 	@Override
 	public ModelType getModelType()
 	{
@@ -705,6 +728,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		// Then identify/check any references to action names
 		findAllActions(synchs);
 
+		// Determine actual model type
+		// (checks/processing below this point can assume that modelType
+		//  is non-null; methods before this point cannot)
+		finaliseModelType();
+		
 		// Various semantic checks 
 		doSemanticChecks();
 		// Type checking
@@ -1244,6 +1272,21 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		return new VarList(this);
 	}
 
+	/**
+	 * Determine the actual model type
+	 */
+	private void finaliseModelType()
+	{
+		// Default (if unspecified) is MDP
+		if (modelTypeInFile == null) {
+			modelType = ModelType.MDP;
+		}
+		// Otherwise, it's just whatever was specified
+		else {
+			modelType = modelTypeInFile;
+		}
+	}
+	
 	// Methods required for ASTElement:
 
 	/**
@@ -1262,7 +1305,9 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		String s = "", tmp;
 		int i, n;
 
-		s += modelType.toString().toLowerCase() + "\n\n";
+		if (modelTypeInFile != null) {
+			s += modelTypeInFile.toString().toLowerCase() + "\n\n";
+		}
 
 		tmp = "" + formulaList;
 		if (tmp.length() > 0)
@@ -1323,6 +1368,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		// Copy ASTElement stuff
 		ret.setPosition(this);
 		// Copy type
+		ret.setModelTypeInFile(modelTypeInFile);
 		ret.setModelType(modelType);
 		// Deep copy main components
 		ret.setFormulaList((FormulaList) formulaList.deepCopy());
diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java
index 0ac0e62d..8989536b 100644
--- a/prism/src/pta/DigitalClocks.java
+++ b/prism/src/pta/DigitalClocks.java
@@ -172,7 +172,7 @@ public class DigitalClocks
 		prop = (Expression) propertyToCheck.deepCopy();
 
 		// Change the model type
-		mf.setModelType(ModelType.MDP);
+		mf.setModelTypeInFile(ModelType.MDP);
 
 		// Change all clock variable declarations to bounded integers
 		mf = (ModulesFile) mf.accept(new ASTTraverseModify()