From b12953b9379ee3c3aea9ba1026b7564eb39e57f7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Jun 2015 15:03:21 +0000 Subject: [PATCH] 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 | 3 +- prism/src/explicit/ConstructModel.java | 7 ++-- prism/src/explicit/DTMCEmbeddedSimple.java | 3 +- .../explicit/DTMCFromMDPAndMDStrategy.java | 3 +- .../DTMCFromMDPMemorylessAdversary.java | 3 +- prism/src/explicit/DTMCModelChecker.java | 5 ++- prism/src/explicit/DTMCUniformisedSimple.java | 3 +- ...astAdaptiveUniformisationModelChecker.java | 19 ++++----- prism/src/explicit/LTLModelChecker.java | 6 +-- prism/src/explicit/NonProbModelChecker.java | 5 ++- prism/src/explicit/PrismExplicit.java | 14 +++---- .../src/explicit/PrismSTPGAbstractRefine.java | 9 +++-- prism/src/explicit/ProbModelChecker.java | 39 ++++++++++--------- prism/src/explicit/Product.java | 3 +- prism/src/explicit/QuantAbstractRefine.java | 20 +++++----- .../explicit/QuantAbstractRefineExample.java | 3 +- prism/src/explicit/STPGAbstrSimple.java | 3 +- prism/src/explicit/STPGModelChecker.java | 3 +- prism/src/explicit/StateModelChecker.java | 5 ++- .../explicit/rewards/ConstructRewards.java | 7 ++-- prism/src/param/ModelBuilder.java | 15 +++---- prism/src/param/ParamModelChecker.java | 25 ++++++------ prism/src/prism/LTL2DA.java | 2 +- prism/src/prism/LTL2RabinLibrary.java | 6 +-- prism/src/prism/LTLModelChecker.java | 2 +- prism/src/prism/Modules2MTBDD.java | 2 +- prism/src/prism/MultiObjModelChecker.java | 4 +- 27 files changed, 119 insertions(+), 100 deletions(-) diff --git a/prism/src/explicit/Bisimulation.java b/prism/src/explicit/Bisimulation.java index 4819169a..6126c462 100644 --- a/prism/src/explicit/Bisimulation.java +++ b/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"); } } diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 4cc2487c..f5b5d459 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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())); diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 3fad7719..abe6b516 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/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) diff --git a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java b/prism/src/explicit/DTMCFromMDPAndMDStrategy.java index f7225b94..8c083ef0 100644 --- a/prism/src/explicit/DTMCFromMDPAndMDStrategy.java +++ b/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) diff --git a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java b/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java index b7c76731..c75628c6 100644 --- a/prism/src/explicit/DTMCFromMDPMemorylessAdversary.java +++ b/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) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 1bc773fd..5b900bd3 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/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"); } /** diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index ccf430b3..14c55824 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/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) diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java index 43e1e17c..cc63656c 100644 --- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java +++ b/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); diff --git a/prism/src/explicit/LTLModelChecker.java b/prism/src/explicit/LTLModelChecker.java index f4509a5d..13111b6c 100644 --- a/prism/src/explicit/LTLModelChecker.java +++ b/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)."); } /** diff --git a/prism/src/explicit/NonProbModelChecker.java b/prism/src/explicit/NonProbModelChecker.java index 93dad65a..9d52c2ea 100644 --- a/prism/src/explicit/NonProbModelChecker.java +++ b/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 { diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index cb681014..f31333c6 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/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; diff --git a/prism/src/explicit/PrismSTPGAbstractRefine.java b/prism/src/explicit/PrismSTPGAbstractRefine.java index bf3c8228..7bcf2168 100644 --- a/prism/src/explicit/PrismSTPGAbstractRefine.java +++ b/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(1)); diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index dfbcdf16..5a721ed7 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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); } diff --git a/prism/src/explicit/Product.java b/prism/src/explicit/Product.java index aeb4d07e..b595d98a 100644 --- a/prism/src/explicit/Product.java +++ b/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 implements ModelTransformation= listNew.size()) listNew.add(new HashSet(1)); diff --git a/prism/src/explicit/STPGAbstrSimple.java b/prism/src/explicit/STPGAbstrSimple.java index 4706ef02..de4ea1b0 100644 --- a/prism/src/explicit/STPGAbstrSimple.java +++ b/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 diff --git a/prism/src/explicit/STPGModelChecker.java b/prism/src/explicit/STPGModelChecker.java index b7d111ba..2d834098 100644 --- a/prism/src/explicit/STPGModelChecker.java +++ b/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 diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 45eebcc3..91d04158 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/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() + "\""); } diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index b74bd617..b163ad31 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/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; diff --git a/prism/src/param/ModelBuilder.java b/prism/src/param/ModelBuilder.java index 50866b02..28702e4a 100644 --- a/prism/src/param/ModelBuilder.java +++ b/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; diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 1e0945f0..af9374a0 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/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); } diff --git a/prism/src/prism/LTL2DA.java b/prism/src/prism/LTL2DA.java index dcc84002..a985be25 100644 --- a/prism/src/prism/LTL2DA.java +++ b/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); diff --git a/prism/src/prism/LTL2RabinLibrary.java b/prism/src/prism/LTL2RabinLibrary.java index c3344437..8a587531 100644 --- a/prism/src/prism/LTL2RabinLibrary.java +++ b/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."); } } diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index cb48df6d..75485fcc 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/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)"); } } diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 2f1e287c..c8ed71fe 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/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(); diff --git a/prism/src/prism/MultiObjModelChecker.java b/prism/src/prism/MultiObjModelChecker.java index b4c3154c..b71e1eb1 100644 --- a/prism/src/prism/MultiObjModelChecker.java +++ b/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) {