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