From c311d413f7f3ac7845090a9ef1043b22e480b679 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 10 Feb 2016 13:44:07 +0000 Subject: [PATCH] prism.NonProbModelChecker: use PrismNotSupportedException for missing CTL functionality git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11172 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NonProbModelChecker.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index 1fc936c2..f2daf9f5 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -101,7 +101,7 @@ public class NonProbModelChecker extends StateModelChecker // Check whether this is a simple path formula (i.e. CTL, not LTL) if (!expr.isSimplePathFormula()) { - throw new PrismException("(Non-probabilistic) LTL model checking is not supported"); + throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported"); } // Negation/parentheses @@ -123,12 +123,12 @@ public class NonProbModelChecker extends StateModelChecker else if (expr instanceof ExpressionTemporal) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr; if (exprTemp.hasBounds()) { - throw new PrismException("Model checking of bounded CTL operators is not supported"); + throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported"); } // Next (EX) if (exprTemp.getOperator() == ExpressionTemporal.P_X) { // TODO - throw new PrismException("CTL model checking of the E X operator is not yet supported"); + throw new PrismNotSupportedException("CTL model checking of the E X operator is not yet supported"); } // Until (EU) else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { @@ -159,7 +159,7 @@ public class NonProbModelChecker extends StateModelChecker // Check whether this is a simple path formula (i.e. CTL, not LTL) if (!expr.isSimplePathFormula()) { - throw new PrismException("(Non-probabilistic) LTL model checking is not supported"); + throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported"); } // Negation/parentheses @@ -181,16 +181,16 @@ public class NonProbModelChecker extends StateModelChecker else if (expr instanceof ExpressionTemporal) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr; if (exprTemp.hasBounds()) { - throw new PrismException("Model checking of bounded CTL operators is not supported"); + throw new PrismNotSupportedException("Model checking of bounded CTL operators is not supported"); } // Next (AX) if (exprTemp.getOperator() == ExpressionTemporal.P_X) { // TODO - throw new PrismException("CTL model checking of the A X operator is not yet supported"); + throw new PrismNotSupportedException("CTL model checking of the A X operator is not yet supported"); } // Until (AU) else if (exprTemp.getOperator() == ExpressionTemporal.P_U) { - throw new PrismException("CTL model checking of the A U operator is not yet supported"); + throw new PrismNotSupportedException("CTL model checking of the A U operator is not yet supported"); } // Eventually (AF) else if (exprTemp.getOperator() == ExpressionTemporal.P_F) {