diff --git a/prism/src/explicit/ModelModelGenerator.java b/prism/src/explicit/ModelModelGenerator.java index 50970600..f4c510fa 100644 --- a/prism/src/explicit/ModelModelGenerator.java +++ b/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 { diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index fefc257e..5a9cdb57 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -60,35 +60,20 @@ 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()); } } - + /** * Add a new variable to the end of the VarList. * @param decl Declaration defining the variable diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index dddb09e8..5de6d999 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/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 synchs; - // Lists of variable info (declaration, name, type) + // Lists of variable info (declaration, name, type, module index) private Vector varDecls; private Vector varNames; private Vector varTypes; + private Vector 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(); varNames = new Vector(); varTypes = new Vector(); + varModules = new Vector(); 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(); varNames = new Vector(); varTypes = new Vector(); + varModules = new Vector(); // 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)varNames.clone(); ret.varTypes = (varTypes == null) ? null : (Vector)varTypes.clone(); + ret.varModules = (varModules == null) ? null : (Vector)varModules.clone(); ret.constantValues = (constantValues == null) ? null : new Values(constantValues); return ret; diff --git a/prism/src/prism/ExplicitFiles2ModelInfo.java b/prism/src/prism/ExplicitFiles2ModelInfo.java index 7422f454..867081e6 100644 --- a/prism/src/prism/ExplicitFiles2ModelInfo.java +++ b/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 varNames; private List varTypes; - private VarList varList; + private int varMins[]; + private int varMaxs[]; + private int varRanges[]; private List 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 }; } diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 5d21075b..110ee765 100644 --- a/prism/src/prism/ModelInfo.java +++ b/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; } diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 569c0dad..2b8b20d2 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/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 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 { diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 8989536b..420555ab 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/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; diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 2aed6b77..bd3a71a5 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/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 diff --git a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java b/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java index 83b914c6..9f0efb8f 100644 --- a/prism/src/simulator/ModulesFileModelGeneratorSymbolic.java +++ b/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