From 6231865f48bb675b2787b89688a97e37129f414d Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 11 Feb 2016 13:01:19 +0000 Subject: [PATCH] symbolic CTL: does not support fairness at the moment git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11183 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NonProbModelChecker.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/prism/src/prism/NonProbModelChecker.java b/prism/src/prism/NonProbModelChecker.java index f2daf9f5..8f331cd6 100644 --- a/prism/src/prism/NonProbModelChecker.java +++ b/prism/src/prism/NonProbModelChecker.java @@ -104,6 +104,10 @@ public class NonProbModelChecker extends StateModelChecker throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported"); } + if (prism.getFairness()) { + throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness"); + } + // Negation/parentheses if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr; @@ -162,6 +166,10 @@ public class NonProbModelChecker extends StateModelChecker throw new PrismNotSupportedException("(Non-probabilistic) LTL model checking is not supported"); } + if (prism.getFairness()) { + throw new PrismNotSupportedException("Non-probabilistic CTL model checking is not supported with fairness"); + } + // Negation/parentheses if (expr instanceof ExpressionUnaryOp) { ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;