From fa2b70f1e6f07d52d1738f04f22484e1343f8648 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 21 Feb 2012 14:38:55 +0000 Subject: [PATCH] Better error message for lack of filters in PTA m/c. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4687 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/pta/PTAModelChecker.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/prism/src/pta/PTAModelChecker.java b/prism/src/pta/PTAModelChecker.java index 3511c49a..4034ce3e 100644 --- a/prism/src/pta/PTAModelChecker.java +++ b/prism/src/pta/PTAModelChecker.java @@ -175,6 +175,8 @@ public class PTAModelChecker res = checkExpressionProb((ExpressionProb) expr); else if (expr instanceof ExpressionReward) res = checkExpressionReward((ExpressionReward) expr); + else if (expr instanceof ExpressionFilter) + throw new PrismException("PTA model checker does not handle filters since it only computes values for the initial state"); else throw new PrismException("PTA model checking not yet supported for this operator (try the digital clocks engine)");