From bd9f2f255d2dc9850fcbc9e1e232d970e111c4a5 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 12 Jul 2016 10:14:59 +0000 Subject: [PATCH] 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 | 4 ++-- prism/src/simulator/ModulesFileModelGenerator.java | 8 ++++++++ prism/src/simulator/TransitionList.java | 10 ++++++++++ 3 files changed, 20 insertions(+), 2 deletions(-) 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. */