From e70e0f3b5567c073633f6afc57d5a6318b04726d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 16 Jun 2020 12:24:43 +0100 Subject: [PATCH] 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 | 19 +++++ prism/src/parser/VarList.java | 33 +++----- prism/src/parser/ast/ModulesFile.java | 25 +++++- prism/src/prism/ExplicitFiles2ModelInfo.java | 47 ++++-------- prism/src/prism/ModelInfo.java | 76 ++++++++++++++++++- prism/src/prism/TestModelGenerator.java | 26 +++---- prism/src/pta/DigitalClocks.java | 2 +- .../simulator/ModulesFileModelGenerator.java | 33 ++++++-- .../ModulesFileModelGeneratorSymbolic.java | 33 ++++++-- 9 files changed, 202 insertions(+), 92 deletions(-) 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