Fix in explicit model construction: allow distinct MDP choices that differ only by action name.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3362 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ConstructModel.java

@@ -73,7 +73,7 @@ public class ConstructModel
 	 */
 	public Model constructModel(ModulesFile modulesFile) throws PrismException
 	{
-		return constructModel(modulesFile, false, false);
+		return constructModel(modulesFile, false, false, true);
 	}
 
 	/**
@@ -85,6 +85,20 @@ public class ConstructModel
 	 * @param buildSparse Build a sparse version of the model (if possible)?
 	 */
 	public Model constructModel(ModulesFile modulesFile, boolean justReach, boolean buildSparse) throws PrismException
+	{
+		return constructModel(modulesFile, justReach, buildSparse, true);
+	}
+	
+	/**
+	 * Construct an explicit-state model from a PRISM model language description and return.
+	 * If {@code justReach} is true, no model is built and null is returned;
+	 * the set of reachable states can be obtained with {@link #getStatesList()}.
+	 * @param modulesFile The PRISM model
+	 * @param justReach If true, just build the reachable state set, not the model
+	 * @param buildSparse Build a sparse version of the model (if possible)?
+	 * @param distinguishActions True if the distributions with different action should be added to the model as separate ones.
+	 */
+	public Model constructModel(ModulesFile modulesFile, boolean justReach, boolean buildSparse, boolean distinguishActions) throws PrismException
 	{
 		// Model info
 		ModelType modelType;
@@ -201,8 +215,12 @@ public class ConstructModel
 				}
 				if (!justReach) {
 					if (modelType == ModelType.MDP) {
-						k = mdp.addChoice(src, distr);
-						mdp.setAction(src, k, engine.getTransitionAction(i, 0));
+						if (distinguishActions) {
+							k = mdp.addActionLabelledChoice(src, distr, engine.getTransitionAction(i, 0));
+							mdp.setAction(src, k, engine.getTransitionAction(i, 0));
+						} else {
+							k = mdp.addChoice(src, distr);
+						}
 					} else if (modelType == ModelType.CTMDP) {
 						ctmdp.addChoice(src, distr);
 					}

prism/src/prism/UndefinedConstants.java

@@ -377,6 +377,7 @@ public class UndefinedConstants
 				pfConsts[index].define(sl, sh, ss);
 			}
 			else {
+				System.out.println("XXX: " + name);
 				if (useAll)
 					throw new PrismException("\"" + name + "\" is not an undefined constant");
 			}

prism/src/simulator/SimulatorEngine.java

@@ -272,6 +272,7 @@ public class SimulatorEngine
 		switch (modelType) {
 		case DTMC:
 		case MDP:
+		case PTA:
 			// Pick a random choice
 			i = rng.randomUnifInt(numChoices);
 			choice = transitionList.getChoice(i);
@@ -596,9 +597,9 @@ public class SimulatorEngine
 		this.mfConstants = modulesFile.getConstantValues();
 
 		// Check for PTAs
-		if (modulesFile.getModelType() == ModelType.PTA) {
+		/*if (modulesFile.getModelType() == ModelType.PTA) {
 			throw new PrismException("Sorry - the simulator does not currently support PTAs");
-		}
+		}*/
 
 		// Check for presence of system...endsystem
 		if (modulesFile.getSystemDefn() != null) {
@@ -1352,7 +1353,7 @@ public class SimulatorEngine
 		for (int i = 0; i < n; i++) {
 			definedPFConstants = undefinedConstants.getPFConstantValues();
 			pfcs[i] = definedPFConstants;
-			propertiesFile.setUndefinedConstants(definedPFConstants);
+			propertiesFile.setSomeUndefinedConstants(definedPFConstants);
 			try {
 				checkPropertyForSimulation(expr);
 				indices[i] = addProperty(expr, propertiesFile);