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;