|
|
|
@ -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; |
|
|
|
|