diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index 40aa0ba3..0c683ecd 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -109,12 +109,10 @@ public class DoubleVector */ public DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException { - long numStates = odd.getEOff() + odd.getTOff(); - if (numStates > Integer.MAX_VALUE) { - throw new PrismNotSupportedException("Can not create DoubleVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); - } + ODDUtils.checkInt(odd, "Can not create DoubleVector"); + v = DV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); - n = (int)numStates; + n = (int)odd.getNumStates(); } private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd); diff --git a/prism/src/dv/IntegerVector.java b/prism/src/dv/IntegerVector.java index 65246169..be1627b3 100644 --- a/prism/src/dv/IntegerVector.java +++ b/prism/src/dv/IntegerVector.java @@ -94,12 +94,10 @@ public class IntegerVector */ public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException { - long numStates = odd.getEOff() + odd.getTOff(); - if (numStates > Integer.MAX_VALUE) { - throw new PrismNotSupportedException("Can not create IntegerVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); - } + ODDUtils.checkInt(odd, "Can not create IntegerVector"); + v = IV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); - n = (int)numStates; + n = (int)odd.getNumStates(); } private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd); diff --git a/prism/src/hybrid/PrismHybrid.java b/prism/src/hybrid/PrismHybrid.java index bf52be94..b8f0d199 100644 --- a/prism/src/hybrid/PrismHybrid.java +++ b/prism/src/hybrid/PrismHybrid.java @@ -79,10 +79,7 @@ public class PrismHybrid { // currently, the hybrid engine internally uses int (signed 32bit) index values // so, if the number of states is larger than Integer.MAX_VALUE, there is a problem - long n = odd.getEOff() + odd.getTOff(); - if (n >= Integer.MAX_VALUE) { - throw new PrismNotSupportedException("The hybrid engine can currently only handle up to " + Integer.MAX_VALUE + " reachable states, model has " + n + " states"); - } + ODDUtils.checkInt(odd, "Currently, the hybrid engine cannot handle models"); } //------------------------------------------------------------------------------ diff --git a/prism/src/odd/ODDNode.java b/prism/src/odd/ODDNode.java index 67473fc4..0939f6ef 100644 --- a/prism/src/odd/ODDNode.java +++ b/prism/src/odd/ODDNode.java @@ -55,6 +55,17 @@ public class ODDNode return ODDUtils.ODD_GetEOff(ptr); } + /** + * Returns the number of states for this ODD node. + * Throws an arithmetic exception if the number of states + * does not fit in a Java long (should not occur as that is + * caught during ODD construction). + */ + public long getNumStates() + { + return Math.addExact(getTOff(), getEOff()); + } + public ODDNode getThen() { return new ODDNode(ODDUtils.ODD_GetThen(ptr)); diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java index 5fdbad7d..514da635 100644 --- a/prism/src/odd/ODDUtils.java +++ b/prism/src/odd/ODDUtils.java @@ -28,6 +28,7 @@ package odd; import jdd.*; import prism.PrismException; +import prism.PrismNotSupportedException; public class ODDUtils { @@ -121,7 +122,57 @@ public class ODDUtils { return JDD.ptrToNode(ODD_SingleIndexToDD(i, odd.ptr(), vars.array(), vars.n())); } - + + /** + * Checks that the given ODD has indices that can be represented by + * Java integers. If that is not the case, or the ODD is {@code null}, + * a PrismNotSupportedException is thrown. + * @param odd the ODD (may be {@code null}) + * @param msg Initial part of error message, will be extended with + * " with more than X states, have Y states" + */ + public static void checkInt(ODDNode odd, String msg) throws PrismNotSupportedException + { + if (odd != null) { + try { + long numStates = odd.getNumStates(); + if (numStates > Integer.MAX_VALUE) { + // number of states fit in long, but not in int + throw new PrismNotSupportedException(msg + " with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); + } else { + // everything is fine + return; + } + } catch (ArithmeticException e) { + // number of states does not fit into long, ignore here, handled below + } + } + + // we either have no ODD or eoff + toff does not fit into long + throw new PrismNotSupportedException(msg + " with more than " + Integer.MAX_VALUE + " states, have at least " + Long.MAX_VALUE + " states"); + } + + /** + * Returns true if the given ODD has indices that can be represented by + * Java integers. If the odd is {@code null}, returns false as well. + * @param odd the ODD (may be {@code null}) + */ + public static boolean hasIntValue(ODDNode odd) + { + if (odd == null) + return false; + + try { + long numStates = odd.getNumStates(); + if (numStates <= Integer.MAX_VALUE) { + return true; + } + } catch (ArithmeticException e) { + // number of states does not fit into long, ignore here, handled below + } + return false; + } + //------------------------------------------------------------------------------ // ODDNode methods //------------------------------------------------------------------------------ diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index aa38e161..3f909aa3 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -100,7 +100,7 @@ public interface Model String globalToLocal(long x); int globalToLocal(long x, int l); State convertBddToState(JDDNode dd); - int convertBddToIndex(JDDNode dd); + int convertBddToIndex(JDDNode dd) throws PrismNotSupportedException; StateList getReachableStates(); diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 6ba33322..0b5ddac5 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -1150,11 +1150,13 @@ public class ProbModel implements Model * Convert a BDD (over model row variables) representing a single state * to a (reachable) state index. */ - public int convertBddToIndex(JDDNode dd) + public int convertBddToIndex(JDDNode dd) throws PrismNotSupportedException { JDDNode ptr; ODDNode oddPtr; int i, n, index; + + ODDUtils.checkInt(odd, "Cannot convert Bdd to index in model"); // Traverse BDD and ODD simultaneously to compute index ptr = dd; oddPtr = odd; diff --git a/prism/src/prism/StateList.java b/prism/src/prism/StateList.java index 1fce06aa..58b3de64 100644 --- a/prism/src/prism/StateList.java +++ b/prism/src/prism/StateList.java @@ -71,7 +71,7 @@ public interface StateList /** * Print the states to a log, in Dot format. */ - void printDot(PrismLog log); + void printDot(PrismLog log) throws PrismException; /** * Format the list of states as a list of strings. @@ -99,7 +99,7 @@ public interface StateList * Get the index of a state in the list, specified as a State object. * Returns -1 if the state is not on the list or there is a problem with the lookup. */ - int getIndexOfState(State state); + int getIndexOfState(State state) throws PrismNotSupportedException; /** * Free any memory associated with storing this list of states. diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java index 33c43c2e..bf6e0770 100644 --- a/prism/src/prism/StateListMTBDD.java +++ b/prism/src/prism/StateListMTBDD.java @@ -188,11 +188,15 @@ public class StateListMTBDD implements StateList } @Override - public void printDot(PrismLog log) + public void printDot(PrismLog log) throws PrismException { outputFormat = OutputFormat.DOT; limit = false; outputLog = log; + + if (odd == null) { + throw new PrismNotSupportedException("Cannot export state list as DOT, too many states"); + } doPrint(); } @@ -245,9 +249,19 @@ public class StateListMTBDD implements StateList if (level == numVars) { switch (outputFormat) { - case NORMAL: outputLog.print(n + ":("); break; + case NORMAL: + if (o != null) { + outputLog.print(n + ":("); + } else { + // we have no index + outputLog.print("("); + } + break; case MATLAB: break; - case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break; + case DOT: + assert(o != null); // should not happen, missing ODD is caught before + outputLog.print(n + " [label=\"" + n + "\\n("); + break; case STRINGS: break; } j = varList.getNumVars(); @@ -282,14 +296,18 @@ public class StateListMTBDD implements StateList e = dd.getElse(); t = dd.getThen(); } - + + ODDNode oe = (o != null ? o.getElse() : null); + ODDNode ot = (o != null ? o.getThen() : null); + long eoff = (o != null ? o.getEOff() : 0); + // then recurse... currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } - printRec(e, level+1, o.getElse(), n); + printRec(e, level+1, oe, n); currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel)); currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } - printRec(t, level+1, o.getThen(), n+o.getEOff()); + printRec(t, level+1, ot, n + eoff); currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); } @@ -374,11 +392,14 @@ public class StateListMTBDD implements StateList } @Override - public int getIndexOfState(State state) + public int getIndexOfState(State state) throws PrismNotSupportedException { // Traverse BDD/ODD, top to bottom, computing index JDDNode ptr = states; ODDNode o = odd; + + ODDUtils.checkInt(odd, "Cannot get index of state in model"); + int level = 0; int index = 0; // Iterate through variables diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index f9ac59eb..b8b1e577 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1150,7 +1150,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // For some types of filter, store info that may be used to optimise model checking FilterOperator op = expr.getOperatorType(); - if (op == FilterOperator.STATE) { + if (op == FilterOperator.STATE && ODDUtils.hasIntValue(odd)) { // Check filter satisfied by exactly one state if (statesFilter.size() != 1) { String s = "Filter should be satisfied in exactly 1 state"; @@ -1158,9 +1158,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker throw new PrismException(s); } currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars)); - } else if (op == FilterOperator.FORALL && filterInit && filterInitSingle) { + } else if (op == FilterOperator.FORALL && filterInit && filterInitSingle && ODDUtils.hasIntValue(odd)) { currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars)); - } else if (op == FilterOperator.FIRST && filterInit && filterInitSingle) { + } else if (op == FilterOperator.FIRST && filterInit && filterInitSingle && ODDUtils.hasIntValue(odd)) { currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars)); } else { currentFilter = null; diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index d334e4b2..aba84ffb 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -167,7 +167,7 @@ public interface StateValues extends StateVector StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException; /** Returns an Object with the value of the i-th entry in this vector. */ - Object getValue(int i); + Object getValue(int i) throws PrismNotSupportedException; /** * Generate BDD for states in the given interval diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 65c58488..1b9baefe 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -134,12 +134,14 @@ public class StateValuesMTBDD implements StateValues /** * Set element i of this vector to value d. */ - public void setElement(int i, double d) + public void setElement(int i, double d) throws PrismNotSupportedException { ODDNode ptr; JDDNode dd; int j, k; - + + ODDUtils.checkInt(odd, "Cannot set element via index for model"); + // Use ODD to build BDD for state index i dd = JDD.Constant(1); ptr = odd; @@ -287,9 +289,12 @@ public class StateValuesMTBDD implements StateValues } @Override - public Object getValue(int i) + public Object getValue(int i) throws PrismNotSupportedException { JDDNode dd = values; + + ODDUtils.checkInt(odd, "Cannot get value for state index in model"); + ODDNode ptr = odd; int o = 0; for (int k = 0; k < numVars; k++) { @@ -653,7 +658,13 @@ public class StateValuesMTBDD implements StateValues // base case - at bottom (nonzero terminal) if (level == numVars) { - outputLog.print(n + ":("); + if (o != null) { + outputLog.print(n + ":("); + } else { + // we have no index + outputLog.print("("); + } + j = varList.getNumVars(); for (i = 0; i < j; i++) { // integer variable @@ -666,6 +677,7 @@ public class StateValuesMTBDD implements StateValues } if (i < j-1) outputLog.print(","); } + outputLog.print(")=" + dd.getValue()); outputLog.println(); return; @@ -680,13 +692,17 @@ public class StateValuesMTBDD implements StateValues t = dd.getThen(); } + ODDNode oe = (o != null ? o.getElse() : null); + ODDNode ot = (o != null ? o.getThen() : null); + long eoff = (o != null ? o.getEOff() : 0); + // then recurse... currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } - printRec(e, level+1, o.getElse(), n); + printRec(e, level+1, oe, n); currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel)); currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; } - printRec(t, level+1, o.getThen(), n+o.getEOff()); + printRec(t, level+1, ot, n + eoff); currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; } varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel)); } diff --git a/prism/src/prism/StateVector.java b/prism/src/prism/StateVector.java index 4fd212ba..b2da1826 100644 --- a/prism/src/prism/StateVector.java +++ b/prism/src/prism/StateVector.java @@ -39,7 +39,7 @@ public interface StateVector /** * Get the value of the ith element of the vector, as an Object. */ - public Object getValue(int i); + public Object getValue(int i) throws PrismNotSupportedException; /** * Clear the vector, i.e. free any used memory. diff --git a/prism/src/sparse/PrismSparse.java b/prism/src/sparse/PrismSparse.java index 95008a8a..b10d6f0b 100644 --- a/prism/src/sparse/PrismSparse.java +++ b/prism/src/sparse/PrismSparse.java @@ -33,6 +33,7 @@ import jdd.JDD; import jdd.JDDNode; import jdd.JDDVars; import odd.ODDNode; +import odd.ODDUtils; import prism.NativeIntArray; import prism.OpsAndBoundsList; import prism.PrismException; @@ -89,10 +90,7 @@ public class PrismSparse { // currently, the sparse engine internally uses int (signed 32bit) index values // so, if the number of states is larger than Integer.MAX_VALUE, there is a problem - long n = odd.getEOff() + odd.getTOff(); - if (n >= Integer.MAX_VALUE) { - throw new PrismNotSupportedException("The sparse engine can currently only handle up to " + Integer.MAX_VALUE + " reachable states, model has " + n + " states"); - } + ODDUtils.checkInt(odd, "Currently, the sparse engine cannot handle models"); } //----------------------------------------------------------------------------------------------