From 8dbdce2e910499f0bbab37eac1f75be003209f80 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 21 Aug 2015 00:28:44 +0000 Subject: [PATCH] Test code for LTL formulas in PrismParser. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10554 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 1867 +++++++++-------- prism/src/parser/PrismParser.jj | 50 + prism/src/parser/PrismParserTokenManager.java | 2 + 3 files changed, 1010 insertions(+), 909 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index febefe5c..3fb86b5c 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -5,8 +5,10 @@ import java.io.*; import java.util.List; import java.util.ArrayList; +import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; @@ -40,6 +42,7 @@ public class PrismParser implements PrismParserConstants { System.out.println("Where: = -modulesfile or -mf"); System.out.println(" -propertiesfile or -pf"); System.out.println(" -expression or -e"); + System.out.println(" -ltl or -l"); System.exit(1); } @@ -70,6 +73,25 @@ public class PrismParser implements PrismParserConstants { expr.semanticCheck(); System.out.println("Type: " + expr.getType().getTypeString()); System.out.println("Eval: " + expr.evaluate()); + } + else if (args[0].equals("-ltl") || args[0].equals("-l")) { + Expression expr = p.parseSingleLTLFormula(str); + expr = (Expression) expr.accept(new ASTTraverseModify() { + public Object visit(ExpressionIdent e) throws PrismLangException + { + return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance()); + } + }); + System.out.println("LTL formula: " + expr.toString()); + System.out.print("Tree:\u005cn=====\u005cn" + expr.toTreeString()); + expr.typeCheck(); + expr.semanticCheck(); + System.out.println("Type: " + expr.getType().getTypeString()); + boolean pnf = Expression.isPositiveNormalFormLTL(expr); + System.out.println("Positive normal form: " + pnf); + if (!pnf) { + System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy())); + } } else { System.out.println("Unknown switch"); System.exit(1); } @@ -160,6 +182,24 @@ public class PrismParser implements PrismParserConstants { return expr; } + // Parse a single LTL formula + + public Expression parseSingleLTLFormula(InputStream str) throws PrismLangException + { + Expression expr = null; + + // (Re)start parser + ReInit(str); + // Parse + try { + expr = SingleLTLFormula(); + } + catch (ParseException e) { + throw generateSyntaxError(e); + } + return expr; + } + // Parse a for loop public ForLoop parseForLoop(InputStream str) throws PrismLangException @@ -668,6 +708,15 @@ public class PrismParser implements PrismParserConstants { throw new Error("Missing return statement in function"); } +// A single LTL formula + static final public Expression SingleLTLFormula() throws ParseException { + Expression ret; + ret = Expression(true, true); + jj_consume_token(0); + {if (true) return ret;} + throw new Error("Missing return statement in function"); + } + //----------------------------------------------------------------------------------- // Modules file stuff (a few bits of which are reused for property files) //----------------------------------------------------------------------------------- @@ -3428,1629 +3477,1629 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(17, xla); } } - static private boolean jj_3R_168() { - if (jj_3R_47()) return true; + static private boolean jj_3R_165() { + if (jj_scan_token(P)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_190()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_191()) { + jj_scanpos = xsp; + if (jj_3R_192()) { + jj_scanpos = xsp; + if (jj_3R_193()) { + jj_scanpos = xsp; + if (jj_3R_194()) return true; + } + } + } return false; } - static private boolean jj_3R_67() { - if (jj_scan_token(MAX)) return true; + static private boolean jj_3R_62() { + if (jj_scan_token(U)) return true; return false; } - static private boolean jj_3R_66() { - if (jj_scan_token(MIN)) return true; + static private boolean jj_3R_147() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_165()) { + jj_scanpos = xsp; + if (jj_3R_166()) { + jj_scanpos = xsp; + if (jj_3R_167()) return true; + } + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_38()) return true; + xsp = jj_scanpos; + if (jj_3R_168()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_75() { - if (jj_3R_82()) return true; + static private boolean jj_3R_56() { Token xsp; xsp = jj_scanpos; - if (jj_3R_83()) jj_scanpos = xsp; + if (jj_3R_62()) { + jj_scanpos = xsp; + if (jj_3R_63()) { + jj_scanpos = xsp; + if (jj_3R_64()) return true; + } + } + xsp = jj_scanpos; + if (jj_3R_65()) jj_scanpos = xsp; + if (jj_3R_55()) return true; return false; } - static private boolean jj_3R_100() { - if (jj_3R_32()) return true; + static private boolean jj_3R_189() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_98() { - if (jj_3R_32()) return true; + static private boolean jj_3R_164() { + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_96() { - if (jj_3R_32()) return true; + static private boolean jj_3R_46() { + if (jj_3R_55()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_56()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_94() { - if (jj_3R_32()) return true; + static private boolean jj_3R_48() { + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } - static private boolean jj_3R_57() { - if (jj_scan_token(LBRACE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_66()) { - jj_scanpos = xsp; - if (jj_3R_67()) return true; - } - if (jj_scan_token(RBRACE)) return true; + static private boolean jj_3R_186() { + if (jj_scan_token(OR)) return true; return false; } - static private boolean jj_3R_89() { - if (jj_scan_token(EQ)) return true; - if (jj_3R_38()) return true; + static private boolean jj_3R_90() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_88() { - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(COMMA)) return true; + static private boolean jj_3R_146() { + if (jj_scan_token(LPARENTH)) return true; if (jj_3R_38()) return true; - if (jj_scan_token(RBRACKET)) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_47() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RBRACE)) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_57()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_163() { + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_87() { - if (jj_scan_token(GT)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_100()) { - jj_scanpos = xsp; - if (jj_3R_101()) return true; - } + static private boolean jj_3R_32() { + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_86() { - if (jj_scan_token(GE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_98()) { - jj_scanpos = xsp; - if (jj_3R_99()) return true; - } + static private boolean jj_3R_157() { + if (jj_scan_token(FALSE)) return true; return false; } - static private boolean jj_3R_85() { - if (jj_scan_token(LT)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_96()) { - jj_scanpos = xsp; - if (jj_3R_97()) return true; - } + static private boolean jj_3R_156() { + if (jj_scan_token(TRUE)) return true; return false; } - static private boolean jj_3R_84() { - if (jj_scan_token(LE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_94()) { - jj_scanpos = xsp; - if (jj_3R_95()) return true; - } + static private boolean jj_3R_185() { + if (jj_scan_token(AND)) return true; return false; } - static private boolean jj_3R_76() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_84()) { - jj_scanpos = xsp; - if (jj_3R_85()) { - jj_scanpos = xsp; - if (jj_3R_86()) { - jj_scanpos = xsp; - if (jj_3R_87()) { - jj_scanpos = xsp; - if (jj_3R_88()) { - jj_scanpos = xsp; - if (jj_3R_89()) return true; - } - } - } - } - } + static private boolean jj_3R_183() { + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_61() { - if (jj_3R_75()) return true; + static private boolean jj_3R_38() { + if (jj_3R_46()) return true; return false; } - static private boolean jj_3R_74() { - if (jj_3R_76()) return true; + static private boolean jj_3_4() { + if (jj_scan_token(LABEL)) return true; return false; } - static private boolean jj_3R_73() { - if (jj_scan_token(G)) return true; + static private boolean jj_3R_29() { + if (jj_scan_token(REG_IDENT)) return true; return false; } - static private boolean jj_3R_72() { - if (jj_scan_token(F)) return true; + static private boolean jj_3R_155() { + if (jj_scan_token(REG_DOUBLE)) return true; return false; } - static private boolean jj_3R_71() { - if (jj_scan_token(X)) return true; + static private boolean jj_3_3() { + if (jj_scan_token(LABEL)) return true; + if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_60() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_71()) { - jj_scanpos = xsp; - if (jj_3R_72()) { - jj_scanpos = xsp; - if (jj_3R_73()) return true; - } - } - xsp = jj_scanpos; - if (jj_3R_74()) jj_scanpos = xsp; - if (jj_3R_55()) return true; + static private boolean jj_3R_181() { + if (jj_scan_token(INIT)) return true; return false; } - static private boolean jj_3R_191() { - if (jj_3R_45()) return true; + static private boolean jj_3R_162() { + if (jj_scan_token(MIN)) return true; + return false; + } + + static private boolean jj_3R_188() { + if (jj_scan_token(COMMA)) return true; if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_190() { + static private boolean jj_3R_79() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_32()) return true; + if (jj_3R_31()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_54() { - if (jj_scan_token(LE)) return true; + static private boolean jj_3R_154() { + if (jj_scan_token(REG_INT)) return true; return false; } - static private boolean jj_3R_53() { - if (jj_scan_token(GE)) return true; + static private boolean jj_3R_78() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_52() { - if (jj_scan_token(LT)) return true; - return false; - } - - static private boolean jj_3R_51() { - if (jj_scan_token(GT)) return true; + static private boolean jj_3R_187() { + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_45() { + static private boolean jj_3R_142() { Token xsp; xsp = jj_scanpos; - if (jj_3R_51()) { + if (jj_3R_154()) { jj_scanpos = xsp; - if (jj_3R_52()) { + if (jj_3R_155()) { jj_scanpos = xsp; - if (jj_3R_53()) { + if (jj_3R_156()) { jj_scanpos = xsp; - if (jj_3R_54()) return true; + if (jj_3R_157()) return true; } } } return false; } - static private boolean jj_3R_194() { - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_184() { + if (jj_scan_token(PLUS)) return true; return false; } - static private boolean jj_3R_193() { + static private boolean jj_3R_182() { if (jj_scan_token(MIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_192() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_77() { + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_167() { - if (jj_scan_token(PMAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_70() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_55() { + static private boolean jj_3R_160() { + if (jj_scan_token(MAX)) return true; + return false; + } + + static private boolean jj_3R_180() { + if (jj_3R_29()) return true; + return false; + } + + static private boolean jj_3R_68() { Token xsp; xsp = jj_scanpos; - if (jj_3R_60()) { + if (jj_3R_77()) { jj_scanpos = xsp; - if (jj_3R_61()) return true; + if (jj_3R_78()) { + jj_scanpos = xsp; + if (jj_3R_79()) return true; + } } return false; } - static private boolean jj_3R_166() { - if (jj_scan_token(PMIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_153() { + if (jj_scan_token(FILTER)) return true; + if (jj_scan_token(LPARENTH)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_182()) { + jj_scanpos = xsp; + if (jj_3R_183()) { + jj_scanpos = xsp; + if (jj_3R_184()) { + jj_scanpos = xsp; + if (jj_3R_185()) { + jj_scanpos = xsp; + if (jj_3R_186()) { + jj_scanpos = xsp; + if (jj_3R_187()) return true; + } + } + } + } + } + if (jj_scan_token(COMMA)) return true; + if (jj_3R_38()) return true; + xsp = jj_scanpos; + if (jj_3R_188()) jj_scanpos = xsp; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_65() { - if (jj_3R_76()) return true; + static private boolean jj_3R_161() { + if (jj_3R_38()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_189()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_119() { - if (jj_scan_token(NE)) return true; + static private boolean jj_3R_91() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(RENAME)) return true; + if (jj_3R_29()) return true; return false; } - static private boolean jj_3R_64() { - if (jj_scan_token(R)) return true; + static private boolean jj_3_9() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; return false; } - static private boolean jj_3R_115() { + static private boolean jj_3R_81() { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(RENAME)) return true; + if (jj_3R_29()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_118()) { - jj_scanpos = xsp; - if (jj_3R_119()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3R_91()) { jj_scanpos = xsp; break; } } + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_118() { - if (jj_scan_token(EQ)) return true; - return false; - } - - static private boolean jj_3R_63() { - if (jj_scan_token(W)) return true; + static private boolean jj_3R_50() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_165() { - if (jj_scan_token(P)) return true; + static private boolean jj_3R_145() { + if (jj_scan_token(FUNC)) return true; + if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_190()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_191()) { - jj_scanpos = xsp; - if (jj_3R_192()) { + if (jj_3R_162()) { jj_scanpos = xsp; - if (jj_3R_193()) { + if (jj_3R_163()) { jj_scanpos = xsp; - if (jj_3R_194()) return true; - } + if (jj_3R_164()) return true; } } + if (jj_scan_token(COMMA)) return true; + if (jj_3R_161()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_62() { - if (jj_scan_token(U)) return true; + static private boolean jj_3R_179() { + if (jj_3R_143()) return true; return false; } - static private boolean jj_3R_147() { + static private boolean jj_3R_152() { + if (jj_scan_token(DQUOTE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_165()) { - jj_scanpos = xsp; - if (jj_3R_166()) { + if (jj_3R_180()) { jj_scanpos = xsp; - if (jj_3R_167()) return true; + if (jj_3R_181()) return true; } + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static private boolean jj_3R_80() { + if (jj_scan_token(DIVIDE)) return true; + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_29()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_90()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - xsp = jj_scanpos; - if (jj_3R_168()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_56() { + static private boolean jj_3R_69() { Token xsp; xsp = jj_scanpos; - if (jj_3R_62()) { - jj_scanpos = xsp; - if (jj_3R_63()) { + if (jj_3R_80()) { jj_scanpos = xsp; - if (jj_3R_64()) return true; + if (jj_3R_81()) return true; } + return false; + } + + static private boolean jj_3R_177() { + if (jj_3R_148()) return true; + return false; + } + + static private boolean jj_3R_58() { + if (jj_3R_68()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_69()) { jj_scanpos = xsp; break; } } - xsp = jj_scanpos; - if (jj_3R_65()) jj_scanpos = xsp; - if (jj_3R_55()) return true; return false; } - static private boolean jj_3R_189() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; + static private boolean jj_3R_159() { + if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_164() { - if (jj_3R_29()) return true; + static private boolean jj_3_8() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; return false; } - static private boolean jj_3R_46() { - if (jj_3R_55()) return true; + static private boolean jj_3R_144() { Token xsp; xsp = jj_scanpos; - if (jj_3R_56()) jj_scanpos = xsp; + if (jj_3R_159()) { + jj_scanpos = xsp; + if (jj_3R_160()) return true; + } + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_161()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_48() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + static private boolean jj_3R_217() { + Token xsp; + xsp = jj_scanpos; + if (jj_scan_token(86)) { + jj_scanpos = xsp; + if (jj_scan_token(89)) return true; + } return false; } - static private boolean jj_3R_186() { + static private boolean jj_3R_43() { if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; + if (jj_3R_49()) return true; return false; } - static private boolean jj_3R_90() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; - return false; - } - - static private boolean jj_3R_146() { + static private boolean jj_3R_158() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_38()) return true; + if (jj_3R_161()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_163() { - if (jj_scan_token(MAX)) return true; - return false; - } - - static private boolean jj_3R_32() { - if (jj_3R_29()) return true; + static private boolean jj_3_10() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(LBRACKET)) return true; return false; } - static private boolean jj_3R_157() { - if (jj_scan_token(FALSE)) return true; + static private boolean jj_3R_218() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_217()) return true; return false; } - static private boolean jj_3R_156() { - if (jj_scan_token(TRUE)) return true; + static private boolean jj_3R_214() { + if (jj_3R_217()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_218()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_185() { - if (jj_scan_token(AND)) return true; + static private boolean jj_3_2() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(DQUOTE)) return true; + if (jj_scan_token(COLON)) return true; return false; } - static private boolean jj_3R_183() { - if (jj_scan_token(MAX)) return true; + static private boolean jj_3R_143() { + if (jj_3R_29()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_158()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_38() { - if (jj_3R_46()) return true; + static private boolean jj_3R_210() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_214()) jj_scanpos = xsp; return false; } - static private boolean jj_3_4() { - if (jj_scan_token(LABEL)) return true; + static private boolean jj_3R_209() { + if (jj_scan_token(TIMES)) return true; return false; } - static private boolean jj_3R_29() { - if (jj_scan_token(REG_IDENT)) return true; + static private boolean jj_3R_207() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_209()) { + jj_scanpos = xsp; + if (jj_3R_210()) return true; + } return false; } - static private boolean jj_3R_155() { - if (jj_scan_token(REG_DOUBLE)) return true; + static private boolean jj_3R_59() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_29()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_70()) { jj_scanpos = xsp; break; } + } + if (jj_scan_token(RBRACKET)) return true; + if (jj_scan_token(OR)) return true; + if (jj_3R_58()) return true; return false; } - static private boolean jj_3_3() { - if (jj_scan_token(LABEL)) return true; - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_49() { + if (jj_3R_58()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_59()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_181() { - if (jj_scan_token(INIT)) return true; + static private boolean jj_3R_141() { + if (jj_3R_153()) return true; return false; } - static private boolean jj_3R_162() { - if (jj_scan_token(MIN)) return true; + static private boolean jj_3R_140() { + if (jj_3R_152()) return true; return false; } - static private boolean jj_3R_188() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; + static private boolean jj_3R_139() { + if (jj_3R_151()) return true; return false; } - static private boolean jj_3R_79() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_31()) return true; - if (jj_scan_token(RPARENTH)) return true; + static private boolean jj_3R_178() { + if (jj_3R_146()) return true; return false; } - static private boolean jj_3R_154() { - if (jj_scan_token(REG_INT)) return true; + static private boolean jj_3R_176() { + if (jj_3R_147()) return true; return false; } - static private boolean jj_3R_78() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_138() { + if (jj_3R_150()) return true; return false; } - static private boolean jj_3R_187() { - if (jj_3R_29()) return true; + static private boolean jj_3R_175() { + if (jj_scan_token(DLBRACKET)) return true; + if (jj_3R_207()) return true; + if (jj_scan_token(DRBRACKET)) return true; return false; } - static private boolean jj_3R_142() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_154()) { - jj_scanpos = xsp; - if (jj_3R_155()) { - jj_scanpos = xsp; - if (jj_3R_156()) { - jj_scanpos = xsp; - if (jj_3R_157()) return true; - } - } - } + static private boolean jj_3R_137() { + if (jj_3R_149()) return true; return false; } - static private boolean jj_3R_184() { - if (jj_scan_token(PLUS)) return true; + static private boolean jj_3R_127() { + if (jj_scan_token(DIVIDE)) return true; return false; } - static private boolean jj_3R_182() { - if (jj_scan_token(MIN)) return true; + static private boolean jj_3R_216() { + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_77() { - if (jj_3R_29()) return true; + static private boolean jj_3R_174() { + if (jj_scan_token(DLT)) return true; + if (jj_3R_207()) return true; + if (jj_scan_token(DGT)) return true; return false; } - static private boolean jj_3R_70() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; + static private boolean jj_3R_136() { + if (jj_3R_148()) return true; return false; } - static private boolean jj_3R_160() { - if (jj_scan_token(MAX)) return true; + static private boolean jj_3R_135() { + if (jj_3R_33()) return true; return false; } - static private boolean jj_3R_180() { - if (jj_3R_29()) return true; + static private boolean jj_3R_134() { + if (jj_3R_147()) return true; return false; } - static private boolean jj_3R_68() { + static private boolean jj_3R_151() { Token xsp; xsp = jj_scanpos; - if (jj_3R_77()) { - jj_scanpos = xsp; - if (jj_3R_78()) { + if (jj_3R_174()) { jj_scanpos = xsp; - if (jj_3R_79()) return true; - } + if (jj_3R_175()) return true; } - return false; - } - - static private boolean jj_3R_153() { - if (jj_scan_token(FILTER)) return true; - if (jj_scan_token(LPARENTH)) return true; - Token xsp; xsp = jj_scanpos; - if (jj_3R_182()) { - jj_scanpos = xsp; - if (jj_3R_183()) { - jj_scanpos = xsp; - if (jj_3R_184()) { + if (jj_3R_176()) { jj_scanpos = xsp; - if (jj_3R_185()) { + if (jj_3R_177()) { jj_scanpos = xsp; - if (jj_3R_186()) { + if (jj_3R_178()) { jj_scanpos = xsp; - if (jj_3R_187()) return true; - } - } - } + if (jj_3R_179()) return true; } } - if (jj_scan_token(COMMA)) return true; - if (jj_3R_38()) return true; - xsp = jj_scanpos; - if (jj_3R_188()) jj_scanpos = xsp; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - - static private boolean jj_3R_161() { - if (jj_3R_38()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_189()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_91() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(RENAME)) return true; - if (jj_3R_29()) return true; + static private boolean jj_3R_133() { + if (jj_3R_146()) return true; return false; } - static private boolean jj_3_9() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; + static private boolean jj_3R_132() { + if (jj_3R_145()) return true; return false; } - static private boolean jj_3R_81() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(RENAME)) return true; - if (jj_3R_29()) return true; + static private boolean jj_3R_42() { + if (jj_3R_49()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_91()) { jj_scanpos = xsp; break; } + if (jj_3R_50()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_50() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; - if (jj_3R_35()) return true; + static private boolean jj_3R_131() { + if (jj_3R_144()) return true; return false; } - static private boolean jj_3R_145() { - if (jj_scan_token(FUNC)) return true; - if (jj_scan_token(LPARENTH)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_162()) { - jj_scanpos = xsp; - if (jj_3R_163()) { - jj_scanpos = xsp; - if (jj_3R_164()) return true; - } - } - if (jj_scan_token(COMMA)) return true; - if (jj_3R_161()) return true; - if (jj_scan_token(RPARENTH)) return true; + static private boolean jj_3R_130() { + if (jj_3R_143()) return true; return false; } - static private boolean jj_3R_179() { - if (jj_3R_143()) return true; + static private boolean jj_3R_129() { + if (jj_3R_142()) return true; return false; } - static private boolean jj_3R_152() { - if (jj_scan_token(DQUOTE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_180()) { - jj_scanpos = xsp; - if (jj_3R_181()) return true; - } - if (jj_scan_token(DQUOTE)) return true; - return false; - } - - static private boolean jj_3R_80() { - if (jj_scan_token(DIVIDE)) return true; - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_29()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_90()) { jj_scanpos = xsp; break; } - } - if (jj_scan_token(RBRACE)) return true; + static private boolean jj_3R_212() { + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_69() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_80()) { - jj_scanpos = xsp; - if (jj_3R_81()) return true; - } + static private boolean jj_3R_123() { + if (jj_scan_token(MINUS)) return true; return false; } - static private boolean jj_3R_177() { - if (jj_3R_148()) return true; + static private boolean jj_3R_150() { + if (jj_scan_token(A)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_58() { - if (jj_3R_68()) return true; + static private boolean jj_3R_128() { Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_69()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_129()) { + jj_scanpos = xsp; + if (jj_3R_130()) { + jj_scanpos = xsp; + if (jj_3R_131()) { + jj_scanpos = xsp; + if (jj_3R_132()) { + jj_scanpos = xsp; + if (jj_3R_133()) { + jj_scanpos = xsp; + if (jj_3R_134()) { + jj_scanpos = xsp; + if (jj_3R_135()) { + jj_scanpos = xsp; + if (jj_3R_136()) { + jj_scanpos = xsp; + if (jj_3R_137()) { + jj_scanpos = xsp; + if (jj_3R_138()) { + jj_scanpos = xsp; + if (jj_3R_139()) { + jj_scanpos = xsp; + if (jj_3R_140()) { + jj_scanpos = xsp; + if (jj_3R_141()) return true; + } + } + } + } + } + } + } + } + } + } + } } return false; } - static private boolean jj_3R_159() { - if (jj_scan_token(MIN)) return true; + static private boolean jj_3R_125() { + if (jj_3R_128()) return true; return false; } - static private boolean jj_3_8() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; + static private boolean jj_3R_124() { + if (jj_scan_token(MINUS)) return true; + if (jj_3R_120()) return true; return false; } - static private boolean jj_3R_144() { + static private boolean jj_3R_35() { + if (jj_3R_42()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_159()) { - jj_scanpos = xsp; - if (jj_3R_160()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3R_43()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_161()) return true; - if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_217() { + static private boolean jj_3R_120() { Token xsp; xsp = jj_scanpos; - if (jj_scan_token(86)) { + if (jj_3R_124()) { jj_scanpos = xsp; - if (jj_scan_token(89)) return true; + if (jj_3R_125()) return true; } return false; } - static private boolean jj_3_2() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; - if (jj_scan_token(COLON)) return true; - return false; - } - - static private boolean jj_3R_43() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; - if (jj_3R_49()) return true; - return false; - } - - static private boolean jj_3R_158() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_161()) return true; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - - static private boolean jj_3_10() { - if (jj_scan_token(OR)) return true; + static private boolean jj_3R_149() { + if (jj_scan_token(E)) return true; if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_218() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_217()) return true; + static private boolean jj_3R_126() { + if (jj_scan_token(TIMES)) return true; return false; } - static private boolean jj_3R_214() { - if (jj_3R_217()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_218()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_31() { + if (jj_3R_35()) return true; return false; } - static private boolean jj_3R_143() { - if (jj_3R_29()) return true; + static private boolean jj_3R_121() { Token xsp; xsp = jj_scanpos; - if (jj_3R_158()) jj_scanpos = xsp; + if (jj_3R_126()) { + jj_scanpos = xsp; + if (jj_3R_127()) return true; + } + if (jj_3R_120()) return true; return false; } - static private boolean jj_3R_210() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_214()) jj_scanpos = xsp; + static private boolean jj_3_7() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_31()) return true; return false; } - static private boolean jj_3R_209() { - if (jj_scan_token(TIMES)) return true; + static private boolean jj_3_18() { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_207() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_209()) { - jj_scanpos = xsp; - if (jj_3R_210()) return true; - } + static private boolean jj_3R_206() { + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_59() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_29()) return true; + static private boolean jj_3R_116() { + if (jj_3R_120()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_70()) { jj_scanpos = xsp; break; } + if (jj_3R_121()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(RBRACKET)) return true; - if (jj_scan_token(OR)) return true; - if (jj_3R_58()) return true; return false; } - static private boolean jj_3R_49() { - if (jj_3R_58()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_59()) jj_scanpos = xsp; + static private boolean jj_3_17() { + if (jj_3R_33()) return true; return false; } - static private boolean jj_3R_141() { - if (jj_3R_153()) return true; + static private boolean jj_3R_205() { + if (jj_scan_token(I)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_140() { - if (jj_3R_152()) return true; + static private boolean jj_3_16() { + if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_139() { - if (jj_3R_151()) return true; + static private boolean jj_3R_204() { + if (jj_scan_token(C)) return true; return false; } - static private boolean jj_3R_178() { - if (jj_3R_146()) return true; + static private boolean jj_3R_203() { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_176() { - if (jj_3R_147()) return true; + static private boolean jj_3R_122() { + if (jj_scan_token(PLUS)) return true; return false; } - static private boolean jj_3R_138() { - if (jj_3R_150()) return true; + static private boolean jj_3R_202() { + if (jj_scan_token(S)) return true; return false; } - static private boolean jj_3R_175() { - if (jj_scan_token(DLBRACKET)) return true; - if (jj_3R_207()) return true; - if (jj_scan_token(DRBRACKET)) return true; + static private boolean jj_3R_173() { + if (jj_3R_47()) return true; return false; } - static private boolean jj_3R_137() { - if (jj_3R_149()) return true; + 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_127() { - if (jj_scan_token(DIVIDE)) return true; + static private boolean jj_3R_117() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_122()) { + jj_scanpos = xsp; + if (jj_3R_123()) return true; + } + if (jj_3R_116()) return true; return false; } - static private boolean jj_3R_216() { - if (jj_3R_38()) return true; + static private boolean jj_3R_201() { + if (jj_3R_33()) return true; return false; } - static private boolean jj_3R_174() { - if (jj_scan_token(DLT)) return true; - if (jj_3R_207()) return true; - if (jj_scan_token(DGT)) return true; + static private boolean jj_3R_215() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_136() { - if (jj_3R_148()) return true; + static private boolean jj_3R_172() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_201()) { + jj_scanpos = xsp; + if (jj_3R_202()) { + jj_scanpos = xsp; + if (jj_3R_203()) { + jj_scanpos = xsp; + if (jj_3R_204()) { + jj_scanpos = xsp; + if (jj_3R_205()) { + jj_scanpos = xsp; + if (jj_3R_206()) return true; + } + } + } + } + } return false; } - static private boolean jj_3R_135() { - if (jj_3R_33()) return true; + static private boolean jj_3_15() { + if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_134() { - if (jj_3R_147()) return true; + static private boolean jj_3R_113() { + if (jj_3R_116()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_117()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_151() { + static private boolean jj_3_6() { + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static private boolean jj_3R_211() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_29()) return true; + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static private boolean jj_3R_213() { + if (jj_scan_token(DIVIDE)) return true; + if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_174()) { + if (jj_3R_215()) { jj_scanpos = xsp; - if (jj_3R_175()) return true; + if (jj_3R_216()) return true; } + if (jj_scan_token(RBRACE)) return true; + return false; + } + + static private boolean jj_3R_114() { + if (jj_3R_45()) return true; + if (jj_3R_113()) return true; + return false; + } + + static private boolean jj_3R_208() { + if (jj_scan_token(LBRACE)) return true; + Token xsp; xsp = jj_scanpos; - if (jj_3R_176()) { - jj_scanpos = xsp; - if (jj_3R_177()) { - jj_scanpos = xsp; - if (jj_3R_178()) { + if (jj_3R_211()) { jj_scanpos = xsp; - if (jj_3R_179()) return true; - } - } + if (jj_3R_212()) return true; } + if (jj_scan_token(RBRACE)) return true; + xsp = jj_scanpos; + if (jj_3R_213()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_133() { - if (jj_3R_146()) return true; + static private boolean jj_3R_111() { + if (jj_3R_113()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_114()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_132() { - if (jj_3R_145()) return true; + static private boolean jj_3R_112() { + if (jj_3R_115()) return true; + if (jj_3R_111()) return true; return false; } - static private boolean jj_3R_42() { - if (jj_3R_49()) return true; + static private boolean jj_3R_110() { + if (jj_3R_111()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_50()) { jj_scanpos = xsp; break; } + if (jj_3R_112()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3R_131() { - if (jj_3R_144()) return true; + static private boolean jj_3R_109() { + if (jj_3R_110()) return true; return false; } - static private boolean jj_3R_130() { - if (jj_3R_143()) return true; + static private boolean jj_3R_108() { + if (jj_scan_token(NOT)) return true; + if (jj_3R_106()) return true; return false; } - static private boolean jj_3R_129() { - if (jj_3R_142()) return true; + static private boolean jj_3R_101() { + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_212() { + static private boolean jj_3R_99() { if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_123() { - if (jj_scan_token(MINUS)) return true; + static private boolean jj_3R_97() { + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_150() { - if (jj_scan_token(A)) return true; - if (jj_scan_token(LBRACKET)) return true; + static private boolean jj_3R_95() { if (jj_3R_38()) return true; - if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_128() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_129()) { - jj_scanpos = xsp; - if (jj_3R_130()) { - jj_scanpos = xsp; - if (jj_3R_131()) { - jj_scanpos = xsp; - if (jj_3R_132()) { - jj_scanpos = xsp; - if (jj_3R_133()) { - jj_scanpos = xsp; - if (jj_3R_134()) { - jj_scanpos = xsp; - if (jj_3R_135()) { - jj_scanpos = xsp; - if (jj_3R_136()) { - jj_scanpos = xsp; - if (jj_3R_137()) { - jj_scanpos = xsp; - if (jj_3R_138()) { - jj_scanpos = xsp; - if (jj_3R_139()) { - jj_scanpos = xsp; - if (jj_3R_140()) { - jj_scanpos = xsp; - if (jj_3R_141()) return true; - } - } - } - } - } - } - } - } - } - } - } - } + static private boolean jj_3R_197() { + if (jj_3R_45()) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_125() { - if (jj_3R_128()) return true; + static private boolean jj_3R_196() { + if (jj_3R_208()) return true; return false; } - static private boolean jj_3R_124() { - if (jj_scan_token(MINUS)) return true; - if (jj_3R_120()) return true; + static private boolean jj_3R_195() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_32()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_35() { - if (jj_3R_42()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_43()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_41() { + if (jj_scan_token(AND)) return true; + if (jj_3R_40()) return true; return false; } - static private boolean jj_3R_120() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_124()) { - jj_scanpos = xsp; - if (jj_3R_125()) return true; - } + static private boolean jj_3R_200() { + if (jj_scan_token(MAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_149() { - if (jj_scan_token(E)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(RBRACKET)) return true; + static private boolean jj_3R_171() { + if (jj_scan_token(RMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_126() { - if (jj_scan_token(TIMES)) return true; + static private boolean jj_3R_199() { + if (jj_scan_token(MIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_31() { - if (jj_3R_35()) return true; + static private boolean jj_3R_170() { + if (jj_scan_token(RMIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_121() { + static private boolean jj_3R_106() { Token xsp; xsp = jj_scanpos; - if (jj_3R_126()) { + if (jj_3R_108()) { jj_scanpos = xsp; - if (jj_3R_127()) return true; + if (jj_3R_109()) return true; } - if (jj_3R_120()) return true; - return false; - } - - static private boolean jj_3_7() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_31()) return true; return false; } - static private boolean jj_3_18() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; - return false; - } - - static private boolean jj_3_1() { - if (jj_scan_token(MODULE)) return true; - if (jj_3R_29()) return true; + static private boolean jj_3R_198() { if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_206() { - if (jj_3R_38()) return true; + static private boolean jj_3R_39() { + if (jj_3R_47()) return true; return false; } - static private boolean jj_3R_116() { - if (jj_3R_120()) return true; + static private boolean jj_3R_169() { + if (jj_scan_token(R)) return true; Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_121()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_195()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_196()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_197()) { + jj_scanpos = xsp; + if (jj_3R_198()) { + jj_scanpos = xsp; + if (jj_3R_199()) { + jj_scanpos = xsp; + if (jj_3R_200()) return true; + } + } } return false; } - static private boolean jj_3_17() { - if (jj_3R_33()) return true; - return false; - } - - static private boolean jj_3R_205() { - if (jj_scan_token(I)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_38()) return true; - return false; - } - - static private boolean jj_3_16() { - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_107() { + if (jj_scan_token(AND)) return true; + if (jj_3R_106()) return true; return false; } - static private boolean jj_3R_204() { - if (jj_scan_token(C)) return true; + static private boolean jj_3R_148() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_169()) { + jj_scanpos = xsp; + if (jj_3R_170()) { + jj_scanpos = xsp; + if (jj_3R_171()) return true; + } + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_172()) return true; + xsp = jj_scanpos; + if (jj_3R_173()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_203() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; + static private boolean jj_3R_40() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_48()) return true; + if (jj_scan_token(EQ)) return true; if (jj_3R_38()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_122() { - if (jj_scan_token(PLUS)) return true; - return false; - } - - static private boolean jj_3R_202() { - if (jj_scan_token(S)) return true; + static private boolean jj_3R_104() { + if (jj_3R_106()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_107()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_173() { - if (jj_3R_47()) return true; + static private boolean jj_3R_105() { + if (jj_scan_token(OR)) return true; + if (jj_3R_104()) return true; return false; } - static private boolean jj_3R_117() { + static private boolean jj_3R_34() { + if (jj_3R_40()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_122()) { - jj_scanpos = xsp; - if (jj_3R_123()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3R_41()) { jj_scanpos = xsp; break; } } - if (jj_3R_116()) return true; return false; } - static private boolean jj_3R_201() { - if (jj_3R_33()) return true; + static private boolean jj_3_5() { + if (jj_3R_30()) return true; return false; } - static private boolean jj_3R_215() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_102() { + if (jj_3R_104()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_105()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_172() { + static private boolean jj_3R_30() { Token xsp; xsp = jj_scanpos; - if (jj_3R_201()) { - jj_scanpos = xsp; - if (jj_3R_202()) { - jj_scanpos = xsp; - if (jj_3R_203()) { - jj_scanpos = xsp; - if (jj_3R_204()) { - jj_scanpos = xsp; - if (jj_3R_205()) { + if (jj_3R_34()) { jj_scanpos = xsp; - if (jj_3R_206()) return true; - } - } - } - } + if (jj_scan_token(49)) return true; } return false; } - static private boolean jj_3_15() { - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_103() { + if (jj_scan_token(IFF)) return true; + if (jj_3R_102()) return true; return false; } - static private boolean jj_3R_113() { - if (jj_3R_116()) return true; + static private boolean jj_3R_92() { + if (jj_3R_102()) return true; Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_117()) { jj_scanpos = xsp; break; } + if (jj_3R_103()) { jj_scanpos = xsp; break; } } return false; } - static private boolean jj_3_6() { - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_37() { + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_211() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_29()) return true; - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_44() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_32()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_213() { - if (jj_scan_token(DIVIDE)) return true; - if (jj_scan_token(LBRACE)) return true; + static private boolean jj_3R_36() { Token xsp; xsp = jj_scanpos; - if (jj_3R_215()) { - jj_scanpos = xsp; - if (jj_3R_216()) return true; - } - if (jj_scan_token(RBRACE)) return true; + if (jj_3R_44()) jj_scanpos = xsp; + if (jj_3R_45()) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_114() { - if (jj_3R_45()) return true; - if (jj_3R_113()) return true; + static private boolean jj_3R_93() { + if (jj_scan_token(IMPLIES)) return true; + if (jj_3R_92()) return true; return false; } - static private boolean jj_3R_208() { - if (jj_scan_token(LBRACE)) return true; + static private boolean jj_3R_82() { + if (jj_3R_92()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_93()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_33() { + if (jj_scan_token(S)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_211()) { + if (jj_3R_36()) { jj_scanpos = xsp; - if (jj_3R_212()) return true; + if (jj_3R_37()) return true; } - if (jj_scan_token(RBRACE)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_38()) return true; xsp = jj_scanpos; - if (jj_3R_213()) jj_scanpos = xsp; + if (jj_3R_39()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_111() { - if (jj_3R_113()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_114()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_83() { + if (jj_scan_token(QMARK)) return true; + if (jj_3R_82()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_3R_75()) return true; return false; } - static private boolean jj_3R_112() { - if (jj_3R_115()) return true; - if (jj_3R_111()) return true; + static private boolean jj_3_14() { + if (jj_3R_32()) return true; + if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_110() { - if (jj_3R_111()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_112()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3_13() { + if (jj_3R_32()) return true; + if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_109() { - if (jj_3R_110()) return true; + static private boolean jj_3_12() { + if (jj_3R_32()) return true; + if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_108() { - if (jj_scan_token(NOT)) return true; - if (jj_3R_106()) return true; + static private boolean jj_3_11() { + if (jj_3R_32()) return true; + if (jj_scan_token(LPARENTH)) return true; return false; } - static private boolean jj_3R_101() { - if (jj_3R_38()) return true; + static private boolean jj_3R_168() { + if (jj_3R_47()) return true; return false; } - static private boolean jj_3R_99() { - if (jj_3R_38()) return true; + static private boolean jj_3R_67() { + if (jj_scan_token(MAX)) return true; return false; } - static private boolean jj_3R_97() { - if (jj_3R_38()) return true; + static private boolean jj_3R_66() { + if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_95() { - if (jj_3R_38()) return true; + static private boolean jj_3R_75() { + if (jj_3R_82()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_83()) jj_scanpos = xsp; return false; } - static private boolean jj_3R_197() { - if (jj_3R_45()) return true; - if (jj_3R_38()) return true; + static private boolean jj_3R_100() { + if (jj_3R_32()) return true; return false; } - static private boolean jj_3R_196() { - if (jj_3R_208()) return true; + static private boolean jj_3R_98() { + if (jj_3R_32()) return true; return false; } - static private boolean jj_3R_195() { - if (jj_scan_token(LPARENTH)) return true; + static private boolean jj_3R_96() { if (jj_3R_32()) return true; - if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_41() { - if (jj_scan_token(AND)) return true; - if (jj_3R_40()) return true; + static private boolean jj_3R_94() { + if (jj_3R_32()) return true; return false; } - static private boolean jj_3R_200() { - if (jj_scan_token(MAX)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_57() { + if (jj_scan_token(LBRACE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_66()) { + jj_scanpos = xsp; + if (jj_3R_67()) return true; + } + if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_171() { - if (jj_scan_token(RMAX)) return true; + static private boolean jj_3R_89() { if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + if (jj_3R_38()) return true; return false; } - static private boolean jj_3R_199() { - if (jj_scan_token(MIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_88() { + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3R_170() { - if (jj_scan_token(RMIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_47() { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(RBRACE)) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_57()) { jj_scanpos = xsp; break; } + } return false; } - static private boolean jj_3R_106() { + static private boolean jj_3R_87() { + if (jj_scan_token(GT)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_108()) { + if (jj_3R_100()) { jj_scanpos = xsp; - if (jj_3R_109()) return true; + if (jj_3R_101()) return true; } return false; } - static private boolean jj_3R_198() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_86() { + if (jj_scan_token(GE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_98()) { + jj_scanpos = xsp; + if (jj_3R_99()) return true; + } return false; } - static private boolean jj_3R_39() { - if (jj_3R_47()) return true; + static private boolean jj_3R_85() { + if (jj_scan_token(LT)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_96()) { + jj_scanpos = xsp; + if (jj_3R_97()) return true; + } return false; } - static private boolean jj_3R_169() { - if (jj_scan_token(R)) return true; + static private boolean jj_3R_84() { + if (jj_scan_token(LE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_195()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_196()) jj_scanpos = xsp; + if (jj_3R_94()) { + jj_scanpos = xsp; + if (jj_3R_95()) return true; + } + return false; + } + + static private boolean jj_3R_76() { + Token xsp; xsp = jj_scanpos; - if (jj_3R_197()) { + if (jj_3R_84()) { jj_scanpos = xsp; - if (jj_3R_198()) { + if (jj_3R_85()) { jj_scanpos = xsp; - if (jj_3R_199()) { + if (jj_3R_86()) { jj_scanpos = xsp; - if (jj_3R_200()) return true; + if (jj_3R_87()) { + jj_scanpos = xsp; + if (jj_3R_88()) { + jj_scanpos = xsp; + if (jj_3R_89()) return true; + } + } } } } return false; } - static private boolean jj_3R_107() { - if (jj_scan_token(AND)) return true; - if (jj_3R_106()) return true; + static private boolean jj_3R_61() { + if (jj_3R_75()) return true; return false; } - static private boolean jj_3R_148() { + static private boolean jj_3R_74() { + if (jj_3R_76()) return true; + return false; + } + + static private boolean jj_3R_73() { + if (jj_scan_token(G)) return true; + return false; + } + + static private boolean jj_3R_72() { + if (jj_scan_token(F)) return true; + return false; + } + + static private boolean jj_3R_71() { + if (jj_scan_token(X)) return true; + return false; + } + + static private boolean jj_3R_60() { Token xsp; xsp = jj_scanpos; - if (jj_3R_169()) { + if (jj_3R_71()) { jj_scanpos = xsp; - if (jj_3R_170()) { + if (jj_3R_72()) { jj_scanpos = xsp; - if (jj_3R_171()) return true; + if (jj_3R_73()) return true; } } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_172()) return true; xsp = jj_scanpos; - if (jj_3R_173()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + if (jj_3R_74()) jj_scanpos = xsp; + if (jj_3R_55()) return true; return false; } - static private boolean jj_3R_40() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_48()) return true; - if (jj_scan_token(EQ)) return true; + static private boolean jj_3R_191() { + if (jj_3R_45()) return true; if (jj_3R_38()) return true; - if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_104() { - if (jj_3R_106()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_107()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_190() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_32()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_105() { - if (jj_scan_token(OR)) return true; - if (jj_3R_104()) return true; + static private boolean jj_3R_54() { + if (jj_scan_token(LE)) return true; return false; } - static private boolean jj_3R_34() { - if (jj_3R_40()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_41()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_53() { + if (jj_scan_token(GE)) return true; return false; } - static private boolean jj_3_5() { - if (jj_3R_30()) return true; + static private boolean jj_3R_52() { + if (jj_scan_token(LT)) return true; return false; } - static private boolean jj_3R_102() { - if (jj_3R_104()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_105()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_51() { + if (jj_scan_token(GT)) return true; return false; } - static private boolean jj_3R_30() { + static private boolean jj_3R_45() { Token xsp; xsp = jj_scanpos; - if (jj_3R_34()) { + if (jj_3R_51()) { jj_scanpos = xsp; - if (jj_scan_token(49)) return true; + if (jj_3R_52()) { + jj_scanpos = xsp; + if (jj_3R_53()) { + jj_scanpos = xsp; + if (jj_3R_54()) return true; + } + } } return false; } - static private boolean jj_3R_103() { - if (jj_scan_token(IFF)) return true; - if (jj_3R_102()) return true; + static private boolean jj_3R_194() { + if (jj_scan_token(MAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_92() { - if (jj_3R_102()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_103()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_193() { + if (jj_scan_token(MIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_37() { + static private boolean jj_3R_192() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_44() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_32()) return true; - if (jj_scan_token(RPARENTH)) return true; + static private boolean jj_3R_167() { + if (jj_scan_token(PMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_36() { + static private boolean jj_3R_55() { Token xsp; xsp = jj_scanpos; - if (jj_3R_44()) jj_scanpos = xsp; - if (jj_3R_45()) return true; - if (jj_3R_38()) return true; - return false; - } - - static private boolean jj_3R_93() { - if (jj_scan_token(IMPLIES)) return true; - if (jj_3R_92()) return true; + if (jj_3R_60()) { + jj_scanpos = xsp; + if (jj_3R_61()) return true; + } return false; } - static private boolean jj_3R_82() { - if (jj_3R_92()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_93()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_166() { + if (jj_scan_token(PMIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_33() { - if (jj_scan_token(S)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_36()) { - jj_scanpos = xsp; - if (jj_3R_37()) return true; - } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_38()) return true; - xsp = jj_scanpos; - if (jj_3R_39()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + static private boolean jj_3R_65() { + if (jj_3R_76()) return true; return false; } - static private boolean jj_3R_83() { - if (jj_scan_token(QMARK)) return true; - if (jj_3R_82()) return true; - if (jj_scan_token(COLON)) return true; - if (jj_3R_75()) return true; + static private boolean jj_3R_119() { + if (jj_scan_token(NE)) return true; return false; } - static private boolean jj_3_14() { - if (jj_3R_32()) return true; - if (jj_scan_token(LPARENTH)) return true; + static private boolean jj_3R_64() { + if (jj_scan_token(R)) return true; return false; } - static private boolean jj_3_13() { - if (jj_3R_32()) return true; - if (jj_scan_token(LPARENTH)) return true; + static private boolean jj_3R_115() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_118()) { + jj_scanpos = xsp; + if (jj_3R_119()) return true; + } return false; } - static private boolean jj_3_12() { - if (jj_3R_32()) return true; - if (jj_scan_token(LPARENTH)) return true; + static private boolean jj_3R_118() { + if (jj_scan_token(EQ)) return true; return false; } - static private boolean jj_3_11() { - if (jj_3R_32()) return true; - if (jj_scan_token(LPARENTH)) return true; + static private boolean jj_3R_63() { + if (jj_scan_token(W)) return true; return false; } diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 1ce1b92e..ee8bccdf 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -37,8 +37,10 @@ import java.io.*; import java.util.List; import java.util.ArrayList; +import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import parser.visitor.*; import prism.ModelType; import prism.PrismLangException; @@ -73,6 +75,7 @@ public class PrismParser System.out.println("Where: = -modulesfile or -mf"); System.out.println(" -propertiesfile or -pf"); System.out.println(" -expression or -e"); + System.out.println(" -ltl or -l"); System.exit(1); } @@ -103,6 +106,25 @@ public class PrismParser expr.semanticCheck(); System.out.println("Type: " + expr.getType().getTypeString()); System.out.println("Eval: " + expr.evaluate()); + } + else if (args[0].equals("-ltl") || args[0].equals("-l")) { + Expression expr = p.parseSingleLTLFormula(str); + expr = (Expression) expr.accept(new ASTTraverseModify() { + public Object visit(ExpressionIdent e) throws PrismLangException + { + return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance()); + } + }); + System.out.println("LTL formula: " + expr.toString()); + System.out.print("Tree:\n=====\n" + expr.toTreeString()); + expr.typeCheck(); + expr.semanticCheck(); + System.out.println("Type: " + expr.getType().getTypeString()); + boolean pnf = Expression.isPositiveNormalFormLTL(expr); + System.out.println("Positive normal form: " + pnf); + if (!pnf) { + System.out.println("Positive normal form conversion: " + BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy())); + } } else { System.out.println("Unknown switch"); System.exit(1); } @@ -193,6 +215,24 @@ public class PrismParser return expr; } + // Parse a single LTL formula + + public Expression parseSingleLTLFormula(InputStream str) throws PrismLangException + { + Expression expr = null; + + // (Re)start parser + ReInit(str); + // Parse + try { + expr = SingleLTLFormula(); + } + catch (ParseException e) { + throw generateSyntaxError(e); + } + return expr; + } + // Parse a for loop public ForLoop parseForLoop(InputStream str) throws PrismLangException @@ -600,6 +640,16 @@ Expression SingleExpression() : ( ret = Expression(false, false) ) { return ret; } } +// A single LTL formula + +Expression SingleLTLFormula() : +{ + Expression ret; +} +{ + ( ret = Expression(true, true) ) { return ret; } +} + //----------------------------------------------------------------------------------- // Modules file stuff (a few bits of which are reused for property files) //----------------------------------------------------------------------------------- diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index 72a27f88..dc522b57 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -3,8 +3,10 @@ package parser; import java.io.*; import java.util.List; import java.util.ArrayList; +import parser.BooleanUtils; import parser.ast.*; import parser.type.*; +import parser.visitor.*; import prism.ModelType; import prism.PrismLangException;