From 7511a39939a153c001c5ba363126fdf3aeea0b5f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Sep 2015 21:07:33 +0000 Subject: [PATCH] Additional functionality in LTL parser test code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10612 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 19 +++++++++++-------- prism/src/parser/PrismParser.jj | 5 ++++- 2 files changed, 15 insertions(+), 9 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 551c1a44..d3a7271c 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -90,8 +90,11 @@ public class PrismParser implements PrismParserConstants { System.out.println("Type: " + expr.getType().getTypeString()); boolean pnf = Expression.isPositiveNormalFormLTL(expr); System.out.println("Positive normal form: " + pnf); + System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(expr)); if (!pnf) { - System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy())); + Expression exprPnf = BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy()); + System.out.println("Positive normal form conversion: " + exprPnf); + System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf)); } Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() { public Object visit(ExpressionVar e) throws PrismLangException @@ -4290,6 +4293,13 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3_1() { + if (jj_scan_token(MODULE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(EQ)) return true; + return false; + } + static private boolean jj_3R_117() { Token xsp; xsp = jj_scanpos; @@ -4301,13 +4311,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_1() { - if (jj_scan_token(MODULE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(EQ)) return true; - return false; - } - static private boolean jj_3R_201() { if (jj_3R_33()) return true; return false; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 34e2774c..9be848f5 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -123,8 +123,11 @@ public class PrismParser System.out.println("Type: " + expr.getType().getTypeString()); boolean pnf = Expression.isPositiveNormalFormLTL(expr); System.out.println("Positive normal form: " + pnf); + System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(expr)); if (!pnf) { - System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy())); + Expression exprPnf = BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy()); + System.out.println("Positive normal form conversion: " + exprPnf); + System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf)); } Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() { public Object visit(ExpressionVar e) throws PrismLangException