diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 81fe13e3..7e2d62b5 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -144,7 +144,7 @@ public class ConstructModel extends PrismComponent // Display a warning if there are unbounded vars VarList varList = modulesFile.createVarList(); - if (varList.containsUnboundedVariables()) + if (modulesFile.containsUnboundedVariables()) mainLog.printWarning("Model contains one or more unbounded variables: model construction may not terminate"); // Starting reachability... diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 08d32e91..99675e06 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -487,21 +487,6 @@ public class VarList return state; } - /** - * Does the variable list contain any variables with unbounded range (e.g. "clock: or "int")? - */ - public boolean containsUnboundedVariables() - { - int n = getNumVars(); - for (int i = 0; i < n; i++) { - DeclarationType declType = getDeclaration(i).getDeclType(); - if (declType instanceof DeclarationClock || declType instanceof DeclarationIntUnbounded) { - return true; - } - } - return false; - } - /** * Clone this list. */ diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index a0613efb..9836df7a 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -558,6 +558,18 @@ public class ModulesFile extends ASTElement return false; } + public boolean containsUnboundedVariables() + { + int n = getNumVars(); + for (int i = 0; i < n; i++) { + DeclarationType declType = getVarDeclaration(i).getDeclType(); + if (declType instanceof DeclarationClock || declType instanceof DeclarationIntUnbounded) { + return true; + } + } + return false; + } + /** * Method to "tidy up" after parsing (must be called) * (do some checks and extract some information) diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index c10ec384..9207b312 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -180,7 +180,7 @@ public class Modules2MTBDD // get variable info from ModulesFile varList = modulesFile.createVarList(); - if (varList.containsUnboundedVariables()) + if (modulesFile.containsUnboundedVariables()) throw new PrismNotSupportedException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)"); numVars = varList.getNumVars(); constantValues = modulesFile.getConstantValues();