From 1d3363ab89ba097f9f6c7fbbe97c9d26d06c73c7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 16 Jun 2020 00:43:40 +0100 Subject: [PATCH] Don't store Declaration objects in VarList. Instead, store the variable name and DeclarationType separately. DeclarationType stores the type info we actually need, e.g., ranges for bounded integer variables. Declaration has other information such as initial values, which is not needed here. A new addVar(name, declType) method is added (and preferred). Methods to add variables via Declarations remain, for convenience. --- prism/src/parser/VarList.java | 91 ++++++++++++----------- prism/src/prism/ModelGenerator2MTBDD.java | 2 +- 2 files changed, 49 insertions(+), 44 deletions(-) diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index d1a045e8..fefc257e 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -29,6 +29,7 @@ package parser; import java.util.*; import prism.*; +import parser.VarList.Var; import parser.ast.*; import parser.type.*; @@ -96,10 +97,7 @@ public class VarList */ public void addVar(Declaration decl, int module, Values constantValues) throws PrismLangException { - Var var = createVar(decl, module, constantValues); - vars.add(var); - totalNumBits += getRangeLogTwo(vars.size() - 1); - nameMap.put(decl.getName(), vars.size() - 1); + addVar(decl.getName(), decl.getDeclType(), module, constantValues); } /** @@ -110,7 +108,7 @@ public class VarList */ public void addVar(int i, Declaration decl, int module, Values constantValues) throws PrismLangException { - Var var = createVar(decl, module, constantValues); + Var var = createVar(decl.getName(), decl.getDeclType(), module, constantValues); vars.add(i, var); totalNumBits += getRangeLogTwo(i); // Recompute name map @@ -122,26 +120,38 @@ public class VarList } } + /** + * Add a new variable to the end of the VarList. + * @param name Variable name + * @param declType Type declaration defining the variable + * @param module Index of module containing variable + * @param constantValues Values of constants needed to evaluate low/high/etc. + */ + public void addVar(String name, DeclarationType declType, int module, Values constantValues) throws PrismLangException + { + Var var = createVar(name, declType, module, constantValues); + vars.add(var); + totalNumBits += getRangeLogTwo(vars.size() - 1); + nameMap.put(name, vars.size() - 1); + } + /** * Create a new variable object to the store in the list. - * @param decl Declaration defining the variable + * @param name Variable name + * @param declType Type declaration defining the variable * @param module Index of module containing variable * @param constantValues Values of constants needed to evaluate low/high/etc. */ - private Var createVar(Declaration decl, int module, Values constantValues) throws PrismLangException + private Var createVar(String name, DeclarationType declType, int module, Values constantValues) throws PrismLangException { Var var; int low, high; - DeclarationType declType; // Create new Var object - var = new Var(); - - // Store name/type/module - var.decl = decl; + var = new Var(name, declType.getType()); + var.declType = declType; var.module = module; - - declType = decl.getDeclType(); + // Variable is a bounded integer if (declType instanceof DeclarationInt) { DeclarationInt intdecl = (DeclarationInt) declType; @@ -149,12 +159,12 @@ public class VarList high = intdecl.getHigh().evaluateInt(constantValues); // Check range is valid if (high - low <= 0) { - String s = "Invalid range (" + low + "-" + high + ") for variable \"" + decl.getName() + "\""; - throw new PrismLangException(s, decl); + String s = "Invalid range (" + low + "-" + high + ") for variable \"" + name + "\""; + throw new PrismLangException(s, declType); } if ((long) high - (long) low >= Integer.MAX_VALUE) { - String s = "Range for variable \"" + decl.getName() + "\" (" + low + "-" + high + ") is too big"; - throw new PrismLangException(s, decl); + String s = "Range for variable \"" + name + "\" (" + low + "-" + high + ") is too big"; + throw new PrismLangException(s, declType); } } // Variable is a Boolean @@ -175,7 +185,7 @@ public class VarList high = 1; } else { - throw new PrismLangException("Unknown variable type \"" + declType + "\" in declaration", decl); + throw new PrismLangException("Unknown variable type \"" + declType + "\" in declaration", declType); } // Store low/high and return @@ -212,24 +222,11 @@ public class VarList } /** - * Get the declaration of the ith variable in this list. + * Get the declaration type of the ith variable in this list. */ - public Declaration getDeclaration(int i) + public DeclarationType getDeclarationType(int i) { - return vars.get(i).decl; - } - - /** - * Get the index in this VarList for a given declaration. - */ - public int getIndexFromDeclaration(Declaration d) - { - for (int i=0;i