From 2fe6c5d762aaff3fe95523f1a032e16e6f397f58 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 4 Dec 2015 04:27:13 +0000 Subject: [PATCH] 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 | 2 +- prism/src/parser/ast/PropertiesFile.java | 2 +- prism/src/parser/visitor/FindAllVars.java | 18 +++++++----- prism/src/prism/DefaultModelGenerator.java | 10 +++++++ prism/src/prism/ModelInfo.java | 29 +++++++++++++++++++ prism/src/prism/TestModelGenerator.java | 26 ++++++++++++++++- .../simulator/ModulesFileModelGenerator.java | 19 ++++++++++++ 7 files changed, 95 insertions(+), 11 deletions(-) diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 49f03601..83260575 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/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 varIdents, Vector varTypes) throws PrismLangException + public ASTElement findAllVars(List varIdents, List varTypes) throws PrismLangException { FindAllVars visitor = new FindAllVars(varIdents, varTypes); return (ASTElement) accept(visitor); diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 2b861e97..13254ee0 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/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); diff --git a/prism/src/parser/visitor/FindAllVars.java b/prism/src/parser/visitor/FindAllVars.java index d5d3fe4e..5e7c36f1 100644 --- a/prism/src/parser/visitor/FindAllVars.java +++ b/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 varIdents; - private Vector varTypes; + private List varIdents; + private List varTypes; - public FindAllVars(Vector varIdents, Vector varTypes) + public FindAllVars(List varIdents, List 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); diff --git a/prism/src/prism/DefaultModelGenerator.java b/prism/src/prism/DefaultModelGenerator.java index ffb1d5b7..339752e6 100644 --- a/prism/src/prism/DefaultModelGenerator.java +++ b/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 getVarNames(); + + @Override + public abstract List getVarTypes(); + @Override public int getNumLabels() { diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index ac6d5f5d..793a7b58 100644 --- a/prism/src/prism/ModelInfo.java +++ b/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 getVarNames(); + + /** + * Get the types of all the variables in the model. + */ + public List 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. */ diff --git a/prism/src/prism/TestModelGenerator.java b/prism/src/prism/TestModelGenerator.java index 9cc29839..a454d902 100644 --- a/prism/src/prism/TestModelGenerator.java +++ b/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 varNames = Arrays.asList("x"); + protected List 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 getVarNames() + { + return varNames; + } + + @Override + public List 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); diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 4afd7a57..499f79f9 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/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 getVarNames() + { + return modulesFile.getVarNames(); + } + + @Override + public List getVarTypes() + { + return modulesFile.getVarTypes(); + } + @Override public int getNumLabels() {