From 1097ecaaebe0d073889da115ea6a20c01fda6e32 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Sep 2015 21:06:50 +0000 Subject: [PATCH] Add a second syntactic co-safe-ness check, which first converts to positive normal form. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10611 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/Expression.java | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index f16c2a26..4f37c215 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -809,13 +809,29 @@ public abstract class Expression extends ASTElement /** * Test if an expression is a co-safe LTL formula, detected syntactically - * (i.e. if it is in positive normal form and only uses X, F and U). + * (i.e. if it is in positive normal form and only uses X, F and U). */ public static boolean isCoSafeLTLSyntactic(Expression expr) { - // Check for positive normal form - if (!isPositiveNormalFormLTL(expr)) - return false; + return isCoSafeLTLSyntactic(expr, false); + } + + /** + * Test if an expression is a co-safe LTL formula, detected syntactically + * (i.e. if it is in positive normal form and only uses X, F and U). + * If {@code convert} is true, the expression is first converted into positive normal form, + * and then it is checked whether it only uses X, F and U. + * For example, a => ! (G b) would return true if (and only if) {@code convert} was true. + */ + public static boolean isCoSafeLTLSyntactic(Expression expr, boolean convert) + { + // Convert to or check for positive normal form + if (convert) { + expr = BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy()); + } else { + if (!isPositiveNormalFormLTL(expr)) + return false; + } // Check temporal operators try { ASTTraverse astt = new ASTTraverse()