Simplify ModelGenerator/ModelInfo interfaces slightly.

* Remove some unneeded methods: getExploreState() and getTransitionAction(int i)
* Add a default implementation of getNumVars() based on name list

Existing code which implements the first two methods and annotates them with @Override needs to be changed.

TestModelGenerator, ModulesFileModelGenerator, ModulesFileModelGeneratorSymbolic updated accordingly.

prism/src/prism/ModelGenerator.java

@@ -73,12 +73,6 @@ public interface ModelGenerator extends ModelInfo
 	 */
 	public void exploreState(State exploreState) throws PrismException;
 
-	/**
-	 * Get the state that is currently being explored, i.e. the last one for which
-	 * {@link #exploreState(State)} was called. Can return null if there is no such state. 
-	 */
-	public State getExploreState();
-	
 	/**
 	 * Get the number of nondeterministic choices in the current state.
 	 */
@@ -104,15 +98,6 @@ public interface ModelGenerator extends ModelInfo
 	 */
 	public int getNumTransitions(int i) throws PrismException;
 
-	/**
-	 * Get the action label of a transition, 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: For most types of models, the action label will be the same for all transitions within
-	 * the same nondeterministic choice, so it is better to query the action by choice, not transition.
-	 */
-	public Object getTransitionAction(int i) throws PrismException;
-
 	/**
 	 * Get the action label of a transition within a choice, specified by its index/offset.
 	 * The label can be any Object, but will often be treated as a string, so it should at least

prism/src/prism/ModelInfo.java

@@ -32,6 +32,10 @@ import java.util.List;
 
 import parser.Values;
 import parser.VarList;
+import parser.ast.Declaration;
+import parser.ast.DeclarationBool;
+import parser.ast.DeclarationInt;
+import parser.ast.Expression;
 import parser.ast.RewardStruct;
 import parser.type.Type;
 
@@ -105,7 +109,11 @@ public interface ModelInfo
 	/**
 	 * Get the number of variables in the model. 
 	 */
-	public int getNumVars();
+	public default int getNumVars()
+	{
+		// Default implementation just extracts from getVarNames() 
+		return getVarNames().size();
+	}
 	
 	/**
 	 * Get the names of all the variables in the model.

prism/src/prism/TestModelGenerator.java

@@ -61,12 +61,6 @@ public class TestModelGenerator implements ModelGenerator
 		return ModelType.DTMC;
 	}
 
-	@Override
-	public int getNumVars()
-	{
-		return 1;
-	}
-	
 	@Override
 	public List<String> getVarNames()
 	{
@@ -79,12 +73,6 @@ public class TestModelGenerator implements ModelGenerator
 		return varTypes;
 	}
 
-	@Override
-	public int getNumLabels()
-	{
-		return 1;
-	}
-	
 	@Override
 	public List<String> getLabelNames()
 	{
@@ -106,12 +94,6 @@ public class TestModelGenerator implements ModelGenerator
 		x = ((Integer) exploreState.varValues[0]).intValue();
 	}
 
-	@Override
-	public State getExploreState()
-	{
-		return exploreState;
-	}
-
 	@Override
 	public int getNumChoices() throws PrismException
 	{
@@ -124,12 +106,6 @@ public class TestModelGenerator implements ModelGenerator
 		return x > 0 && x < n ? 2 : 1;
 	}
 
-	@Override
-	public Object getTransitionAction(int i) throws PrismException
-	{
-		return null;
-	}
-
 	@Override
 	public Object getTransitionAction(int i, int offset) throws PrismException
 	{

prism/src/simulator/ModulesFileModelGenerator.java

@@ -265,12 +265,6 @@ public class ModulesFileModelGenerator implements ModelGenerator
 		transitionListBuilt = false;
 	}
 	
-	@Override
-	public State getExploreState()
-	{
-		return exploreState;
-	}
-	
 	@Override
 	public int getNumChoices() throws PrismException
 	{
@@ -289,13 +283,6 @@ public class ModulesFileModelGenerator implements ModelGenerator
 		return getTransitionList().getChoice(index).size();
 	}
 
-	@Override
-	public String getTransitionAction(int index) throws PrismException
-	{
-		int a = getTransitionList().getTransitionModuleOrActionIndex(index);
-		return a < 0 ? null : modulesFile.getSynch(a - 1);
-	}
-
 	@Override
 	public String getTransitionAction(int index, int offset) throws PrismException
 	{

prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

@@ -294,12 +294,6 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		transitionListBuilt = false;
 	}
 	
-	@Override
-	public State getExploreState()
-	{
-		return exploreState;
-	}
-	
 	@Override
 	public int getNumChoices() throws PrismException
 	{
@@ -318,13 +312,6 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		return getTransitionList().getChoice(index).size();
 	}
 
-	@Override
-	public String getTransitionAction(int index) throws PrismException
-	{
-		int a = getTransitionList().getTransitionModuleOrActionIndex(index);
-		return a < 0 ? null : modulesFile.getSynch(a - 1);
-	}
-
 	@Override
 	public String getTransitionAction(int index, int offset) throws PrismException
 	{