diff --git a/prism/src/prism/DefaultModelGenerator.java b/prism/src/prism/DefaultModelGenerator.java index 64eeda02..c898f31b 100644 --- a/prism/src/prism/DefaultModelGenerator.java +++ b/prism/src/prism/DefaultModelGenerator.java @@ -171,6 +171,12 @@ public abstract class DefaultModelGenerator implements ModelGenerator @Override public abstract Object getTransitionAction(int i, int offset) throws PrismException; + @Override + public Object getChoiceAction(int i) throws PrismException + { + return getTransitionAction(i, 0); + } + @Override public abstract double getTransitionProbability(int i, int offset) throws PrismException; diff --git a/prism/src/prism/ModelGenerator.java b/prism/src/prism/ModelGenerator.java index 730b9e0d..3c354c3b 100644 --- a/prism/src/prism/ModelGenerator.java +++ b/prism/src/prism/ModelGenerator.java @@ -106,6 +106,16 @@ public interface ModelGenerator extends ModelInfo */ public Object getTransitionAction(int i, int offset) throws PrismException; + /** + * Get the action label of a choice, specified by its index. + * The label can be any Object, but will often be treated as a string, so it should at least + * have a meaningful toString() method implemented. Absence of an action label is denoted by null. + * Note: If the model has different actions for different transitions within a choice + * (as can be the case for Markov chains), this method returns the action for the first transition. + * So, this method is essentially equivalent to {@code getTransitionAction(i, 0)}. + */ + public Object getChoiceAction(int i) throws PrismException; + /** * Get the probability/rate of a transition within a choice, specified by its index/offset. * @param i Index of the nondeterministic choice