Browse Source

PrismHybrid.java: Protect interval iteration JNI calls against large state spaces

The corresponding `checkNumStates(odd)` were missing.
accumulation-v4.7
Joachim Klein 7 years ago
committed by GitHub
parent
commit
d73591178b
No known key found for this signature in database GPG Key ID: 4AEE18F83AFDEB23
  1. 4
      prism/src/hybrid/PrismHybrid.java

4
prism/src/hybrid/PrismHybrid.java

@ -204,6 +204,8 @@ public class PrismHybrid
private static native long PH_ProbUntilInterval(long trans, long odd, long rv, int nrv, long cv, int ncv, long yes, long maybe, int flags);
public static DoubleVector ProbUntilInterval(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int flags) throws PrismException
{
checkNumStates(odd);
long ptr = PH_ProbUntilInterval(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), flags);
if (ptr == 0) throw generateExceptionForError();
return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
@ -246,6 +248,8 @@ public class PrismHybrid
private static native long PH_ProbReachRewardInterval(long trans, long sr, long trr, long odd, long rv, int nrv, long cv, int ncv, long goal, long inf, long maybe, long lower, long upper, int flags);
public static DoubleVector ProbReachRewardInterval(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal, JDDNode inf, JDDNode maybe, JDDNode lower, JDDNode upper, int flags) throws PrismException
{
checkNumStates(odd);
long ptr = PH_ProbReachRewardInterval(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr(), lower.ptr(), upper.ptr(), flags);
if (ptr == 0) throw generateExceptionForError();
return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));

Loading…
Cancel
Save