Add slightly more efficient implementation of getChoiceAction for PRISM models.

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

prism/src/explicit/ConstructModel.java

@@ -275,13 +275,13 @@ public class ConstructModel extends PrismComponent
 				if (!justReach) {
 					if (modelType == ModelType.MDP) {
 						if (distinguishActions) {
-							mdp.addActionLabelledChoice(src, distr, modelGen.getTransitionAction(i, 0));
+							mdp.addActionLabelledChoice(src, distr, modelGen.getChoiceAction(i));
 						} else {
 							mdp.addChoice(src, distr);
 						}
 					} else if (modelType == ModelType.CTMDP) {
 						if (distinguishActions) {
-							ctmdp.addActionLabelledChoice(src, distr, modelGen.getTransitionAction(i, 0));
+							ctmdp.addActionLabelledChoice(src, distr, modelGen.getChoiceAction(i));
 						} else {
 							ctmdp.addChoice(src, distr);
 						}

prism/src/simulator/ModulesFileModelGenerator.java

@@ -282,6 +282,14 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator
 		return a < 0 ? null : modulesFile.getSynch(a - 1);
 	}
 
+	@Override
+	public String getChoiceAction(int index) throws PrismException
+	{
+		TransitionList transitions = getTransitionList();
+		int a = transitions.getChoiceModuleOrActionIndex(index);
+		return a < 0 ? null : modulesFile.getSynch(a - 1);
+	}
+
 	@Override
 	public double getTransitionProbability(int index, int offset) throws PrismException
 	{

prism/src/simulator/TransitionList.java

@@ -205,6 +205,16 @@ public class TransitionList
 		return getChoiceOfTransition(index).getModuleOrActionIndex();
 	}
 
+	/**
+	 * Get the index of the action/module of a choice, specified by its index.
+	 * (-i for independent in ith module, i for synchronous on ith action)
+	 * (in both cases, modules/actions are 1-indexed)
+	 */
+	public int getChoiceModuleOrActionIndex(int index)
+	{
+		return getChoice(index).getModuleOrActionIndex();
+	}
+
 	/**
 	 * Get the probability/rate of a transition, specified by its index.
 	 */