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

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

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