Add basic variable info to ModelInfo interface.

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

prism/src/parser/ast/ASTElement.java

@@ -311,7 +311,7 @@ public abstract class ASTElement
 	 * Find all references to variables, replace any identifier objects with variable objects,
 	 * check variables exist and store their index (as defined by the containing ModuleFile).
 	 */
-	public ASTElement findAllVars(Vector<String> varIdents, Vector<Type> varTypes) throws PrismLangException
+	public ASTElement findAllVars(List<String> varIdents, List<Type> varTypes) throws PrismLangException
 	{
 		FindAllVars visitor = new FindAllVars(varIdents, varTypes);
 		return (ASTElement) accept(visitor);

prism/src/parser/ast/PropertiesFile.java

@@ -289,7 +289,7 @@ public class PropertiesFile extends ASTElement
 		checkPropertyNames();
 
 		// Find all instances of variables (i.e. locate idents which are variables).
-		findAllVars(modulesFile.getVarNames(), modulesFile.getVarTypes());
+		findAllVars(modelInfo.getVarNames(), modelInfo.getVarTypes());
 
 		// Find all instances of property refs
 		findAllPropRefs(null, this);

prism/src/parser/visitor/FindAllVars.java

@@ -26,10 +26,12 @@
 
 package parser.visitor;
 
-import java.util.Vector;
+import java.util.List;
 
-import parser.ast.*;
-import parser.type.*;
+import parser.ast.ExpressionIdent;
+import parser.ast.ExpressionVar;
+import parser.ast.Update;
+import parser.type.Type;
 import prism.PrismLangException;
 
 /**
@@ -38,10 +40,10 @@ import prism.PrismLangException;
  */
 public class FindAllVars extends ASTTraverseModify
 {
-	private Vector<String> varIdents;
-	private Vector<Type> varTypes;
+	private List<String> varIdents;
+	private List<Type> varTypes;
 	
-	public FindAllVars(Vector<String> varIdents, Vector<Type> varTypes)
+	public FindAllVars(List<String> varIdents, List<Type> varTypes)
 	{
 		this.varIdents = varIdents;
 		this.varTypes = varTypes;
@@ -63,7 +65,7 @@ public class FindAllVars extends ASTTraverseModify
 				throw new PrismLangException(s, e.getVarIdent(i));
 			}
 			// Store the type
-			e.setType(i, varTypes.elementAt(j));
+			e.setType(i, varTypes.get(j));
 			// And store the variable index
 			e.setVarIndex(i, j);
 		}
@@ -76,7 +78,7 @@ public class FindAllVars extends ASTTraverseModify
 		i = varIdents.indexOf(e.getName());
 		if (i != -1) {
 			// If so, replace it with an ExpressionVar object
-			ExpressionVar expr = new ExpressionVar(e.getName(), varTypes.elementAt(i));
+			ExpressionVar expr = new ExpressionVar(e.getName(), varTypes.get(i));
 			expr.setPosition(e);
 			// Store variable index
 			expr.setIndex(i);

prism/src/prism/DefaultModelGenerator.java

@@ -32,6 +32,7 @@ import java.util.List;
 
 import parser.State;
 import parser.Values;
+import parser.type.Type;
 
 /**
  * Default implementation of the {@link ModelGenerator} interface
@@ -63,6 +64,15 @@ public abstract class DefaultModelGenerator implements ModelGenerator
 		return new Values();
 	}
 	
+	@Override
+	public abstract int getNumVars();
+	
+	@Override
+	public abstract List<String> getVarNames();
+	
+	@Override
+	public abstract List<Type> getVarTypes();
+	
 	@Override
 	public int getNumLabels()
 	{

prism/src/prism/ModelInfo.java

@@ -27,6 +27,10 @@
 
 package prism;
 
+import java.util.List;
+
+import parser.type.Type;
+
 /**
  * Interface for classes that provide some basic (syntactic) information about a probabilistic model.
  */
@@ -42,6 +46,31 @@ public interface ModelInfo
 	 */
 	public boolean containsUnboundedVariables();
 
+	/**
+	 * Get the number of variables in the model. 
+	 */
+	public int getNumVars();
+	
+	/**
+	 * Get the names of all the variables in the model.
+	 */
+	public List<String> getVarNames();
+	
+	/**
+	 * Get the types of all the variables in the model.
+	 */
+	public List<Type> getVarTypes();
+
+	/**
+	 * Get the name of the {@code i}th variable in the model.
+	 */
+	//public String getVarName(int i) throws PrismException;
+
+	/**
+	 * Get the type of the {@code i}th variable in the model.
+	 */
+	//public Type getVarType(int i) throws PrismException;
+
 	/**
 	 * Get the number of labels (atomic propositions) defined for the model. 
 	 */

prism/src/prism/TestModelGenerator.java

@@ -28,6 +28,8 @@ package prism;
 
 import java.io.File;
 import java.io.FileNotFoundException;
+import java.util.Arrays;
+import java.util.List;
 
 import parser.State;
 import parser.VarList;
@@ -35,6 +37,8 @@ import parser.ast.Declaration;
 import parser.ast.DeclarationInt;
 import parser.ast.Expression;
 import parser.ast.PropertiesFile;
+import parser.type.Type;
+import parser.type.TypeInt;
 import explicit.ConstructModel;
 import explicit.DTMCModelChecker;
 
@@ -43,6 +47,8 @@ public class TestModelGenerator extends DefaultModelGenerator
 	protected State exploreState;
 	protected int x;
 	protected int n;
+	protected List<String> varNames = Arrays.asList("x");
+	protected List<Type> varTypes = Arrays.asList((Type) TypeInt.getInstance());
 
 	public TestModelGenerator(int n)
 	{
@@ -55,6 +61,24 @@ public class TestModelGenerator extends DefaultModelGenerator
 		return ModelType.DTMC;
 	}
 
+	@Override
+	public int getNumVars()
+	{
+		return 1;
+	}
+	
+	@Override
+	public List<String> getVarNames()
+	{
+		return varNames;
+	}
+
+	@Override
+	public List<Type> getVarTypes()
+	{
+		return varTypes;
+	}
+
 	@Override
 	public int getNumLabels()
 	{
@@ -186,7 +210,7 @@ public class TestModelGenerator extends DefaultModelGenerator
 				TestModelGenerator modelGen2 = new TestModelGenerator(10);
 				prism.loadModelGenerator(modelGen2);
 				prism.exportTransToFile(true, Prism.EXPORT_DOT_STATES, new File("test2.dot"));
-				PropertiesFile pf = prism.parsePropertiesString(modelGen2, "P=? [F \"goal\"]");
+				PropertiesFile pf = prism.parsePropertiesString(modelGen2, "P=? [F x=10]");
 				Expression expr = pf.getProperty(0);
 				Result res = prism.modelCheck(pf, expr);
 				System.out.println(res);

prism/src/simulator/ModulesFileModelGenerator.java

@@ -10,6 +10,7 @@ import parser.ast.Expression;
 import parser.ast.LabelList;
 import parser.ast.ModulesFile;
 import parser.ast.RewardStruct;
+import parser.type.Type;
 import prism.DefaultModelGenerator;
 import prism.ModelType;
 import prism.PrismComponent;
@@ -124,6 +125,24 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator
 		return mfConstants;
 	}
 	
+	@Override
+	public int getNumVars()
+	{
+		return modulesFile.getNumVars();
+	}
+	
+	@Override
+	public List<String> getVarNames()
+	{
+		return modulesFile.getVarNames();
+	}
+
+	@Override
+	public List<Type> getVarTypes()
+	{
+		return modulesFile.getVarTypes();
+	}
+
 	@Override
 	public int getNumLabels()
 	{