diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 6ed25a0c..64dd84a7 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -273,6 +273,15 @@ public class ConstructModel extends PrismComponent // Look at each outgoing choice in turn nc = modelGen.getNumChoices(); for (i = 0; i < nc; i++) { + // If required, check for duplicate actions here + if (modelType.partiallyObservable()) { + if (((NondetModel) modelSimple).getChoiceByAction(src, modelGen.getChoiceAction(i)) != -1) { + String act = modelGen.getChoiceAction(i) == null ? "" : modelGen.getChoiceAction(i).toString(); + String err = modelType + " is not allowed duplicate action"; + err += " (\"" + act + "\") in state " + state.toString(modelGen); + throw new PrismException(err); + } + } // For nondet models, collect transitions in a Distribution if (!justReach && modelType.nondeterministic()) { distr = new Distribution(); diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index a02ee18c..49fe9557 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -75,6 +75,27 @@ public interface NondetModel extends Model */ public Object getAction(int s, int i); + /** + * Get the index of the (first) choice in state {@code s} with action label {@code action}. + * Action labels (which are {@link Object}s) are tested for equality using {@link Object#equals()}. + * Returns -1 if there is no matching action. + */ + public default int getChoiceByAction(int s, Object action) + { + int numChoices = getNumChoices(s); + for (int i = 0; i < numChoices; i++) { + Object a = getAction(s, i); + if (a == null) { + if (action == null) { + return i; + } + } else if (a.equals(action)) { + return i; + } + } + return -1; + } + /** * Do all choices in in each state have a unique action label? *