Add areAllChoiceActionsUnique() method to NondetModel.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7603 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/MDPExplicit.java

@@ -30,6 +30,7 @@ package explicit;
 import java.io.FileWriter;
 import java.io.IOException;
 import java.util.BitSet;
+import java.util.HashSet;
 import java.util.Iterator;
 import java.util.Map;
 import java.util.TreeMap;
@@ -225,6 +226,26 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 		}
 	}
 
+	// Accessors (for NondetModel)
+	
+	@Override
+	public boolean areAllChoiceActionsUnique()
+	{
+		HashSet<Object> sActions = new HashSet<Object>();
+		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
@@ -340,7 +361,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 		}*/
 		return maxDiff;
 	}
-	
+
 	@Override
 	public Model constructInducedModel(MDStrategy strat)
 	{

prism/src/explicit/MDPSimple.java

@@ -508,7 +508,7 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 	}
 
 	// Accessors (for NondetModel)
-	
+
 	@Override
 	public int getNumChoices(int s)
 	{
@@ -547,13 +547,13 @@ public class MDPSimple extends MDPExplicit implements NondetModelSimple
 	{
 		return trans.get(s).get(i).isSubsetOf(set);
 	}
-	
+
 	@Override
 	public boolean someSuccessorsInSet(int s, int i, BitSet set)
 	{
 		return trans.get(s).get(i).containsOneOf(set);
 	}
-	
+
 	// Accessors (for MDP)
 
 	@Override

prism/src/explicit/NondetModel.java

@@ -59,6 +59,11 @@ public interface NondetModel extends Model
 	 */
 	public Object getAction(int s, int i);
 
+	/**
+	 * Do all choices in in each state have a unique action label?
+	 */
+	public boolean areAllChoiceActionsUnique();
+	
 	/**
 	 * Check if all the successor states from choice {@code i} of state {@code s} are in the set {@code set}.
 	 * @param s The state to check

prism/src/explicit/STPGAbstrSimple.java

@@ -487,6 +487,12 @@ 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)
 	{

prism/src/explicit/SubNondetModel.java

@@ -31,6 +31,7 @@ import java.io.File;
 import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
@@ -294,6 +295,12 @@ public class SubNondetModel implements NondetModel {
 		return model.getAction(s, i);
 	}
 
+	@Override
+	public boolean areAllChoiceActionsUnique()
+	{
+		throw new RuntimeException("Not implemented");
+	}
+
 	@Override
 	public boolean allSuccessorsInSet(int s, int i, BitSet set) {
 		s = translateState(s);