Allow the actual type of a PRISM model to differ from the one specified in the file.

For now, this provides a cleaner implementation of the default (unspecified)
model type being set to an MDP. Later, this will allow the actual model type
to be omitted or partially specified and derived from langage features.

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));

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));

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());

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()