From f5b7af9c98373fbc0897945e49dd64e392f17b46 Mon Sep 17 00:00:00 2001 From: ep2016 Date: Tue, 18 Sep 2018 12:26:35 +0100 Subject: [PATCH] Check for unbounded variables in ModelGenerator2MTBDD. --- prism/src/prism/ModelGenerator2MTBDD.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/prism/src/prism/ModelGenerator2MTBDD.java b/prism/src/prism/ModelGenerator2MTBDD.java index bc7ff3b9..7b05f0eb 100644 --- a/prism/src/prism/ModelGenerator2MTBDD.java +++ b/prism/src/prism/ModelGenerator2MTBDD.java @@ -35,6 +35,9 @@ import jdd.JDDVars; import parser.State; import parser.Values; import parser.VarList; +import parser.ast.DeclarationClock; +import parser.ast.DeclarationIntUnbounded; +import parser.ast.DeclarationType; /** * Class to construct a symbolic representation from a ModelGenerator object. @@ -234,7 +237,7 @@ public class ModelGenerator2MTBDD * allocate DD vars for system * i.e. decide on variable ordering and request variables from CUDD */ - private void allocateDDVars() + private void allocateDDVars() throws PrismNotSupportedException { JDDNode vr, vc; int i, j, n; @@ -268,6 +271,10 @@ public class ModelGenerator2MTBDD // go through all vars in order (incl. global variables) // so overall ordering can be specified by ordering in the input file for (i = 0; i < numVars; i++) { + DeclarationType declType = varList.getDeclaration(i).getDeclType(); + if (declType instanceof DeclarationClock || declType instanceof DeclarationIntUnbounded) { + throw new PrismNotSupportedException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)"); + } // get number of dd variables needed // (ceiling of log2 of range of variable) n = varList.getRangeLogTwo(i);