From 0ed7e6cec6790b6e7f7deccb979250a5b672d3d0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:35 +0200 Subject: [PATCH] imported patch time-bounded-not-supported-message.patch --- prism/src/prism/LTLModelChecker.java | 2 +- prism/src/prism/NondetModelChecker.java | 8 ++++---- prism/src/prism/ProbModelChecker.java | 8 ++++---- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 8a82b3fd..82b5bccc 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -324,7 +324,7 @@ public class LTLModelChecker extends PrismComponent if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { - throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); + throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); } if (!expr.isSimplePathFormula()) { diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index dd4542f6..6fbe7811 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1555,7 +1555,7 @@ public class NondetModelChecker extends NonProbModelChecker if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { JDD.Deref(statesOfInterest); - throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); + throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); } if (expr.isSimplePathFormula()) { @@ -1569,18 +1569,18 @@ public class NondetModelChecker extends NonProbModelChecker expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); } else { JDD.Deref(statesOfInterest); - throw new PrismException("Time-bounded operators not supported in LTL: " + expr); + throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr); } } // Can't do "dfa" properties yet if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { JDD.Deref(statesOfInterest); - throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); + throw new PrismNotSupportedException("Model checking for \"dfa\" specifications not supported yet"); } if (Expression.containsTemporalRewardBounds(expr)) { - throw new PrismException("Can not handle reward bounds via deterministic automata."); + throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata."); } if (Expression.isHOA(expr)) { diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 83e22ff8..0c14bec6 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1015,25 +1015,25 @@ public class ProbModelChecker extends NonProbModelChecker if (Expression.containsTemporalRewardBounds(expr)) { JDD.Deref(statesOfInterest); - throw new PrismException("Can not handle reward bounds via deterministic automata."); + throw new PrismNotSupportedException("Can not handle reward bounds via deterministic automata."); } if (Expression.containsTemporalTimeBounds(expr)) { if (model.getModelType().continuousTime()) { JDD.Deref(statesOfInterest); - throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); + throw new PrismNotSupportedException("DA construction for time-bounded operators not supported for " + model.getModelType()+"."); } if (!expr.isSimplePathFormula()) { JDD.Deref(statesOfInterest); - throw new PrismException("Time-bounded operators not supported in LTL: " + expr); + throw new PrismNotSupportedException("Time-bounded operators not supported in LTL: " + expr); } } // Can't do "dfa" properties yet if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) { JDD.Deref(statesOfInterest); - throw new PrismException("Model checking for \"dfa\" specifications not supported yet"); + throw new PrismNotSupportedException("Model checking for \"dfa\" specifications not supported yet"); } if (Expression.isHOA(expr)) {