diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index bd1c8e8e..c72f58ba 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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); } diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 699cac9e..762c92ad 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/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 { diff --git a/prism/src/simulator/TransitionList.java b/prism/src/simulator/TransitionList.java index 68d43ac2..c1a116ef 100644 --- a/prism/src/simulator/TransitionList.java +++ b/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. */