diff --git a/prism/src/automata/LTSFromDA.java b/prism/src/automata/LTSFromDA.java index c453e8fc..53e2aa88 100644 --- a/prism/src/automata/LTSFromDA.java +++ b/prism/src/automata/LTSFromDA.java @@ -164,12 +164,6 @@ public class LTSFromDA extends ModelExplicit implements LTS return null; } - @Override - public boolean areAllChoiceActionsUnique() - { - return false; - } - @Override public int getNumTransitions(int s, int i) { diff --git a/prism/src/explicit/LTSExplicit.java b/prism/src/explicit/LTSExplicit.java index de14a261..65a54292 100644 --- a/prism/src/explicit/LTSExplicit.java +++ b/prism/src/explicit/LTSExplicit.java @@ -89,13 +89,6 @@ public class LTSExplicit extends ModelExplicit implements LTS return null; } - @Override - public boolean areAllChoiceActionsUnique() - { - // as we don't assign action labels, they are not unique - return false; - } - @Override public int getNumTransitions(int s, int i) { diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java index a2226d44..93911281 100644 --- a/prism/src/explicit/MDPExplicit.java +++ b/prism/src/explicit/MDPExplicit.java @@ -27,8 +27,6 @@ package explicit; -import java.util.HashSet; - import strat.MDStrategy; /** @@ -36,26 +34,6 @@ import strat.MDStrategy; */ public abstract class MDPExplicit extends ModelExplicit implements MDP { - // Accessors (for NondetModel) - - @Override - public boolean areAllChoiceActionsUnique() - { - HashSet sActions = new HashSet(); - for (int s = 0; s < numStates; s++) { - int n = getNumChoices(s); - if (n > 1) { - sActions.clear(); - for (int i = 0; i < n; i++) { - if (!sActions.add(getAction(s, i))) { - return false; - } - } - } - } - return true; - } - // Accessors (for MDP) @Override diff --git a/prism/src/explicit/NondetModel.java b/prism/src/explicit/NondetModel.java index 65624a4f..a02ee18c 100644 --- a/prism/src/explicit/NondetModel.java +++ b/prism/src/explicit/NondetModel.java @@ -27,6 +27,7 @@ package explicit; import java.util.BitSet; +import java.util.HashSet; import java.util.Iterator; import java.util.function.IntPredicate; @@ -76,8 +77,28 @@ public interface NondetModel extends Model /** * Do all choices in in each state have a unique action label? + *

+ * NB: "true" does not imply that all choices are labelled, + * e.g., an a-labelled choice and an unlabelled one _are_ considered unique; + * multiple unlabelled choices are _not_ considered unique. */ - public boolean areAllChoiceActionsUnique(); + public default boolean areAllChoiceActionsUnique() + { + int numStates = getNumStates(); + HashSet sActions = new HashSet(); + for (int s = 0; s < numStates; s++) { + int n = getNumChoices(s); + if (n > 1) { + sActions.clear(); + for (int i = 0; i < n; i++) { + if (!sActions.add(getAction(s, i))) { + return false; + } + } + } + } + return true; + } /** * Get the number of transitions from choice {@code i} of state {@code s}. diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 030405c0..e3bb26fc 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/prism/src/explicit/STPGAbstrSimple.java @@ -438,12 +438,6 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS return null; } - @Override - public boolean areAllChoiceActionsUnique() - { - throw new RuntimeException("Not implemented"); - } - @Override public boolean allSuccessorsInSet(int s, int i, BitSet set) { diff --git a/prism/src/explicit/SubNondetModel.java b/prism/src/explicit/SubNondetModel.java index b69691af..5753ff18 100644 --- a/prism/src/explicit/SubNondetModel.java +++ b/prism/src/explicit/SubNondetModel.java @@ -289,12 +289,6 @@ public class SubNondetModel implements NondetModel return model.getAction(sOriginal, iOriginal); } - @Override - public boolean areAllChoiceActionsUnique() - { - throw new RuntimeException("Not implemented"); - } - @Override public int getNumTransitions(int s, int i) { diff --git a/prism/src/explicit/modelviews/MDPAdditionalChoices.java b/prism/src/explicit/modelviews/MDPAdditionalChoices.java index 1f2454d9..3bec697f 100644 --- a/prism/src/explicit/modelviews/MDPAdditionalChoices.java +++ b/prism/src/explicit/modelviews/MDPAdditionalChoices.java @@ -185,13 +185,6 @@ public class MDPAdditionalChoices extends MDPView return (additional == null) ? null : additional.get(choice - numOriginalChoices); } - @Override - public boolean areAllChoiceActionsUnique() - { - return model.areAllChoiceActionsUnique() && super.areAllChoiceActionsUnique(); - } - - //--- MDP --- diff --git a/prism/src/explicit/modelviews/MDPDroppedAllChoices.java b/prism/src/explicit/modelviews/MDPDroppedAllChoices.java index 4cd6ad4e..f71f75c9 100644 --- a/prism/src/explicit/modelviews/MDPDroppedAllChoices.java +++ b/prism/src/explicit/modelviews/MDPDroppedAllChoices.java @@ -169,12 +169,6 @@ public class MDPDroppedAllChoices extends MDPView return model.getAction(state, choice); } - @Override - public boolean areAllChoiceActionsUnique() - { - return model.areAllChoiceActionsUnique() ? true : super.areAllChoiceActionsUnique(); - } - @Override public Iterator getSuccessorsIterator(final int state, final int choice) { diff --git a/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java b/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java index ea81933f..7ebc5dbb 100644 --- a/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java +++ b/prism/src/explicit/modelviews/MDPDroppedChoicesCached.java @@ -186,12 +186,6 @@ public class MDPDroppedChoicesCached extends MDPView return model.getAction(state, originalChoice); } - @Override - public boolean areAllChoiceActionsUnique() - { - return model.areAllChoiceActionsUnique() ? true : super.areAllChoiceActionsUnique(); - } - @Override public Iterator getSuccessorsIterator(final int state, final int choice) { diff --git a/prism/src/explicit/modelviews/MDPView.java b/prism/src/explicit/modelviews/MDPView.java index fb5b2121..e51c1c4f 100644 --- a/prism/src/explicit/modelviews/MDPView.java +++ b/prism/src/explicit/modelviews/MDPView.java @@ -27,7 +27,6 @@ package explicit.modelviews; -import java.util.HashSet; import java.util.Iterator; import java.util.Map.Entry; import java.util.PrimitiveIterator; @@ -89,25 +88,6 @@ public abstract class MDPView extends ModelView implements MDP, Cloneable //--- NondetModel --- - @Override - public boolean areAllChoiceActionsUnique() - { - final HashSet actions = new HashSet(); - for (int state = 0, numStates = getNumStates(); state < numStates; state++) { - final int numChoices = getNumChoices(state); - if (numChoices <= 1) { - continue; - } - actions.clear(); - for (int choice = 0; choice < numChoices; choice++) { - if (!actions.add(getAction(state, choice))) { - return false; - } - } - } - return true; - } - @Override public SuccessorsIterator getSuccessors(final int state, final int choice) { diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index 3a1a9d52..131e32ff 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -429,13 +429,6 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric