PrismCL: Allow overriding the model type to a game (STPG, SMG)

prism/src/parser/PrismParser.java

@@ -153,7 +153,7 @@ public ModulesFile parseModulesFile(InputStream str, ModelType typeOverride) thr
                 }
                 // Override type of model if requested
                 if (typeOverride != null) {
-                        mf.setModelType(typeOverride);
+                        mf.overrideModelType(typeOverride);
                 }
 
                 return mf;

prism/src/parser/PrismParser.jj

@@ -185,7 +185,7 @@ public class PrismParser
 		}
 		// Override type of model if requested
 		if (typeOverride != null) {
-			mf.setModelType(typeOverride);
+			mf.overrideModelType(typeOverride);
 		}
 
 		return mf;

prism/src/parser/ast/ModulesFile.java

@@ -50,6 +50,8 @@ public class ModulesFile extends ASTElement implements ModelInfo
 {
 	// Model type (enum)
 	private ModelType modelType;
+	// The model type that was originally specified but was later overridden
+	private ModelType overriddenModelType;
 
 	// Model components
 	private FormulaList formulaList;
@@ -130,6 +132,13 @@ public void setModelType(ModelType t)
 		modelType = t;
 	}
 
+	/** Override the model type (stores current model type as the overridden model type) */
+	public void overrideModelType(ModelType t)
+	{
+		overriddenModelType = modelType;
+		modelType = t;
+	}
+
 	public void addGlobal(Declaration d)
 	{
 		globals.add(d);
@@ -306,6 +315,15 @@ public ModelType getModelType()
 		return modelType;
 	}
 
+	/**
+	 * If the original model type was overriden (e.g., via a command line switch),
+	 * this returns the original model type. If it was not overriden, returns {@code null}.
+	 */
+	public ModelType getOverridenModelType()
+	{
+		return overriddenModelType;
+	}
+
 	public String getTypeString()
 	{
 		return "" + modelType;
@@ -1104,7 +1122,15 @@ private void checkPlayerDefns() throws PrismLangException
 		if (modelType.multiplePlayers()) {
 			// (NB: compositional games don't need this)
 			if (players.isEmpty() && systemDefns.size() == 0) {
-				throw new PrismLangException(modelType + " model has no player definitions");
+				if (overriddenModelType != null && !overriddenModelType.multiplePlayers()) {
+					// we started with a non-game model and the model type was overridden
+					// to be a game, so we add a single player controlling all nondeterminism
+					// in the system
+					addPlayer(Player.singlePlayerForEverything(this));
+				} else {
+					// we started as a game, so the lack of a player definition is an error
+					throw new PrismLangException(modelType + " model has no player definitions");
+				}
 			}
 		} else {
 			if (!players.isEmpty()) {
@@ -1526,6 +1552,7 @@ public ASTElement deepCopy(List<String> modulesToAdd) throws PrismLangException
 		ret.setPosition(this);
 		// Copy type
 		ret.setModelType(modelType);
+		ret.overriddenModelType = overriddenModelType;
 		// Deep copy main components
 		ret.setFormulaList((FormulaList) formulaList.deepCopy());
 		ret.setLabelList((LabelList) labelList.deepCopy());

prism/src/parser/ast/Player.java

@@ -53,6 +53,25 @@ public Player(String name)
 		actions = new ArrayList<String>();
 	}
 
+	/**
+	 * Generate the specification for a single player that controls all modules/actions
+	 * in the given ModulesFile.
+	 */
+	public static Player singlePlayerForEverything(ModulesFile mf)
+	{
+		Player player = new Player("p1");
+
+		for (int i = 0; i < mf.getNumModules(); i++) {
+			player.addModule(mf.getModuleName(i));
+		}
+
+		for (String a : mf.getSynchs()) {
+			player.addAction(a);
+		}
+
+		return player;
+	}
+
 	// Set methods
 
 	public void addModule(String moduleName)

prism/src/prism/PrismCL.java

@@ -1294,6 +1294,14 @@ else if (sw.equals("mdp")) {
 				else if (sw.equals("ctmc")) {
 					typeOverride = ModelType.CTMC;
 				}
+				// override model type to stpg
+				else if (sw.equals("stpg")) {
+					typeOverride = ModelType.STPG;
+				}
+				// override model type to smg
+				else if (sw.equals("smg")) {
+					typeOverride = ModelType.SMG;
+				}
 
 				// EXPORT OPTIONS:
 
@@ -2335,6 +2343,8 @@ private void printHelp()
 		mainLog.println("-dtmc .......................... Force imported/built model to be a DTMC");
 		mainLog.println("-ctmc .......................... Force imported/built model to be a CTMC");
 		mainLog.println("-mdp ........................... Force imported/built model to be an MDP");
+		mainLog.println("-stpg .......................... Force imported/built model to be an STPG");
+		mainLog.println("-smg ........................... Force imported/built model to be an SMG");
 		mainLog.println();
 		mainLog.println("EXPORT OPTIONS:");
 		mainLog.println("-exportresults <file[:options]>  Export the results of model checking to a file");