From 844a87dadcf527d4b1e8baa2574a9e5a2a0b28bd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 15 Jun 2020 07:29:02 +0100 Subject: [PATCH] Remove initial variable value info from VarList. VarList should focus on the range, structure, etc. of the variables. The initial values of the variables for a model are stored separately. This info was only accessed from Modules2MTBDD, which now extracts initial variable values itself, and uses the VarList.encodeToInt helper method. Checking that bounded integer vars are in range is now moved there. --- prism/src/parser/VarList.java | 36 ++++++++++-------------------- prism/src/prism/Modules2MTBDD.java | 12 ++++++++-- 2 files changed, 22 insertions(+), 26 deletions(-) diff --git a/prism/src/parser/VarList.java b/prism/src/parser/VarList.java index 985de787..d1a045e8 100644 --- a/prism/src/parser/VarList.java +++ b/prism/src/parser/VarList.java @@ -35,7 +35,7 @@ import parser.type.*; /** * Class to store information about the set of variables in a PRISM model. * Assumes that any constants in the model have been given fixed values. - * Thus, initial/min/max values for all variables are known. + * Thus, min/max values for all variables are known. * VarList also takes care of how each variable will be encoded to an integer * (e.g. for (MT)BDD representation). */ @@ -131,7 +131,7 @@ public class VarList private Var createVar(Declaration decl, int module, Values constantValues) throws PrismLangException { Var var; - int low, high, start; + int low, high; DeclarationType declType; // Create new Var object @@ -147,7 +147,6 @@ public class VarList DeclarationInt intdecl = (DeclarationInt) declType; low = intdecl.getLow().evaluateInt(constantValues); high = intdecl.getHigh().evaluateInt(constantValues); - start = decl.getStartOrDefault().evaluateInt(constantValues); // Check range is valid if (high - low <= 0) { String s = "Invalid range (" + low + "-" + high + ") for variable \"" + decl.getName() + "\""; @@ -157,40 +156,31 @@ public class VarList String s = "Range for variable \"" + decl.getName() + "\" (" + low + "-" + high + ") is too big"; throw new PrismLangException(s, decl); } - // Check start is valid - if (start < low || start > high) { - String s = "Invalid initial value (" + start + ") for variable \"" + decl.getName() + "\""; - throw new PrismLangException(s, decl); - } } // Variable is a Boolean else if (declType instanceof DeclarationBool) { low = 0; high = 1; - start = (decl.getStartOrDefault().evaluateBoolean(constantValues)) ? 1 : 0; } // Variable is a clock else if (declType instanceof DeclarationClock) { // Create dummy info low = 0; high = 1; - start = 0; } // Variable is an (unbounded) integer else if (declType instanceof DeclarationIntUnbounded) { // Create dummy range info low = 0; high = 1; - start = decl.getStartOrDefault().evaluateInt(constantValues); } else { throw new PrismLangException("Unknown variable type \"" + declType + "\" in declaration", decl); } - // Store low/high/start and return + // Store low/high and return var.low = low; var.high = high; - var.start = start; return var; } @@ -306,14 +296,6 @@ public class VarList return totalNumBits; } - /** - * Get the initial value of the ith variable in this list (when encoded as an integer). - */ - public int getStart(int i) - { - return vars.get(i).start; - } - /** * Get the value (as an Object) for the ith variable, from its encoding as an integer. */ @@ -336,6 +318,7 @@ public class VarList * Get the integer encoding of a value for the ith variable, specified as an Object. * The Object is assumed to be of correct type (e.g. Integer, Boolean). * Throws an exception if Object is of the wrong type. + * Also throws an exception if the value is out of range. */ public int encodeToInt(int i, Object val) throws PrismLangException { @@ -343,7 +326,11 @@ public class VarList try { // Integer type if (type instanceof TypeInt) { - return ((TypeInt) type).castValueTo(val).intValue() - getLow(i); + int intVal = ((TypeInt) type).castValueTo(val).intValue(); + if (intVal < getLow(i) || intVal > getHigh(i)) { + throw new PrismLangException("Value " + val + " out of range for variable " + getName(i)); + } + return intVal - getLow(i); } // Boolean type else if (type instanceof TypeBool) { @@ -368,6 +355,9 @@ public class VarList if (type instanceof TypeInt) { try { int iVal = Integer.parseInt(s); + if (iVal < getLow(i) || iVal > getHigh(i)) { + throw new PrismLangException("Value " + iVal + " out of range for variable " + getName(i)); + } return iVal - getLow(i); } catch (NumberFormatException e) { throw new PrismLangException("\"" + s + "\" is not a valid integer value"); @@ -529,7 +519,6 @@ public class VarList // Info about how variable is encoded as an integer public int low; public int high; - public int start; // Default constructor public Var() @@ -543,7 +532,6 @@ public class VarList module = var.module; low = var.low; high = var.high; - start = var.start; } } } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index bb9b47ab..45fde5b6 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -2066,8 +2066,16 @@ public class Modules2MTBDD else { start = JDD.Constant(1); for (i = 0; i < numVars; i++) { - tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], varList.getStart(i)-varList.getLow(i), 1); - start = JDD.And(start, tmp); + Object startObj = modulesFile.getVarDeclaration(i).getStartOrDefault().evaluate(constantValues); + try { + int startInt = varList.encodeToInt(i, startObj); + tmp = JDD.SetVectorElement(JDD.Constant(0), varDDRowVars[i], startInt, 1); + start = JDD.And(start, tmp); + } catch (PrismLangException e) { + // attach initial value spec for better error reporting + e.setASTElement(modulesFile.getVarDeclaration(i).getStart()); + throw e; + } } } }