From 0d5cc45f531dc9523922a5783665cb1c04adc88f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 21 Aug 2015 07:41:11 +0000 Subject: [PATCH] Bug fix in the check for syntactic co-safe LTL formulas: implication/iff not allowed. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10555 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/Expression.java | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index a3e91fee..f16c2a26 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -761,6 +761,7 @@ public abstract class Expression extends ASTElement /** * Test if an expression is an LTL formula and is in positive normal form, * i.e. where negation only occurs at the level of state formulae. + * This means that the operators => and <=> are also disallowed. */ public static boolean isPositiveNormalFormLTL(Expression expr) { @@ -782,7 +783,15 @@ public abstract class Expression extends ASTElement } else if (expr instanceof ExpressionBinaryOp) { ExpressionBinaryOp exprBinOp = (ExpressionBinaryOp) expr; - return isPositiveNormalFormLTL(exprBinOp.getOperand1()) && isPositiveNormalFormLTL(exprBinOp.getOperand2()); + int op = exprBinOp.getOperator(); + switch (op) { + // => and <=> are not allowed + case ExpressionBinaryOp.IMPLIES: + case ExpressionBinaryOp.IFF: + return false; + default: + return isPositiveNormalFormLTL(exprBinOp.getOperand1()) && isPositiveNormalFormLTL(exprBinOp.getOperand2()); + } } else if (expr instanceof ExpressionTemporal) { ExpressionTemporal exprTemp = (ExpressionTemporal) expr;