mtbdd/hybrid/sparse: Generate PrismNotSupportedExceptions if native error message contains 'not supported'

prism/src/hybrid/PrismHybrid.java

@@ -144,6 +144,22 @@ public class PrismHybrid
 		return PH_GetErrorMessage();
 	}
 
+	/**
+	 * Generate the proper exception for an error from the native layer.
+	 * Gets the error message and returns the corresponding exception,
+	 * i.e., if the message contains "not supported" then a PrismNotSupportedException
+	 * is returned, otherwise a plain PrismException.
+	 */
+	private static PrismException generateExceptionForError()
+	{
+		String msg = getErrorMessage();
+		if (msg.contains("not supported")) {
+			return new PrismNotSupportedException(msg);
+		} else {
+			return new PrismException(msg);
+		}
+	}
+
 	//------------------------------------------------------------------------------
 	// numerical computation detail queries
 	//------------------------------------------------------------------------------
@@ -169,7 +185,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -180,7 +196,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -189,7 +205,7 @@ public class PrismHybrid
 	public static DoubleVector ProbUntilInterval(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int flags) throws PrismException
 	{
 		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 new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -200,7 +216,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -211,7 +227,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -222,7 +238,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -231,7 +247,7 @@ public class PrismHybrid
 	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
 	{
 		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 new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -242,7 +258,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_ProbTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -257,7 +273,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_NondetBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), time, minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -268,7 +284,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_NondetUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -279,7 +295,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_NondetUntilInterval(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -290,7 +306,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_NondetReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -306,7 +322,7 @@ public class PrismHybrid
 
 		long mult = (multProbs == null) ? 0 : multProbs.getPtr();
 		long ptr = PH_StochBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), time, mult);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -317,7 +333,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_StochCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -328,7 +344,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_StochSteadyState(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -339,7 +355,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_StochTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -354,7 +370,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_Power(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -365,7 +381,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_PowerInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -376,7 +392,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_JOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums, omega);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -387,7 +403,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_JORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, row_sums, omega, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -398,7 +414,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_SOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums, omega, backwards);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -409,7 +425,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_SORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, row_sums, omega, backwards, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -420,7 +436,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_PSOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums, omega, backwards);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -431,7 +447,7 @@ public class PrismHybrid
 		checkNumStates(odd);
 
 		long ptr = PH_PSORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, row_sums, omega, backwards, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 

prism/src/mtbdd/PrismMTBDD.java

@@ -131,6 +131,22 @@ public class PrismMTBDD
 		return PM_GetErrorMessage();
 	}
 
+	/**
+	 * Generate the proper exception for an error from the native layer.
+	 * Gets the error message and returns the corresponding exception,
+	 * i.e., if the message contains "not supported" then a PrismNotSupportedException
+	 * is returned, otherwise a plain PrismException.
+	 */
+	private static PrismException generateExceptionForError()
+	{
+		String msg = getErrorMessage();
+		if (msg.contains("not supported")) {
+			return new PrismNotSupportedException(msg);
+		} else {
+			return new PrismException(msg);
+		}
+	}
+
 	//------------------------------------------------------------------------------
 	// JNI wrappers for blocks of mtbdd code
 	//------------------------------------------------------------------------------
@@ -384,7 +400,7 @@ public class PrismMTBDD
 	public static JDDNode ProbBoundedUntil(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int bound) throws PrismException
 	{
 		long ptr = PM_ProbBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 	
@@ -393,7 +409,7 @@ public class PrismMTBDD
 	public static JDDNode ProbUntil(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe) throws PrismException
 	{
 		long ptr = PM_ProbUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -402,7 +418,7 @@ public class PrismMTBDD
 	public static JDDNode ProbUntilInterval(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int flags) throws PrismException
 	{
 		long ptr = PM_ProbUntilInterval(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -411,7 +427,7 @@ public class PrismMTBDD
 	public static JDDNode ProbCumulReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, int bound) throws PrismException
 	{
 		long ptr = PM_ProbCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -420,7 +436,7 @@ public class PrismMTBDD
 	public static JDDNode ProbInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDVars rows, JDDVars cols, int time) throws PrismException
 	{
 		long ptr = PM_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -429,7 +445,7 @@ public class PrismMTBDD
 	public static JDDNode ProbReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode goal, JDDNode inf, JDDNode maybe) throws PrismException
 	{
 		long ptr = PM_ProbReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -438,7 +454,7 @@ public class PrismMTBDD
 	public static JDDNode 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
 	{
 		long ptr = PM_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 new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -447,7 +463,7 @@ public class PrismMTBDD
 	public static JDDNode ProbTransient(JDDNode trans, ODDNode odd, JDDNode init, JDDVars rows, JDDVars cols, int time) throws PrismException
 	{
 		long ptr = PM_ProbTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -460,7 +476,7 @@ public class PrismMTBDD
 	public static JDDNode NondetBoundedUntil(JDDNode trans, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, int bound, boolean minmax) throws PrismException
 	{
 		long ptr = PM_NondetBoundedUntil(trans.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), bound, minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 	
@@ -469,7 +485,7 @@ public class PrismMTBDD
 	public static JDDNode NondetUntil(JDDNode trans, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax) throws PrismException
 	{
 		long ptr = PM_NondetUntil(trans.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -478,7 +494,7 @@ public class PrismMTBDD
 	public static JDDNode NondetUntilInterval(JDDNode trans, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax, int flags) throws PrismException
 	{
 		long ptr = PM_NondetUntilInterval(trans.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -487,7 +503,7 @@ public class PrismMTBDD
 	public static JDDNode NondetInstReward(JDDNode trans, JDDNode sr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, int time, boolean minmax, JDDNode init) throws PrismException
 	{
 		long ptr = PM_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax, init.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -496,7 +512,7 @@ public class PrismMTBDD
 	public static JDDNode NondetReachReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, boolean minmax) throws PrismException
 	{
 		long ptr = PM_NondetReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -505,7 +521,7 @@ public class PrismMTBDD
 	public static JDDNode NondetReachRewardInterval(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDNode nondetMask, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, JDDNode lower, JDDNode upper, boolean minmax, int flags) throws PrismException
 	{
 		long ptr = PM_NondetReachRewardInterval(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), nondetMask.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), lower.ptr(), upper.ptr(), minmax, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -519,7 +535,7 @@ public class PrismMTBDD
 	{
 		long mult = (multProbs == null) ? 0 : multProbs.ptr();
 		long ptr = PM_StochBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), time, mult);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 	
@@ -528,7 +544,7 @@ public class PrismMTBDD
 	public static JDDNode StochCumulReward(JDDNode trans, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, double time) throws PrismException
 	{
 		long ptr = PM_StochCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 	
@@ -537,7 +553,7 @@ public class PrismMTBDD
 	public static JDDNode StochSteadyState(JDDNode trans, ODDNode odd, JDDNode init, JDDVars rows, JDDVars cols) throws PrismException
 	{
 		long ptr = PM_StochSteadyState(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 	
@@ -546,7 +562,7 @@ public class PrismMTBDD
 	public static JDDNode StochTransient(JDDNode trans, ODDNode odd, JDDNode init, JDDVars rows, JDDVars cols, double time) throws PrismException
 	{
 		long ptr = PM_StochTransient(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -596,7 +612,7 @@ public class PrismMTBDD
 	public static JDDNode Power(ODDNode odd, JDDVars rows, JDDVars cols, JDDNode a, JDDNode b, JDDNode init, boolean transpose) throws PrismException
 	{
 		long ptr = PM_Power(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -605,7 +621,7 @@ public class PrismMTBDD
 	public static JDDNode PowerInterval(ODDNode odd, JDDVars rows, JDDVars cols, JDDNode a, JDDNode b, JDDNode lower, JDDNode upper, boolean transpose, int flags) throws PrismException
 	{
 		long ptr = PM_PowerInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -614,7 +630,7 @@ public class PrismMTBDD
 	public static JDDNode JOR(ODDNode odd, JDDVars rows, JDDVars cols, JDDNode a, JDDNode b, JDDNode init, boolean transpose, double omega) throws PrismException
 	{
 		long ptr = PM_JOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, omega);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 
@@ -623,7 +639,7 @@ public class PrismMTBDD
 	public static JDDNode JORInterval(ODDNode odd, JDDVars rows, JDDVars cols, JDDNode a, JDDNode b, JDDNode lower, JDDNode upper, boolean transpose, double omega, int flags) throws PrismException
 	{
 		long ptr = PM_JORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, omega, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return JDD.ptrToNode(ptr);
 	}
 

prism/src/sparse/PrismSparse.java

@@ -154,6 +154,22 @@ public class PrismSparse
 		return PS_GetErrorMessage();
 	}
 
+	/**
+	 * Generate the proper exception for an error from the native layer.
+	 * Gets the error message and returns the corresponding exception,
+	 * i.e., if the message contains "not supported" then a PrismNotSupportedException
+	 * is returned, otherwise a plain PrismException.
+	 */
+	private static PrismException generateExceptionForError()
+	{
+		String msg = getErrorMessage();
+		if (msg.contains("not supported")) {
+			return new PrismNotSupportedException(msg);
+		} else {
+			return new PrismException(msg);
+		}
+	}
+
 	//----------------------------------------------------------------------------------------------
 	// JNI wrappers for blocks of sparse code
 	//----------------------------------------------------------------------------------------------
@@ -169,7 +185,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -180,7 +196,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -189,7 +205,7 @@ public class PrismSparse
 	public static DoubleVector ProbUntilInterval(JDDNode trans, ODDNode odd, JDDVars rows, JDDVars cols, JDDNode yes, JDDNode maybe, int flags) throws PrismException
 	{
 		long ptr = PS_ProbUntilInterval(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -200,7 +216,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), bound);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -211,7 +227,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -222,7 +238,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbReachReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), goal.ptr(), inf.ptr(), maybe.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -231,7 +247,7 @@ public class PrismSparse
 	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
 	{
 		long ptr = PS_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 new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -242,7 +258,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_ProbTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -257,7 +273,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_NondetBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), time, minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -268,7 +284,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_NondetUntil(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, (strat == null) ? 0 : strat.getPtr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -277,7 +293,7 @@ public class PrismSparse
 	public static DoubleVector NondetUntilInterval(JDDNode trans, JDDNode transActions, List<String> synchs, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode yes, JDDNode maybe, boolean minmax, IntegerVector strat, int flags) throws PrismException
 	{
 		long ptr = PS_NondetUntilInterval(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), yes.ptr(), maybe.ptr(), minmax, (strat == null) ? 0 : strat.getPtr(), flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -288,7 +304,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_NondetCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), bound, minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -299,7 +315,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_NondetInstReward(trans.ptr(), sr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), time, minmax, init.ptr());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -310,7 +326,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_NondetReachReward(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), minmax);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -319,7 +335,7 @@ public class PrismSparse
 	public static DoubleVector NondetReachRewardInterval(JDDNode trans, JDDNode transActions, List<String> synchs, JDDNode sr, JDDNode trr, ODDNode odd, JDDVars rows, JDDVars cols, JDDVars nondet, JDDNode goal, JDDNode inf, JDDNode maybe, JDDNode lower, JDDNode upper, boolean minmax, int flags) throws PrismException
 	{
 		long ptr = PS_NondetReachRewardInterval(trans.ptr(), (transActions == null) ? 0 : transActions.ptr(), synchs, sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), nondet.array(), nondet.n(), goal.ptr(), inf.ptr(), maybe.ptr(), lower.ptr(), upper.ptr(), minmax, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -523,7 +539,7 @@ public class PrismSparse
 
 		long mult = (multProbs == null) ? 0 : multProbs.getPtr();
 		long ptr = PS_StochBoundedUntil(trans.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), yes.ptr(), maybe.ptr(), time, mult);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -534,7 +550,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_StochCumulReward(trans.ptr(), sr.ptr(), trr.ptr(), odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -545,7 +561,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_StochSteadyState(trans.ptr(), odd.ptr(), init.ptr(), rows.array(), rows.n(), cols.array(), cols.n());
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 	
@@ -556,7 +572,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_StochTransient(trans.ptr(), odd.ptr(), init.getPtr(), rows.array(), rows.n(), cols.array(), cols.n(), time);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -620,7 +636,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_Power(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -631,7 +647,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_PowerInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -642,7 +658,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_JOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums, omega);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -653,7 +669,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_JORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, row_sums, omega, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -664,7 +680,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_SOR(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), init.ptr(), transpose, row_sums, omega, forwards);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}
 
@@ -675,7 +691,7 @@ public class PrismSparse
 		checkNumStates(odd);
 
 		long ptr = PS_SORInterval(odd.ptr(), rows.array(), rows.n(), cols.array(), cols.n(), a.ptr(), b.ptr(), lower.ptr(), upper.ptr(), transpose, row_sums, omega, forwards, flags);
-		if (ptr == 0) throw new PrismException(getErrorMessage());
+		if (ptr == 0) throw generateExceptionForError();
 		return new DoubleVector(ptr, (int)(odd.getEOff() + odd.getTOff()));
 	}