ModelGenerator (actually ModelInfo) improvements.

A default implementation of createVarList() in ModelInfo now creates
a VarList automatically, so this does not need to be implemented when
creating a ModelGenerator. Instead, just getVarDeclarationType(int i),
which is a newly added method, should be implemented. There is also
a default implementation of this, but it assumes that integer variables
are unbounded, which will not work with the symbolic engine.

In a related change, ModelInfo can now optionally specify which "module"
a variable belongs to (via getVarModuleIndex and getModuleName).

ModulesFile is updated, to fully support the new version of ModelInfo,
and all implementations of ModelGenerator are simplified where possible.
The old VarList constructor which takes a ModulesFile is removed and
replaced with one which takes a ModelInfo object.

prism/src/explicit/ModelModelGenerator.java

@@ -33,6 +33,7 @@ import java.util.Map;
 
 import parser.State;
 import parser.VarList;
+import parser.ast.DeclarationType;
 import parser.type.Type;
 import prism.ModelGenerator;
 import prism.ModelInfo;
@@ -95,6 +96,24 @@ public class ModelModelGenerator implements ModelGenerator
 		return modelInfo.getVarTypes();
 	}
 
+	@Override
+	public DeclarationType getVarDeclarationType(int i) throws PrismException
+	{
+		return modelInfo.getVarDeclarationType(i);
+	}
+
+	@Override
+	public int getVarModuleIndex(int i)
+	{
+		return modelInfo.getVarModuleIndex(i);
+	}
+	
+	@Override
+	public String getModuleName(int i)
+	{
+		return modelInfo.getModuleName(i);
+	}
+	
 	@Override
 	public VarList createVarList() throws PrismException
 	{

prism/src/parser/VarList.java

@@ -60,32 +60,17 @@ public class VarList
 	}
 
 	/**
-	 * Construct variable list for a ModulesFile.
-	 */
-	public VarList(ModulesFile modulesFile) throws PrismLangException
+	* Construct variable list for a ModelInfo object.
+	*/
+	public VarList(ModelInfo modelInfo) throws PrismException
 	{
 		this();
 
-		int i, j, n, n2;
-		parser.ast.Module module;
-		Declaration decl;
-
-		// First add all globals to the list
-		n = modulesFile.getNumGlobals();
-		for (i = 0; i < n; i++) {
-			decl = modulesFile.getGlobal(i);
-			addVar(decl, -1, modulesFile.getConstantValues());
-		}
-
-		// Then add all module variables to the list
-		n = modulesFile.getNumModules();
-		for (i = 0; i < n; i++) {
-			module = modulesFile.getModule(i);
-			n2 = module.getNumDeclarations();
-			for (j = 0; j < n2; j++) {
-				decl = module.getDeclaration(j);
-				addVar(decl, i, modulesFile.getConstantValues());
-			}
+		int numVars = modelInfo.getNumVars();
+		for (int i = 0; i < numVars; i++) {
+			DeclarationType declType = modelInfo.getVarDeclarationType(i);
+			int module = modelInfo.getVarModuleIndex(i);
+			addVar(modelInfo.getVarName(i), declType, module, modelInfo.getConstantValues());
 		}
 	}
 	 

prism/src/parser/ast/ModulesFile.java

@@ -74,10 +74,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 	private String[] moduleNames;
 	// List of synchronising actions
 	private Vector<String> synchs;
-	// Lists of variable info (declaration, name, type)
+	// Lists of variable info (declaration, name, type, module index)
 	private Vector<Declaration> varDecls;
 	private Vector<String> varNames;
 	private Vector<Type> varTypes;
+	private Vector<Integer> varModules;
 
 	// Values set for undefined constants (null if none)
 	private Values undefinedConstantValues;
@@ -103,6 +104,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		varDecls = new Vector<Declaration>();
 		varNames = new Vector<String>();
 		varTypes = new Vector<Type>();
+		varModules = new Vector<Integer>();
 		undefinedConstantValues = null;
 		constantValues = null;
 	}
@@ -657,6 +659,18 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		return varTypes;
 	}
 
+	@Override
+	public DeclarationType getVarDeclarationType(int i)
+	{
+		return varDecls.get(i).getDeclType();
+	}
+
+	@Override
+	public int getVarModuleIndex(int i)
+	{
+		return varModules.get(i);
+	}
+
 	public boolean isGlobalVariable(String s)
 	{
 		int i, n;
@@ -694,6 +708,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		varDecls.clear();
 		varNames.clear();
 		varTypes.clear();
+		varModules.clear();
 		
 		// Expansion of formulas and renaming
 
@@ -939,6 +954,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 			varDecls.add(getGlobal(i));
 			varNames.add(s);
 			varTypes.add(getGlobal(i).getType());
+			varModules.add(-1);
 		}
 
 		// locals
@@ -952,6 +968,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 				varDecls.add(module.getDeclaration(j));
 				varNames.add(s);
 				varTypes.add(module.getDeclaration(j).getType());
+				varModules.add(i);
 			}
 		}
 
@@ -1232,11 +1249,13 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		varDecls = new Vector<Declaration>();
 		varNames = new Vector<String>();
 		varTypes = new Vector<Type>();
+		varModules = new Vector<Integer>();
 		// Globals
 		for (Declaration decl : globals) {
 			varDecls.add(decl);
 			varNames.add(decl.getName());
 			varTypes.add(decl.getType());
+			varModules.add(-1);
 		}
 		// Locals
 		n = modules.size();
@@ -1245,6 +1264,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 				varDecls.add(decl);
 				varNames.add(decl.getName());
 				varTypes.add(decl.getType());
+				varModules.add(i);
 			}
 		}
 		// Find all instances of variables, replace identifiers with variables.
@@ -1257,7 +1277,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 	 * Assumes that values for constants have been provided for the model.
 	 * Also performs various syntactic checks on the variables.   
 	 */
-	public VarList createVarList() throws PrismLangException
+	public VarList createVarList() throws PrismException
 	{
 		return new VarList(this);
 	}
@@ -1393,6 +1413,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		}
 		ret.varNames = (varNames == null) ? null : (Vector<String>)varNames.clone();
 		ret.varTypes = (varTypes == null) ? null : (Vector<Type>)varTypes.clone();
+		ret.varModules = (varModules == null) ? null : (Vector<Integer>)varModules.clone();
 		ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
 		
 		return ret;

prism/src/prism/ExplicitFiles2ModelInfo.java

@@ -37,8 +37,6 @@ import java.util.List;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
-import parser.VarList;
-import parser.ast.Declaration;
 import parser.ast.DeclarationBool;
 import parser.ast.DeclarationInt;
 import parser.ast.DeclarationType;
@@ -59,7 +57,9 @@ public class ExplicitFiles2ModelInfo extends PrismComponent
 	private int numVars;
 	private List<String> varNames;
 	private List<Type> varTypes;
-	private VarList varList;
+	private int varMins[];
+	private int varMaxs[];
+	private int varRanges[];
 	private List<String> labelNames;
 	
 	// Num states
@@ -142,9 +142,13 @@ public class ExplicitFiles2ModelInfo extends PrismComponent
 			}
 			
 			@Override
-			public VarList createVarList() throws PrismException
+			public DeclarationType getVarDeclarationType(int i) throws PrismException
 			{
-				return varList;
+				if (varTypes.get(i) instanceof TypeInt) {
+					return new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i]));
+				} else {
+					return new DeclarationBool();
+				}
 			}
 			
 			@Override
@@ -187,12 +191,6 @@ public class ExplicitFiles2ModelInfo extends PrismComponent
 	private void extractVarInfoFromStatesFile(File statesFile) throws PrismException
 	{
 		int i, j, lineNum = 0;
-		Declaration d;
-		DeclarationType dt;
-		// Var info
-		int varMins[];
-		int varMaxs[];
-		int varRanges[];
 
 		// open file for reading, automatic close when done
 		try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) {
@@ -271,20 +269,6 @@ public class ExplicitFiles2ModelInfo extends PrismComponent
 		} catch (PrismException e) {
 			throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of states file \"" + statesFile + "\"");
 		}
-		
-		varList = new VarList();
-		for (i = 0; i < numVars; i++) {
-			if (varTypes.get(i) instanceof TypeInt) {
-				dt = new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i]));
-				d = new Declaration(varNames.get(i), dt);
-				d.setStart(Expression.Int(varMins[i]));
-			} else {
-				dt = new DeclarationBool();
-				d = new Declaration(varNames.get(i), dt);
-				d.setStart(Expression.False());
-			}
-			varList.addVar(d, -1, null);
-		}
 	}
 
 	/**
@@ -308,12 +292,13 @@ public class ExplicitFiles2ModelInfo extends PrismComponent
 		} catch (NumberFormatException e) {
 			throw new PrismException("Error detected at line 1 of transition matrix file \"" + transFile + "\"");
 		}
-		
-		varList = new VarList();
-		DeclarationType dt = new DeclarationInt(Expression.Int(0), Expression.Int(numStates - 1));
-		Declaration d = new Declaration("x", dt);
-		d.setStart(Expression.Int(0));
-		varList.addVar(d, -1, null);
+		// Store dummy variable info
+		numVars = 1;
+		varNames = Collections.singletonList("x");
+		varTypes = Collections.singletonList(TypeInt.getInstance());
+		varMins = new int[] { 0 };
+		varMaxs = new int[] { numStates - 1 };
+		varRanges = new int[] { numStates - 1 };
 	}
 	
 

prism/src/prism/ModelInfo.java

@@ -32,7 +32,12 @@ import java.util.List;
 
 import parser.Values;
 import parser.VarList;
+import parser.ast.DeclarationBool;
+import parser.ast.DeclarationIntUnbounded;
+import parser.ast.DeclarationType;
 import parser.type.Type;
+import parser.type.TypeBool;
+import parser.type.TypeInt;
 
 /**
  * Interface for classes that provide some basic (syntactic) information about a probabilistic model.
@@ -150,6 +155,74 @@ public interface ModelInfo
 		return getVarTypes().get(i);
 	}
 
+	/**
+	 * Get a declaration providing more information about
+	 * the type of the {@code i}th variable in the model.
+	 * For example, for integer variables, this can define
+	 * the lower and upper bounds of the range of the variable.
+	 * This is specified using a subclass of {@link DeclarationType},
+	 * which specifies info such as bounds using {@link Expression} objects.
+	 * These can use constants which will later be supplied,
+	 * e.g., via the {@link #setSomeUndefinedConstants(Values) method.
+	 * If this method is not provided, a default implementation supplies sensible
+	 * declarations, but these are _unbounded_ for integers.
+	 * {@code i} should always be between 0 and getNumVars() - 1.
+	 */
+	public default DeclarationType getVarDeclarationType(int i) throws PrismException
+	{
+		Type type = getVarType(i);
+		// Construct default declarations for basic types (int/boolean)
+		if (type instanceof TypeInt) {
+			return new DeclarationIntUnbounded();
+		} else if (type instanceof TypeBool) {
+			return new DeclarationBool();
+		}
+		throw new PrismException("No default declaration avaiable for type " + type);
+	}
+	
+	/**
+	 * Get the (optionally specified) "module" that the {@code i}th variable in
+	 * the model belongs to (e.g., the PRISM language divides models into such modules).
+	 * This method returns the index of module; use {@link #getModuleName(int)}
+	 * to obtain the name of the corresponding module.
+	 * If there is no module info, or the variable is "global" and does not belong
+	 * to a specific model, this returns -1. A default implementation always returns -1.
+	 * {@code i} should always be between 0 and getNumVars() - 1.
+	 */
+	public default int getVarModuleIndex(int i)
+	{
+		// Default is -1 (unspecified or "global")
+		return -1;
+	}
+
+	/**
+	 * Get the name of the {@code i}th "module"; these are optionally used to
+	 * organise variables within the model, e.g., in the PRISM modelling language.
+	 * The module containing a variable is available via {@link #getVarModuleIndex(int)}.
+	 * This method should return a valid module name for any (non -1)
+	 * value returned by {@link #getVarModuleIndex(int)}.
+	 */
+	public default String getModuleName(int i)
+	{
+		// No names needed by default
+		return null;
+	}
+
+	/**
+	 * Create a {@link VarList} object, collating information about all the variables
+	 * in the model. This provides various helper functions to work with variables.
+	 * This list is created once all undefined constant values have been provided.
+	 * A default implementation of this method creates a {@link VarList} object
+	 * automatically from the variable info supplied by {@link ModelInfo}.
+	 * Generally, this requires {@link #getVarDeclarationType(int)} to
+	 * be properly implemented (beyond the default implementation) so that
+	 * variable ranges can be determined.
+	 */
+	public default VarList createVarList() throws PrismException
+	{
+		return new VarList(this); 
+	}
+	
 	/**
 	 * Get a short description of the action strings associated with transitions/choices.
 	 * For example, for a PRISM model, this is "Module/[action]".
@@ -201,7 +274,4 @@ public interface ModelInfo
 		// Default implementation just extracts from getLabelNames() 
 		return getLabelNames().indexOf(name);
 	}
-	
-	// TODO: can we remove this?
-	public VarList createVarList() throws PrismException;
 }

prism/src/prism/TestModelGenerator.java

@@ -31,16 +31,15 @@ import java.io.FileNotFoundException;
 import java.util.Arrays;
 import java.util.List;
 
+import explicit.ConstructModel;
+import explicit.DTMCModelChecker;
 import parser.State;
-import parser.VarList;
-import parser.ast.Declaration;
 import parser.ast.DeclarationInt;
+import parser.ast.DeclarationType;
 import parser.ast.Expression;
 import parser.ast.PropertiesFile;
 import parser.type.Type;
 import parser.type.TypeInt;
-import explicit.ConstructModel;
-import explicit.DTMCModelChecker;
 
 public class TestModelGenerator implements ModelGenerator
 {
@@ -73,6 +72,12 @@ public class TestModelGenerator implements ModelGenerator
 		return varTypes;
 	}
 
+	@Override
+	public DeclarationType getVarDeclarationType(int i) throws PrismException
+	{
+		return new DeclarationInt(Expression.Int(0), Expression.Int(n));
+	}
+	
 	@Override
 	public List<String> getLabelNames()
 	{
@@ -140,19 +145,6 @@ public class TestModelGenerator implements ModelGenerator
 		}
 	}
 
-	@Override
-	public VarList createVarList()
-	{
-		VarList varList = new VarList();
-		try {
-			varList.addVar(new Declaration("x", new DeclarationInt(Expression.Int(0), Expression.Int(n))), 0, null);
-		} catch (PrismLangException e) {
-			// TODO Auto-generated catch block
-			e.printStackTrace();
-		}
-		return varList;
-	}
-	
 	public static void main(String args[])
 	{
 		try {

prism/src/pta/DigitalClocks.java

@@ -108,7 +108,7 @@ public class DigitalClocks
 	/**
 	 * Main method - translate.
 	 */
-	public void translate(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression propertyToCheck) throws PrismLangException
+	public void translate(ModulesFile modulesFile, PropertiesFile propertiesFile, Expression propertyToCheck) throws PrismException
 	{
 		int i, n;
 		ASTElement ast;

prism/src/simulator/ModulesFileModelGenerator.java

@@ -6,6 +6,7 @@ import java.util.List;
 import parser.State;
 import parser.Values;
 import parser.VarList;
+import parser.ast.DeclarationType;
 import parser.ast.Expression;
 import parser.ast.LabelList;
 import parser.ast.ModulesFile;
@@ -90,7 +91,7 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 	 * (Re-)Initialise the class ready for model exploration
 	 * (can only be done once any constants needed have been provided)
 	 */
-	private void initialise() throws PrismLangException
+	private void initialise() throws PrismException
 	{
 		// Evaluate constants on (a copy) of the modules file, insert constant values and optimize arithmetic expressions
 		modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify();
@@ -165,6 +166,30 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 		return modulesFile.getVarTypes();
 	}
 
+	@Override
+	public DeclarationType getVarDeclarationType(int i) throws PrismException
+	{
+		return modulesFile.getVarDeclarationType(i);
+	}
+	
+	@Override
+	public int getVarModuleIndex(int i)
+	{
+		return modulesFile.getVarModuleIndex(i);
+	}
+	
+	@Override
+	public String getModuleName(int i)
+	{
+		return modulesFile.getModuleName(i);
+	}
+	
+	@Override
+	public VarList createVarList() throws PrismException
+	{
+		return varList;
+	}
+	
 	@Override
 	public int getNumLabels()
 	{
@@ -195,12 +220,6 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 		return labelList.getLabelIndex(label);
 	}
 	
-	@Override
-	public VarList createVarList()
-	{
-		return varList;
-	}
-	
 	// Methods for ModelGenerator interface
 	
 	@Override

prism/src/simulator/ModulesFileModelGeneratorSymbolic.java

@@ -11,6 +11,7 @@ import parser.State;
 import parser.Values;
 import parser.VarList;
 import parser.ast.ConstantList;
+import parser.ast.DeclarationType;
 import parser.ast.Expression;
 import parser.ast.LabelList;
 import parser.ast.ModulesFile;
@@ -110,7 +111,7 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 	 * (Re-)Initialise the class ready for model exploration
 	 * (can only be done once any constants needed have been provided)
 	 */
-	private void initialise() throws PrismLangException
+	private void initialise() throws PrismException
 	{
 		// Evaluate constants on (a copy) of the modules file, insert constant values
 		// Note that we don't optimise expressions since this can create some round-off issues
@@ -198,6 +199,30 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		return modulesFile.getVarTypes();
 	}
 
+	@Override
+	public DeclarationType getVarDeclarationType(int i) throws PrismException
+	{
+		return modulesFile.getVarDeclarationType(i);
+	}
+	
+	@Override
+	public int getVarModuleIndex(int i)
+	{
+		return modulesFile.getVarModuleIndex(i);
+	}
+	
+	@Override
+	public String getModuleName(int i)
+	{
+		return modulesFile.getModuleName(i);
+	}
+	
+	@Override
+	public VarList createVarList() throws PrismException
+	{
+		return varList;
+	}
+	
 	@Override
 	public int getNumLabels()
 	{
@@ -228,12 +253,6 @@ public class ModulesFileModelGeneratorSymbolic implements ModelGeneratorSymbolic
 		return labelList.getLabelIndex(label);
 	}
 	
-	@Override
-	public VarList createVarList()
-	{
-		return varList;
-	}
-	
 	// Methods for ModelGenerator interface
 	
 	@Override