Make use of the new PrismNotSupportedException.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9999 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/Bisimulation.java

@@ -35,6 +35,7 @@ import java.util.Map;
 import parser.State;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Class to perform bisimulation minimisation for explicit-state models.
@@ -69,7 +70,7 @@ public class Bisimulation extends PrismComponent
 		case CTMC:
 			return minimiseCTMC((CTMC) model, propNames, propBSs);
 		default:
-			throw new PrismException("Bisimulation minimisation not yet supported for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Bisimulation minimisation not yet supported for " + model.getModelType() + "s");
 		}
 	}
 

prism/src/explicit/ConstructModel.java

@@ -43,6 +43,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismPrintStreamLog;
+import prism.PrismNotSupportedException;
 import prism.ProgressDisplay;
 import prism.UndefinedConstants;
 import simulator.SimulatorEngine;
@@ -175,7 +176,7 @@ public class ConstructModel extends PrismComponent
 			case STPG:
 			case SMG:
 			case PTA:
-				throw new PrismException("Model construction not supported for " + modelType + "s");
+				throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 			}
 		}
 
@@ -254,7 +255,7 @@ public class ConstructModel extends PrismComponent
 						case STPG:
 						case SMG:
 						case PTA:
-							throw new PrismException("Model construction not supported for " + modelType + "s");
+							throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 						}
 					}
 				}
@@ -331,7 +332,7 @@ public class ConstructModel extends PrismComponent
 			case STPG:
 			case SMG:
 			case PTA:
-				throw new PrismException("Model construction not supported for " + modelType + "s");
+				throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 			}
 			model.setStatesList(statesList);
 			model.setConstantValues(new Values(modulesFile.getConstantValues()));

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -36,6 +36,7 @@ import parser.State;
 import parser.Values;
 import prism.ModelType;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Simple explicit-state representation of a DTMC, constructed (implicitly) as the embedded DTMC of a CTMC.
@@ -72,7 +73,7 @@ public class DTMCEmbeddedSimple extends DTMCExplicit
 	@Override
 	public void buildFromPrismExplicit(String filename) throws PrismException
 	{
-		throw new PrismException("Not supported");
+		throw new PrismNotSupportedException("Not supported");
 	}
 	
 	// Accessors (for Model)

prism/src/explicit/DTMCFromMDPAndMDStrategy.java

@@ -34,6 +34,7 @@ import parser.State;
 import parser.Values;
 import prism.ModelType;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 import strat.MDStrategy;
 
 /**
@@ -61,7 +62,7 @@ public class DTMCFromMDPAndMDStrategy extends DTMCExplicit
 	@Override
 	public void buildFromPrismExplicit(String filename) throws PrismException
 	{
-		throw new PrismException("Not supported");
+		throw new PrismNotSupportedException("Not supported");
 	}
 
 	// Accessors (for Model)

prism/src/explicit/DTMCFromMDPMemorylessAdversary.java

@@ -34,6 +34,7 @@ import parser.State;
 import parser.Values;
 import prism.ModelType;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Explicit-state representation of a DTMC, constructed (implicitly)
@@ -60,7 +61,7 @@ public class DTMCFromMDPMemorylessAdversary extends DTMCExplicit
 	@Override
 	public void buildFromPrismExplicit(String filename) throws PrismException
 	{
-		throw new PrismException("Not supported");
+		throw new PrismNotSupportedException("Not supported");
 	}
 
 	// Accessors (for Model)

prism/src/explicit/DTMCModelChecker.java

@@ -37,6 +37,7 @@ import parser.ast.Expression;
 import parser.type.TypeDouble;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 import prism.PrismUtils;
 import explicit.rewards.MCRewards;
 
@@ -239,7 +240,7 @@ public class DTMCModelChecker extends ProbModelChecker
 	 */
 	public StateValues doTransient(DTMC dtmc, int k, double initDist[]) throws PrismException
 	{
-		throw new PrismException("Not implemented yet");
+		throw new PrismNotSupportedException("Not implemented yet");
 	}
 
 	// Utility methods for probability distributions
@@ -1330,7 +1331,7 @@ public class DTMCModelChecker extends ProbModelChecker
 	 */
 	public ModelCheckerResult computeTransientProbs(DTMC dtmc, int k, double initDist[]) throws PrismException
 	{
-		throw new PrismException("Not implemented yet");
+		throw new PrismNotSupportedException("Not implemented yet");
 	}
 
 	/**

prism/src/explicit/DTMCUniformisedSimple.java

@@ -36,6 +36,7 @@ import parser.State;
 import parser.Values;
 import prism.ModelType;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 import explicit.rewards.MCRewards;
 
 /**
@@ -78,7 +79,7 @@ public class DTMCUniformisedSimple extends DTMCExplicit
 	@Override
 	public void buildFromPrismExplicit(String filename) throws PrismException
 	{
-		throw new PrismException("Not supported");
+		throw new PrismNotSupportedException("Not supported");
 	}
 	
 	// Accessors (for Model)

prism/src/explicit/FastAdaptiveUniformisationModelChecker.java

@@ -38,6 +38,7 @@ import parser.ast.PropertiesFile;
 import parser.ast.RewardStruct;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 import prism.Result;
 import simulator.PrismModelExplorer;
 import simulator.SimulatorEngine;
@@ -122,7 +123,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 		else if (expr instanceof ExpressionReward)
 			res = checkExpressionReward((ExpressionReward) expr);
 		else
-			throw new PrismException("Fast adaptive uniformisation not yet supported for this operator");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation not yet supported for this operator");
 
 		return res;
 	}
@@ -134,15 +135,15 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 	{
 		// Check whether P=? (only case allowed)
 		if (expr.getProb() != null) {
-			throw new PrismException("Fast adaptive uniformisation model checking currently only supports P=? properties");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation model checking currently only supports P=? properties");
 		}
 
 		if (!(expr.getExpression() instanceof ExpressionTemporal)) {
-			throw new PrismException("Fast adaptive uniformisation model checking currently only supports simple path operators");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation model checking currently only supports simple path operators");
 		}
 		ExpressionTemporal exprTemp = (ExpressionTemporal) expr.getExpression();
 		if (!exprTemp.isSimplePathFormula()) {
-			throw new PrismException("Fast adaptive uniformisation window model checking currently only supports simple until operators");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently only supports simple until operators");
 		}
 
 		double timeLower = 0.0;
@@ -150,12 +151,12 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 			timeLower = exprTemp.getLowerBound().evaluateDouble(constantValues);
 		}
 		if (exprTemp.getUpperBound() == null) {
-			throw new PrismException("Fast adaptive uniformisation window model checking currently requires an upper time bound");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently requires an upper time bound");
 		}
 		double timeUpper = exprTemp.getUpperBound().evaluateDouble(constantValues);
 
 		if (!exprTemp.hasBounds()) {
-			throw new PrismException("Fast adaptive uniformisation window model checking currently only supports timed properties");
+			throw new PrismNotSupportedException("Fast adaptive uniformisation window model checking currently only supports timed properties");
 		}
 
 		mainLog.println("Starting transient probability computation using fast adaptive uniformisation...");
@@ -187,7 +188,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 		case ExpressionTemporal.P_W:
 		case ExpressionTemporal.P_R:
 		default:
-			throw new PrismException("operator currently not supported for fast adaptive uniformisation");
+			throw new PrismNotSupportedException("operator currently not supported for fast adaptive uniformisation");
 		}
 		fau.setSink(sink);
 		fau.computeTransientProbsAdaptive(timeLower);
@@ -206,7 +207,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 		case ExpressionTemporal.P_W:
 		case ExpressionTemporal.P_R:
 		default:
-			throw new PrismException("operator currently not supported for fast adaptive uniformisation");
+			throw new PrismNotSupportedException("operator currently not supported for fast adaptive uniformisation");
 		}
 		Values varValues = new Values();
 		varValues.addValue("deadlock", "true");
@@ -238,7 +239,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 			fau.setAnalysisType(FastAdaptiveUniformisation.AnalysisType.REW_CUMUL);
 			break;
 		default:
-			throw new PrismException("Currently only instantaneous or cumulative rewards are allowed.");
+			throw new PrismNotSupportedException("Currently only instantaneous or cumulative rewards are allowed.");
 		}
 		double time = temporal.getUpperBound().evaluateDouble(constantValues);
 		RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues);

prism/src/explicit/LTLModelChecker.java

@@ -53,10 +53,10 @@ import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLangException;
 import prism.PrismLog;
+import prism.PrismNotSupportedException;
 import acceptance.AcceptanceOmega;
 import acceptance.AcceptanceRabin;
 import acceptance.AcceptanceType;
-
 import common.IterableStateSet;
 
 /**
@@ -218,7 +218,7 @@ public class LTLModelChecker extends PrismComponent
 				// formulas only appear positively
 				expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
 			} else {
-				throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
+				throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr);
 			}
 		}
 
@@ -577,7 +577,7 @@ public class LTLModelChecker extends PrismComponent
 		if (acceptance instanceof AcceptanceRabin) {
 			return findAcceptingECStatesForRabin(model, (AcceptanceRabin) acceptance);
 		}
-		throw new PrismException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine).");
+		throw new PrismNotSupportedException("Computing end components for acceptance type '"+acceptance.getTypeName()+"' currently not supported (explicit engine).");
 	}
 
 	/**

prism/src/explicit/NonProbModelChecker.java

@@ -33,6 +33,7 @@ import parser.ast.ExpressionExists;
 import parser.ast.ExpressionForAll;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Explicit-state, non-probabilistic model checker.
@@ -54,11 +55,11 @@ public class NonProbModelChecker extends StateModelChecker
 
 		// E operator
 		if (expr instanceof ExpressionExists) {
-			throw new PrismException("CTL model checking is not yet supported by the explicit engine");
+			throw new PrismNotSupportedException("CTL model checking is not yet supported by the explicit engine");
 		}
 		// A operator
 		else if (expr instanceof ExpressionForAll) {
-			throw new PrismException("CTL model checking is not yet supported by the explicit engine");
+			throw new PrismNotSupportedException("CTL model checking is not yet supported by the explicit engine");
 		}
 		// Otherwise, use the superclass
 		else {

prism/src/explicit/PrismExplicit.java

@@ -61,7 +61,7 @@ public class PrismExplicit extends PrismComponent
 		ConstructModel constructModel;
 
 		if (modulesFile.getModelType() == ModelType.PTA) {
-			throw new PrismException("You cannot build a PTA model explicitly, only perform model checking");
+			throw new PrismNotSupportedException("You cannot build a PTA model explicitly, only perform model checking");
 		}
 
 		mainLog.print("\nBuilding model...\n");
@@ -123,7 +123,7 @@ public class PrismExplicit extends PrismComponent
 		case Prism.EXPORT_MRMC:
 		case Prism.EXPORT_ROWS:
 		case Prism.EXPORT_DOT_STATES:
-			throw new PrismException("Export not yet supported"); // TODO
+			throw new PrismNotSupportedException("Export not yet supported"); // TODO
 		}
 	}
 
@@ -248,7 +248,7 @@ public class PrismExplicit extends PrismComponent
 		PrismLog tmpLog;
 		
 		if (!(model.getModelType() == ModelType.CTMC || model.getModelType() == ModelType.DTMC))
-			throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
+			throw new PrismNotSupportedException("Steady-state probabilities only computed for DTMCs/CTMCs");
 		
 		// no specific states format for MRMC
 		if (exportType == Prism.EXPORT_MRMC) exportType = Prism.EXPORT_PLAIN;
@@ -301,10 +301,10 @@ public class PrismExplicit extends PrismComponent
 			probs = mcDTMC.doSteadyState((DTMC) model);
 		}
 		else if (model.getModelType() == ModelType.CTMC) {
-			throw new PrismException("Not implemented yet"); // TODO
+			throw new PrismNotSupportedException("Not implemented yet"); // TODO
 		}
 		else {
-			throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
+			throw new PrismNotSupportedException("Steady-state probabilities only computed for DTMCs/CTMCs");
 		}
 		return probs;
 	}
@@ -340,7 +340,7 @@ public class PrismExplicit extends PrismComponent
 		l = System.currentTimeMillis();
 
 		if (model.getModelType() == ModelType.DTMC) {
-			throw new PrismException("Not implemented yet"); // TODO
+			throw new PrismNotSupportedException("Not implemented yet"); // TODO
 		}
 		else if (model.getModelType() == ModelType.CTMC) {
 			mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
@@ -348,7 +348,7 @@ public class PrismExplicit extends PrismComponent
 			probs = mcCTMC.doTransient((CTMC) model, time, fileIn);
 		}
 		else {
-			throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs");
+			throw new PrismNotSupportedException("Transient probabilities only computed for DTMCs/CTMCs");
 		}
 		
 		l = System.currentTimeMillis() - l;

prism/src/explicit/PrismSTPGAbstractRefine.java

@@ -31,6 +31,7 @@ import java.util.*;
 import prism.ModelType;
 import prism.PrismComponent;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 {
@@ -91,7 +92,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			modelConcrete = new MDPSimple();
 			break;
 		default:
-			throw new PrismException("Cannot handle model type " + modelType);
+			throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 		}
 		modelConcrete.buildFromPrismExplicit(traFile);
 		if (buildEmbeddedDtmc) {
@@ -162,7 +163,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 			abstraction = new STPGAbstrSimple(nAbstract);
 			break;
 		default:
-			throw new PrismException("Cannot handle model type " + modelType);
+			throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 		}
 		abstraction.addInitialState(0);
 		if (existsTargetAndInitial)
@@ -195,7 +196,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 				j = ((STPGAbstrSimple) abstraction).addDistributionSet(a, set);
 				break;
 			default:
-				throw new PrismException("Cannot handle model type " + modelType);
+				throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 			}
 			list = abstractToConcrete.get(a);
 			if (j >= list.size())
@@ -350,7 +351,7 @@ public class PrismSTPGAbstractRefine extends QuantAbstractRefine
 					j = ((STPGAbstrSimple) abstraction).addDistributionSet(a, set);
 					break;
 				default:
-					throw new PrismException("Cannot handle model type " + modelType);
+					throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 				}
 				if (j >= listNew.size())
 					listNew.add(new HashSet<Integer>(1));

prism/src/explicit/ProbModelChecker.java

@@ -43,6 +43,7 @@ import prism.OpRelOpBound;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismSettings;
+import prism.PrismNotSupportedException;
 import explicit.rewards.ConstructRewards;
 import explicit.rewards.MCRewards;
 import explicit.rewards.MDPRewards;
@@ -173,7 +174,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			} else if (s.equals("Backwards SOR")) {
 				setLinEqMethod(LinEqMethod.BACKWARDS_SOR);
 			} else {
-				throw new PrismException("Explicit engine does not support linear equation solution method \"" + s + "\"");
+				throw new PrismNotSupportedException("Explicit engine does not support linear equation solution method \"" + s + "\"");
 			}
 			// PRISM_MDP_SOLN_METHOD
 			s = settings.getString(PrismSettings.PRISM_MDP_SOLN_METHOD);
@@ -188,7 +189,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			} else if (s.equals("Linear programming")) {
 				setMDPSolnMethod(MDPSolnMethod.LINEAR_PROGRAMMING);
 			} else {
-				throw new PrismException("Explicit engine does not support MDP solution method \"" + s + "\"");
+				throw new PrismNotSupportedException("Explicit engine does not support MDP solution method \"" + s + "\"");
 			}
 			// PRISM_TERM_CRIT
 			s = settings.getString(PrismSettings.PRISM_TERM_CRIT);
@@ -197,7 +198,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			} else if (s.equals("Relative")) {
 				setTermCrit(TermCrit.RELATIVE);
 			} else {
-				throw new PrismException("Unknown termination criterion \"" + s + "\"");
+				throw new PrismNotSupportedException("Unknown termination criterion \"" + s + "\"");
 			}
 			// PRISM_TERM_CRIT_PARAM
 			setTermCritParam(settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM));
@@ -211,7 +212,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			setProb1(settings.getBoolean(PrismSettings.PRISM_PROB1));
 			// PRISM_FAIRNESS
 			if (settings.getBoolean(PrismSettings.PRISM_FAIRNESS)) {
-				throw new PrismException("The explicit engine does not support model checking MDPs under fairness");
+				throw new PrismNotSupportedException("The explicit engine does not support model checking MDPs under fairness");
 			}
 
 			// PRISM_EXPORT_ADV
@@ -477,11 +478,11 @@ public class ProbModelChecker extends NonProbModelChecker
 	{
 		// Only support <<>> right now, not [[]]
 		if (!expr.isThereExists())
-			throw new PrismException("The " + expr.getOperatorString() + " operator is not yet supported");
+			throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is not yet supported");
 
 		// Only support <<>> for MDPs right now
 		if (!(this instanceof MDPModelChecker))
-			throw new PrismException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently");
+			throw new PrismNotSupportedException("The " + expr.getOperatorString() + " operator is only supported for MDPs currently");
 
 		// Extract coalition info
 		Coalition coalition = expr.getCoalition();
@@ -646,7 +647,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((STPGModelChecker) this).computeNextProbs((STPG) model, target, minMax.isMin1(), minMax.isMin2());
 			break;
 		default:
-			throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Cannot model check " + expr + " for " + model.getModelType() + "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}
@@ -723,7 +724,7 @@ public class ProbModelChecker extends NonProbModelChecker
 				res = ((STPGModelChecker) this).computeBoundedUntilProbs((STPG) model, remain, target, windowSize, minMax.isMin1(), minMax.isMin2());
 				break;
 			default:
-				throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
+				throw new PrismNotSupportedException("Cannot model check " + expr + " for " + model.getModelType() + "s");
 			}
 			sv = StateValues.createFromDoubleArray(res.soln, model);
 		}
@@ -743,9 +744,9 @@ public class ProbModelChecker extends NonProbModelChecker
 					break;
 				case STPG:
 					// TODO (JK): Figure out if we can handle lower bounds for STPG in the same way
-					throw new PrismException("Lower bounds not yet supported for STPGModelChecker");
+					throw new PrismNotSupportedException("Lower bounds not yet supported for STPGModelChecker");
 				default:
-					throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
+					throw new PrismNotSupportedException("Cannot model check " + expr + " for " + model.getModelType() + "s");
 				}
 			}
 
@@ -781,7 +782,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((STPGModelChecker) this).computeUntilProbs((STPG) model, remain, target, minMax.isMin1(), minMax.isMin2());
 			break;
 		default:
-			throw new PrismException("Cannot model check " + expr + " for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Cannot model check " + expr + " for " + model.getModelType() + "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}
@@ -792,7 +793,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
 		// To be overridden by subclasses
-		throw new PrismException("Computation not implemented yet");
+		throw new PrismNotSupportedException("Computation not implemented yet");
 	}
 
 	/**
@@ -854,7 +855,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues);
 			break;
 		default:
-			throw new PrismException("Cannot build rewards for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Cannot build rewards for " + model.getModelType() + "s");
 		}
 		return rewards;
 	}
@@ -879,7 +880,7 @@ public class ProbModelChecker extends NonProbModelChecker
 				rewards = checkRewardCumulative(model, modelRewards, exprTemp, minMax);
 				break;
 			default:
-				throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator");
+				throw new PrismNotSupportedException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator");
 			}
 		}
 
@@ -914,7 +915,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((STPGModelChecker) this).computeReachRewards((STPG) model, (STPGRewards) modelRewards, target, minMax.isMin1(), minMax.isMin2());
 			break;
 		default:
-			throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
+			throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
 					+ "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
@@ -938,7 +939,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((CTMCModelChecker) this).computeInstantaneousRewards((CTMC) model, (MCRewards) modelRewards, t);
 			break;
 		default:
-			throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
+			throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
 					+ "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
@@ -954,7 +955,7 @@ public class ProbModelChecker extends NonProbModelChecker
 
 		// Check that there is an upper time bound
 		if (expr.getUpperBound() == null) {
-			throw new PrismException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
+			throw new PrismNotSupportedException("Cumulative reward operator without time bound (C) is only allowed for multi-objective queries");
 		}
 
 		// Get time bound
@@ -989,7 +990,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			result.setStrategy(res.strat);
 			break;
 		default:
-			throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
+			throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
 					+ "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
@@ -1041,7 +1042,7 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((DTMCModelChecker) this).computeSteadyStateBackwardsProbs((DTMC) model, multProbs);
 			break;
 		default:
-			throw new PrismException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Explicit engine does not yet handle the S operator for " + model.getModelType() + "s");
 		}
 		return StateValues.createFromDoubleArray(res.soln, model);
 	}

prism/src/explicit/Product.java

@@ -33,6 +33,7 @@ import parser.type.TypeBool;
 import parser.type.TypeDouble;
 import parser.type.TypeInt;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 /**
  * Base class for the results of a product operation between a model and
@@ -168,7 +169,7 @@ public abstract class Product<M extends Model> implements ModelTransformation<M,
 			} else if (sv.type instanceof TypeDouble) {
 				result.setDoubleValue(modelState, (Double) sv.getValue(productState));
 			} else {
-				throw new PrismException("Handling for type "+sv.type+" not implemented.");
+				throw new PrismNotSupportedException("Handling for type "+sv.type+" not implemented.");
 			}
 		}
 

prism/src/explicit/QuantAbstractRefine.java

@@ -277,7 +277,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			try {
 				setVerbosity((optVal == null) ? 10 : Integer.parseInt(optVal));
 			} catch (NumberFormatException e) {
-				throw new PrismException("Invalid value \"" + optVal + "\" for abstraction-refinement setting \"" + opt + "\"");
+				throw new PrismNotSupportedException("Invalid value \"" + optVal + "\" for abstraction-refinement setting \"" + opt + "\"");
 			}
 		} else if (opt.matches("refine")) {
 			if (optVal != null) {
@@ -471,7 +471,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			mc = new STPGModelChecker(null);
 			break;
 		default:
-			throw new PrismException("Cannot handle model type " + modelType);
+			throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 		}
 		mc.inheritSettings(mcOptions);
 		// But limit verbosity (since model checking will be done many times)
@@ -627,7 +627,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			modelCheckAbstractionExpReach(min);
 			break;
 		default:
-			throw new PrismException("Property type " + propertyType + " not supported");
+			throw new PrismNotSupportedException("Property type " + propertyType + " not supported");
 		}
 
 		// See if each state has "converged", i.e. bounds are close enough to assume exact
@@ -702,7 +702,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			}
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		lbSoln = res.soln;
 		lbLastSoln = lbSoln; // TODO: fix (if nec.)
@@ -743,7 +743,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			}
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		ubSoln = res.soln;
 		ubLastSoln = ubSoln; // TODO: fix (if nec.)
@@ -776,7 +776,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 					results);
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		lbSoln = res.soln;
 		lbLastSoln = res.lastSoln;
@@ -804,7 +804,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 					results);
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		ubSoln = res.soln;
 		ubLastSoln = res.lastSoln;
@@ -841,7 +841,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			}
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		lbSoln = res.soln;
 		lbLastSoln = lbSoln; // TODO: fix (if nec.)
@@ -861,7 +861,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 			}
 			break;
 		default:
-			throw new PrismException("Cannot model check " + abstractionType);
+			throw new PrismNotSupportedException("Cannot model check " + abstractionType);
 		}
 		ubSoln = res.soln;
 		ubLastSoln = ubSoln; // TODO: fix (if nec.)
@@ -1262,7 +1262,7 @@ public abstract class QuantAbstractRefine extends PrismComponent
 		} else if (abstraction instanceof MDPSimple) {
 			stpg = new STPGAbstrSimple((MDPSimple) abstraction);
 		} else {
-			throw new PrismException("Cannot export this model type to a dot file");
+			throw new PrismNotSupportedException("Cannot export this model type to a dot file");
 		}
 
 		try {

prism/src/explicit/QuantAbstractRefineExample.java

@@ -38,6 +38,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismPrintStreamLog;
+import prism.PrismNotSupportedException;
 import prism.UndefinedConstants;
 
 public class QuantAbstractRefineExample extends QuantAbstractRefine
@@ -288,7 +289,7 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine
 					j = ((STPGAbstrSimple) abstraction).addDistributionSet(a, set);
 					break;
 				default:
-					throw new PrismException("Cannot handle model type " + modelType);
+					throw new PrismNotSupportedException("Cannot handle model type " + modelType);
 				}
 				if (j >= listNew.size())
 					listNew.add(new HashSet<Integer>(1));

prism/src/explicit/STPGAbstrSimple.java

@@ -36,6 +36,7 @@ import common.IterableStateSet;
 import explicit.rewards.STPGRewards;
 import prism.ModelType;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 import prism.PrismLog;
 import prism.PrismUtils;
 import strat.MDStrategy;
@@ -428,7 +429,7 @@ public class STPGAbstrSimple extends ModelExplicit implements STPG, NondetModelS
 	@Override
 	public void exportToPrismLanguage(String filename) throws PrismException
 	{
-		throw new PrismException("Export to STPG PRISM models not supported");
+		throw new PrismNotSupportedException("Export to STPG PRISM models not supported");
 	}
 
 	@Override

prism/src/explicit/STPGModelChecker.java

@@ -36,6 +36,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLog;
+import prism.PrismNotSupportedException;
 import prism.PrismUtils;
 import explicit.rewards.STPGRewards;
 
@@ -57,7 +58,7 @@ public class STPGModelChecker extends ProbModelChecker
 	@Override
 	protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
-		throw new PrismException("LTL model checking not yet supported for stochastic games");
+		throw new PrismNotSupportedException("LTL model checking not yet supported for stochastic games");
 	}
 	
 	// Numerical computation functions

prism/src/explicit/StateModelChecker.java

@@ -66,6 +66,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismSettings;
+import prism.PrismNotSupportedException;
 import prism.Result;
 
 /**
@@ -405,7 +406,7 @@ public class StateModelChecker extends PrismComponent
 		}
 		// Anything else - error
 		else {
-			throw new PrismException("Couldn't check " + expr.getClass());
+			throw new PrismNotSupportedException("Couldn't check " + expr.getClass());
 		}
 
 		return res;
@@ -506,7 +507,7 @@ public class StateModelChecker extends PrismComponent
 		case ExpressionFunc.LOG:
 			return checkExpressionFuncBinary(model, expr, statesOfInterest);
 		case ExpressionFunc.MULTI:
-			throw new PrismException("Multi-objective model checking is not supported for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Multi-objective model checking is not supported for " + model.getModelType() + "s");
 		default:
 			throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
 		}

prism/src/explicit/rewards/ConstructRewards.java

@@ -41,6 +41,7 @@ import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLangException;
 import prism.PrismLog;
+import prism.PrismNotSupportedException;
 import explicit.DTMC;
 import explicit.MDP;
 import explicit.Model;
@@ -74,7 +75,7 @@ public class ConstructRewards
 		case MDP:
 			return buildMDPRewardStructure((MDP) model, rewStr, constantValues);
 		default:
-			throw new PrismException("Cannot build rewards for " + model.getModelType() + "s");
+			throw new PrismNotSupportedException("Cannot build rewards for " + model.getModelType() + "s");
 		}
 	}
 
@@ -92,7 +93,7 @@ public class ConstructRewards
 
 		if (rewStr.getNumTransItems() > 0) {
 			// TODO
-			throw new PrismException("Explicit engine does not yet handle transition rewards for D/CTMCs");
+			throw new PrismNotSupportedException("Explicit engine does not yet handle transition rewards for D/CTMCs");
 		}
 		// Special case: constant rewards
 		if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
@@ -231,7 +232,7 @@ public class ConstructRewards
 		}
 
 		if (rewt != null) {
-			throw new PrismException("Explicit engine does not yet handle transition rewards for D/CTMCs");
+			throw new PrismNotSupportedException("Explicit engine does not yet handle transition rewards for D/CTMCs");
 		}
 
 		return rewSA;

prism/src/param/ModelBuilder.java

@@ -44,6 +44,7 @@ import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismLangException;
 import prism.PrismSettings;
+import prism.PrismNotSupportedException;
 import explicit.IndexedSet;
 import explicit.StateStorage;
 
@@ -135,7 +136,7 @@ public final class ModelBuilder extends PrismComponent
 			case ExpressionBinaryOp.DIVIDE:
 				return f1.divide(f2);
 			default:
-				throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
+				throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
 			}
 		} else if (expr instanceof ExpressionUnaryOp) {
 			ExpressionUnaryOp unExpr = ((ExpressionUnaryOp) expr);
@@ -146,10 +147,10 @@ public final class ModelBuilder extends PrismComponent
 			case ExpressionUnaryOp.PARENTH:
 				return f;
 			default:
-				throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
+				throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
 			}
 		} else {
-			throw new PrismException("parametric analysis with rate/probability of " + expr + " not implemented");
+			throw new PrismNotSupportedException("parametric analysis with rate/probability of " + expr + " not implemented");
 		}
 	}
 
@@ -205,7 +206,7 @@ public final class ModelBuilder extends PrismComponent
 		long time;
 
 		if (modulesFile.getModelType() == ModelType.PTA) {
-			throw new PrismException("You cannot build a PTA model explicitly, only perform model checking");
+			throw new PrismNotSupportedException("You cannot build a PTA model explicitly, only perform model checking");
 		}
 
 		mainLog.print("\nBuilding model...\n");
@@ -314,7 +315,7 @@ public final class ModelBuilder extends PrismComponent
 		ModelType modelType;
 
 		if (modulesFile.getInitialStates() != null) {
-			throw new PrismException("Cannot do explicit-state reachability if there are multiple initial states");
+			throw new PrismNotSupportedException("Cannot do explicit-state reachability if there are multiple initial states");
 		}
 
 		mainLog.print("\nComputing reachable states...");
@@ -324,12 +325,12 @@ public final class ModelBuilder extends PrismComponent
 		ParamModel model = new ParamModel();
 		model.setModelType(modelType);
 		if (modelType != ModelType.DTMC && modelType != ModelType.CTMC && modelType != ModelType.MDP) {
-			throw new PrismException("Unsupported model type: " + modelType);
+			throw new PrismNotSupportedException("Unsupported model type: " + modelType);
 		}
 		SymbolicEngine engine = new SymbolicEngine(modulesFile);
 
 		if (modulesFile.getInitialStates() != null) {
-			throw new PrismException("Explicit model construction does not support multiple initial states");
+			throw new PrismNotSupportedException("Explicit model construction does not support multiple initial states");
 		}
 
 		boolean isNonDet = modelType == ModelType.MDP;

prism/src/param/ParamModelChecker.java

@@ -89,6 +89,7 @@ import prism.PrismException;
 import prism.PrismLog;
 import prism.PrismPrintStreamLog;
 import prism.PrismSettings;
+import prism.PrismNotSupportedException;
 import prism.Result;
 import edu.jas.kern.ComputerThreads;
 import explicit.Model;
@@ -314,7 +315,7 @@ final public class ParamModelChecker extends PrismComponent
 			regionOp = Region.DIVIDE;
 			break;
 		default:
-			throw new PrismException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp]
+			throw new PrismNotSupportedException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp]
 					+ "\" not currently supported for parametric analyses");				
 		}
 		return regionOp;
@@ -334,7 +335,7 @@ final public class ParamModelChecker extends PrismComponent
 			regionOp = Region.PARENTH;
 			break;
 		default:
-			throw new PrismException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp]
+			throw new PrismNotSupportedException("operator \"" + ExpressionBinaryOp.opSymbols[parserOp]
 					+ "\" not currently supported for parametric analyses");				
 		}
 		return regionOp;
@@ -399,13 +400,13 @@ final public class ParamModelChecker extends PrismComponent
 						BigRational exprRat = new BigRational(exprStr);
 						stateValues.setStateValue(state, functionFactory.fromBigRational(exprRat));
 					} else {
-						throw new PrismException("model checking expresssion " + expr + " not supported for parametric models");
+						throw new PrismNotSupportedException("model checking expresssion " + expr + " not supported for parametric models");
 					}
 				} else if (exprVar instanceof ExpressionConstant) {
 					ExpressionConstant exprConst = (ExpressionConstant) exprVar;
 					stateValues.setStateValue(state, functionFactory.getVar(exprConst.getName()));
 				} else {
-					throw new PrismException("cannot handle expression " + expr + " in parametric analysis");
+					throw new PrismNotSupportedException("cannot handle expression " + expr + " in parametric analysis");
 				}
 			} else {
 				if (exprVar.getType() instanceof TypeBool) {
@@ -538,7 +539,7 @@ final public class ParamModelChecker extends PrismComponent
 		case MAX:
 		case ARGMIN:
 		case ARGMAX:
-			throw new PrismException("operation not implemented for parametric models");
+			throw new PrismNotSupportedException("operation not implemented for parametric models");
 		case COUNT:
 			resVals = vals.op(Region.COUNT, bsFilter);
 			break;
@@ -555,7 +556,7 @@ final public class ParamModelChecker extends PrismComponent
 			resVals = vals.op(Region.FIRST, bsFilter);
 			break;
 		case RANGE:
-			throw new PrismException("operation not implemented for parametric models");
+			throw new PrismNotSupportedException("operation not implemented for parametric models");
 		case FORALL:
 			resVals = vals.op(Region.FORALL, bsFilter);
 			break;
@@ -870,7 +871,7 @@ final public class ParamModelChecker extends PrismComponent
 
 		// Compute probabilities
 		if (!expr.getExpression().isSimplePathFormula()) {
-			throw new PrismException("Parametric engine does not yet handle LTL-style path formulas");
+			throw new PrismNotSupportedException("Parametric engine does not yet handle LTL-style path formulas");
 		}
 		probs = checkProbPathFormulaSimple(model, expr.getExpression(), min, needStates);
 		probs.clearNotNeeded(needStates);
@@ -923,7 +924,7 @@ final public class ParamModelChecker extends PrismComponent
 		RegionValues probs;
 		switch (modelType) {
 		case CTMC:
-			throw new PrismException("bounded until not implemented for parametric CTMCs");
+			throw new PrismNotSupportedException("bounded until not implemented for parametric CTMCs");
 		case DTMC:
 			probs = checkProbBoundedUntilDTMC(model, b1, b2);
 			break;
@@ -931,7 +932,7 @@ final public class ParamModelChecker extends PrismComponent
 			probs = checkProbBoundedUntilMDP(model, b1, b2, min);
 			break;
 		default:
-			throw new PrismException("Cannot model check for a " + modelType);
+			throw new PrismNotSupportedException("Cannot model check for a " + modelType);
 		}
 
 		return probs;
@@ -1002,7 +1003,7 @@ final public class ParamModelChecker extends PrismComponent
 				rewards = checkRewardSteady(model, rew, exprTemp, min, needStates);				
 				break;
 			default:
-				throw new PrismException("Parametric engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
+				throw new PrismNotSupportedException("Parametric engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
 			}
 		}
 		
@@ -1025,7 +1026,7 @@ final public class ParamModelChecker extends PrismComponent
 	private RegionValues checkRewardSteady(ParamModel model,
 			ParamRewardStruct rew, ExpressionTemporal expr, boolean min, BitSet needStates) throws PrismException {
 		if (model.getModelType() != ModelType.DTMC && model.getModelType() != ModelType.CTMC) {
-			throw new PrismException("Parametric long-run average rewards are only supported for DTMCs and CTMCs");
+			throw new PrismNotSupportedException("Parametric long-run average rewards are only supported for DTMCs and CTMCs");
 		}
 		RegionValues allTrue = regionFactory.completeCover(true);
 		BitSet needStatesInner = new BitSet(needStates.size());
@@ -1128,7 +1129,7 @@ final public class ParamModelChecker extends PrismComponent
 		RegionValues b = checkExpression(model,expr, needStatesInner);
 		if (model.getModelType() != ModelType.DTMC
 				&& model.getModelType() != ModelType.CTMC) {
-			throw new PrismException("Parametric engine currently only implements steady state for DTMCs and CTMCs.");
+			throw new PrismNotSupportedException("Parametric engine currently only implements steady state for DTMCs and CTMCs.");
 		}
 		return valueComputer.computeSteadyState(b, min, null);
 	}

prism/src/prism/LTL2DA.java

@@ -90,7 +90,7 @@ public class LTL2DA extends PrismComponent
 		}
 
 		if (result == null) {
-			throw new PrismException("Could not convert LTL formula to deterministic automaton");
+			throw new PrismNotSupportedException("Could not convert LTL formula to deterministic automaton");
 		}
 
 		result = DASimplifyAcceptance.simplifyAcceptance(result, allowedAcceptance);

prism/src/prism/LTL2RabinLibrary.java

@@ -127,7 +127,7 @@ public class LTL2RabinLibrary
 			    ((ExpressionTemporal)ltl).getOperator() == ExpressionTemporal.P_U) {
 				return constructDRAForSimpleUntilFormula((ExpressionTemporal)ltl, constants, negated);				
 			} else {
-				throw new PrismException("Unsupported LTL formula with time bounds: "+ltl);
+				throw new PrismNotSupportedException("Unsupported LTL formula with time bounds: "+ltl);
 			}
 		}
 		
@@ -169,7 +169,7 @@ public class LTL2RabinLibrary
 				labelA = null;
 				aBoolean = (Boolean) ((ExpressionLiteral)expr.getOperand1()).getValue();
 			} else {
-				throw new PrismException("Unsupported expression "+expr.getOperand1()+" in formula.");
+				throw new PrismNotSupportedException("Unsupported expression "+expr.getOperand1()+" in formula.");
 			}
 		}
 
@@ -182,7 +182,7 @@ public class LTL2RabinLibrary
 				labelB = null;
 				bBoolean = (Boolean) ((ExpressionLiteral)expr.getOperand2()).getValue();
 			} else {
-				throw new PrismException("Unsupported expression "+expr.getOperand2()+" in formula.");
+				throw new PrismNotSupportedException("Unsupported expression "+expr.getOperand2()+" in formula.");
 			}
 		}
 		

prism/src/prism/LTLModelChecker.java

@@ -698,7 +698,7 @@ public class LTLModelChecker extends PrismComponent
 		case RABIN:
 			return findAcceptingECStatesForRabin((AcceptanceRabinDD) acceptance, model, daDDRowVars, daDDColVars, fairness);
 		default:
-			throw new PrismException("Computing the accepting EC states for "+acceptance.getTypeName()+" acceptance is not yet implemented (symbolic engine)");
+			throw new PrismNotSupportedException("Computing the accepting EC states for "+acceptance.getTypeName()+" acceptance is not yet implemented (symbolic engine)");
 		}
 	}
 

prism/src/prism/Modules2MTBDD.java

@@ -181,7 +181,7 @@ public class Modules2MTBDD
 		// get variable info from ModulesFile
 		varList = modulesFile.createVarList();
 		if (varList.containsUnboundedVariables())
-			throw new PrismException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)");
+			throw new PrismNotSupportedException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)");
 		numVars = varList.getNumVars();
 		constantValues = modulesFile.getConstantValues();
 		

prism/src/prism/MultiObjModelChecker.java

@@ -641,12 +641,12 @@ public class MultiObjModelChecker extends PrismComponent
 		
 		try {
 			if (engine != Prism.SPARSE)
-				throw new PrismException("Currently only sparse engine supports multi-objective properties");
+				throw new PrismNotSupportedException("Currently only sparse engine supports multi-objective properties");
 		
 			if (method == Prism.MDP_MULTI_LP) {
 				//LP currently does not support Pareto
 				if (opsAndBounds.numberOfNumerical() > 1) {
-					throw new PrismException("Linear programming method currently does not support generating of Pareto curves.");
+					throw new PrismNotSupportedException("Linear programming method currently does not support generating of Pareto curves.");
 				}
 				
 				if (opsAndBounds.rewardSize() > 0) {