From e572ad0b2dcbc7b50de06541201b9c33d9cfffe3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 19 Mar 2008 17:03:14 +0000 Subject: [PATCH] Added weak until (W) and release (R) to properties language. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@700 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 543 ++++++++++-------- prism/src/parser/PrismParser.jj | 9 +- prism/src/parser/PrismParserConstants.java | 72 +-- prism/src/parser/PrismParserTokenManager.java | 207 +++---- prism/src/parser/ast/Expression.java | 4 + .../parser/ast/PathExpressionTemporal.java | 28 +- prism/src/parser/visitor/TypeCheck.java | 2 + 7 files changed, 471 insertions(+), 394 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index fbdc50ff..17181cb2 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -2072,7 +2072,7 @@ public class PrismParser implements PrismParserConstants { throw new Error("Missing return statement in function"); } -// Temporal operarors (X, U, F, G) +// Temporal operarors (X, U, F, G, W, R) static final public PathExpression PathExpressionTemporal() throws ParseException { PathExpressionTemporal pe = new PathExpressionTemporal(); Expression expr1 = null, expr2 = null; @@ -2104,8 +2104,24 @@ public class PrismParser implements PrismParserConstants { case REG_DOUBLE: case REG_IDENT: expr1 = Expression(); - jj_consume_token(U); - pe.setOperator(PathExpressionTemporal.P_U); + switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case U: + jj_consume_token(U); + pe.setOperator(PathExpressionTemporal.P_U); + break; + case W: + jj_consume_token(W); + pe.setOperator(PathExpressionTemporal.P_W); + break; + case R: + jj_consume_token(R); + pe.setOperator(PathExpressionTemporal.P_R); + break; + default: + jj_la1[61] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } break; case F: jj_consume_token(F); @@ -2116,7 +2132,7 @@ public class PrismParser implements PrismParserConstants { pe.setOperator(PathExpressionTemporal.P_G); break; default: - jj_la1[61] = jj_gen; + jj_la1[62] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2127,7 +2143,7 @@ public class PrismParser implements PrismParserConstants { tb = TimeBound(); break; default: - jj_la1[62] = jj_gen; + jj_la1[63] = jj_gen; ; } switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -2153,7 +2169,7 @@ public class PrismParser implements PrismParserConstants { expr2 = Expression(); break; default: - jj_la1[63] = jj_gen; + jj_la1[64] = jj_gen; ; } if (tb != null) pe.setLowerBound(tb.lBound); @@ -2245,7 +2261,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(RBRACKET); break; default: - jj_la1[64] = jj_gen; + jj_la1[65] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2279,7 +2295,7 @@ public class PrismParser implements PrismParserConstants { relOp = "="; break; default: - jj_la1[65] = jj_gen; + jj_la1[66] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2290,7 +2306,7 @@ public class PrismParser implements PrismParserConstants { filter = Filter(); break; default: - jj_la1[66] = jj_gen; + jj_la1[67] = jj_gen; ; } jj_consume_token(RBRACKET); @@ -2321,7 +2337,7 @@ public class PrismParser implements PrismParserConstants { index = RewardIndex(); break; default: - jj_la1[67] = jj_gen; + jj_la1[68] = jj_gen; ; } switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -2351,7 +2367,7 @@ public class PrismParser implements PrismParserConstants { relOp = "max="; break; default: - jj_la1[68] = jj_gen; + jj_la1[69] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2369,7 +2385,7 @@ public class PrismParser implements PrismParserConstants { relOp = "max="; break; default: - jj_la1[69] = jj_gen; + jj_la1[70] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2380,7 +2396,7 @@ public class PrismParser implements PrismParserConstants { filter = Filter(); break; default: - jj_la1[70] = jj_gen; + jj_la1[71] = jj_gen; ; } jj_consume_token(RBRACKET); @@ -2426,7 +2442,7 @@ public class PrismParser implements PrismParserConstants { index = Expression(); break; default: - jj_la1[71] = jj_gen; + jj_la1[72] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2464,7 +2480,7 @@ public class PrismParser implements PrismParserConstants { pe = new PathExpressionTemporal(PathExpressionTemporal.R_S, null, null); break; default: - jj_la1[72] = jj_gen; + jj_la1[73] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2487,7 +2503,7 @@ public class PrismParser implements PrismParserConstants { s = "init"; break; default: - jj_la1[73] = jj_gen; + jj_la1[74] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2532,7 +2548,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.NE;} break; default: - jj_la1[74] = jj_gen; + jj_la1[75] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2559,7 +2575,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.LE;} break; default: - jj_la1[75] = jj_gen; + jj_la1[76] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2584,7 +2600,7 @@ public class PrismParser implements PrismParserConstants { step = Expression(); break; default: - jj_la1[76] = jj_gen; + jj_la1[77] = jj_gen; ; } jj_consume_token(0); @@ -2660,28 +2676,8 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(8, xla); } } - static final private boolean jj_3R_120() { - Token xsp; - xsp = jj_scanpos; - 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()) return true; - } - } - } - xsp = jj_scanpos; - if (jj_3R_135()) jj_scanpos = xsp; - xsp = jj_scanpos; - if (jj_3R_136()) jj_scanpos = xsp; - return false; - } - - static final private boolean jj_3_9() { - if (jj_scan_token(DQUOTE)) return true; + static final private boolean jj_3R_130() { + if (jj_scan_token(S)) return true; return false; } @@ -2695,22 +2691,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_130() { - if (jj_scan_token(S)) return true; - return false; - } - static final private boolean jj_3R_129() { if (jj_scan_token(F)) return true; if (jj_3R_33()) return true; return false; } - static final private boolean jj_3R_74() { - if (jj_3R_80()) return true; - return false; - } - static final private boolean jj_3R_128() { if (jj_scan_token(I)) return true; if (jj_scan_token(EQ)) return true; @@ -2718,11 +2704,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_105() { - if (jj_3R_121()) return true; - return false; - } - static final private boolean jj_3R_127() { if (jj_scan_token(C)) return true; if (jj_scan_token(LE)) return true; @@ -2730,12 +2711,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_73() { - if (jj_3R_79()) return true; - return false; - } - - static final private boolean jj_3R_142() { + static final private boolean jj_3R_145() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_27()) return true; if (jj_scan_token(DQUOTE)) return true; @@ -2758,6 +2734,21 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_74() { + if (jj_3R_80()) return true; + return false; + } + + static final private boolean jj_3R_105() { + if (jj_3R_121()) return true; + return false; + } + + static final private boolean jj_3R_73() { + if (jj_3R_79()) return true; + return false; + } + static final private boolean jj_3R_31() { if (jj_scan_token(AND)) return true; if (jj_3R_30()) return true; @@ -2784,12 +2775,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_141() { + static final private boolean jj_3R_144() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_140() { + static final private boolean jj_3R_143() { if (jj_scan_token(MIN)) return true; return false; } @@ -2799,23 +2790,23 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_59() { - if (jj_scan_token(MINUS)) return true; - return false; - } - static final private boolean jj_3R_138() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_142()) { + if (jj_3R_145()) { jj_scanpos = xsp; - if (jj_3R_143()) return true; + if (jj_3R_146()) return true; } if (jj_scan_token(RBRACE)) return true; return false; } + static final private boolean jj_3R_59() { + if (jj_scan_token(MINUS)) return true; + return false; + } + static final private boolean jj_3R_30() { if (jj_scan_token(LPARENTH)) return true; if (jj_3R_32()) return true; @@ -2829,9 +2820,9 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_140()) { + if (jj_3R_143()) { jj_scanpos = xsp; - if (jj_3R_141()) return true; + if (jj_3R_144()) return true; } if (jj_scan_token(RBRACE)) return true; return false; @@ -2883,14 +2874,14 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_64() { - if (jj_scan_token(MINUS)) return true; - if (jj_3R_56()) return true; + static final private boolean jj_3R_122() { + if (jj_3R_138()) return true; return false; } - static final private boolean jj_3R_122() { - if (jj_3R_138()) return true; + static final private boolean jj_3R_64() { + if (jj_scan_token(MINUS)) return true; + if (jj_3R_56()) return true; return false; } @@ -2919,22 +2910,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_116() { - if (jj_3R_53()) return true; - if (jj_3R_33()) return true; - return false; - } - - static final private boolean jj_3R_56() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_64()) { - jj_scanpos = xsp; - if (jj_3R_65()) return true; - } - return false; - } - static final private boolean jj_3R_126() { if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; @@ -2956,21 +2931,20 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_110() { - if (jj_scan_token(RMIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static final private boolean jj_3R_116() { + if (jj_3R_53()) return true; + if (jj_3R_33()) return true; return false; } - static final private boolean jj_3R_124() { + static final private boolean jj_3R_110() { + if (jj_scan_token(RMIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_119() { - if (jj_scan_token(MAX)) return true; + static final private boolean jj_3R_124() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; @@ -2981,49 +2955,36 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_66() { - if (jj_scan_token(TIMES)) return true; + static final private boolean jj_3R_56() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_64()) { + jj_scanpos = xsp; + if (jj_3R_65()) return true; + } return false; } - static final private boolean jj_3R_118() { - if (jj_scan_token(MIN)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static final private boolean jj_3R_123() { + if (jj_3R_53()) return true; + if (jj_3R_33()) return true; return false; } - static final private boolean jj_3R_117() { + static final private boolean jj_3R_119() { + if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_57() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_66()) { - jj_scanpos = xsp; - if (jj_3R_67()) return true; - } - if (jj_3R_56()) return true; - return false; - } - - static final private boolean jj_3_6() { - if (jj_scan_token(OR)) return true; - if (jj_scan_token(OR)) return true; - return false; - } - - static final private boolean jj_3R_123() { - if (jj_3R_53()) return true; - if (jj_3R_33()) return true; + static final private boolean jj_3R_66() { + if (jj_scan_token(TIMES)) return true; return false; } - static final private boolean jj_3R_103() { - if (jj_scan_token(PMAX)) return true; + static final private boolean jj_3R_118() { + if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; @@ -3048,8 +3009,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_102() { - if (jj_scan_token(PMIN)) return true; + static final private boolean jj_3R_117() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; @@ -3073,6 +3033,37 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_57() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_66()) { + jj_scanpos = xsp; + if (jj_3R_67()) return true; + } + if (jj_3R_56()) return true; + return false; + } + + static final private boolean jj_3_6() { + if (jj_scan_token(OR)) return true; + if (jj_scan_token(OR)) return true; + return false; + } + + static final private boolean jj_3R_103() { + if (jj_scan_token(PMAX)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + + static final private boolean jj_3R_102() { + if (jj_scan_token(PMIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + static final private boolean jj_3R_101() { if (jj_scan_token(P)) return true; Token xsp; @@ -3145,16 +3136,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_94() { - if (jj_3R_99()) return true; - return false; - } - - static final private boolean jj_3R_93() { - if (jj_3R_98()) return true; - return false; - } - static final private boolean jj_3R_107() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -3167,6 +3148,16 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_94() { + if (jj_3R_99()) return true; + return false; + } + + static final private boolean jj_3R_93() { + if (jj_3R_98()) return true; + return false; + } + static final private boolean jj_3R_92() { if (jj_3R_97()) return true; return false; @@ -3182,11 +3173,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_91() { - if (jj_3R_27()) return true; - return false; - } - static final private boolean jj_3R_98() { if (jj_scan_token(S)) return true; Token xsp; @@ -3203,6 +3189,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_91() { + if (jj_3R_27()) return true; + return false; + } + static final private boolean jj_3R_80() { Token xsp; xsp = jj_scanpos; @@ -3231,6 +3222,21 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_149() { + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_33()) return true; + if (jj_scan_token(COMMA)) return true; + if (jj_3R_33()) return true; + if (jj_scan_token(RBRACKET)) return true; + return false; + } + + static final private boolean jj_3R_148() { + if (jj_scan_token(GE)) return true; + if (jj_3R_33()) return true; + return false; + } + static final private boolean jj_3R_46() { if (jj_3R_48()) return true; Token xsp; @@ -3241,18 +3247,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_146() { - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_33()) return true; - if (jj_scan_token(COMMA)) return true; + static final private boolean jj_3R_147() { + if (jj_scan_token(LE)) return true; if (jj_3R_33()) return true; - if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3R_145() { - if (jj_scan_token(GE)) return true; - if (jj_3R_33()) return true; + static final private boolean jj_3R_142() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_147()) { + jj_scanpos = xsp; + if (jj_3R_148()) { + jj_scanpos = xsp; + if (jj_3R_149()) return true; + } + } return false; } @@ -3270,25 +3280,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_144() { - if (jj_scan_token(LE)) return true; - if (jj_3R_33()) return true; - return false; - } - - static final private boolean jj_3R_139() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_144()) { - jj_scanpos = xsp; - if (jj_3R_145()) { - jj_scanpos = xsp; - if (jj_3R_146()) return true; - } - } - return false; - } - static final private boolean jj_3R_90() { if (jj_scan_token(MAX)) return true; return false; @@ -3362,6 +3353,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_63() { + if (jj_scan_token(LE)) return true; + return false; + } + static final private boolean jj_3R_41() { Token xsp; xsp = jj_scanpos; @@ -3372,11 +3368,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_63() { - if (jj_scan_token(LE)) return true; - return false; - } - static final private boolean jj_3R_62() { if (jj_scan_token(GE)) return true; return false; @@ -3408,13 +3399,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_87() { - if (jj_scan_token(MAX)) return true; + static final private boolean jj_3R_146() { + if (jj_3R_33()) return true; return false; } - static final private boolean jj_3R_143() { - if (jj_3R_33()) return true; + static final private boolean jj_3R_87() { + if (jj_scan_token(MAX)) return true; return false; } @@ -3424,31 +3415,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_39() { - if (jj_3R_41()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_42()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3_3() { - if (jj_scan_token(LABEL)) return true; - return false; - } - - static final private boolean jj_3R_88() { - if (jj_3R_33()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_96()) { jj_scanpos = xsp; break; } - } - return false; - } - static final private boolean jj_3R_55() { if (jj_scan_token(NE)) return true; return false; @@ -3469,11 +3435,36 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_39() { + if (jj_3R_41()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_42()) { jj_scanpos = xsp; break; } + } + return false; + } + static final private boolean jj_3R_115() { if (jj_scan_token(INIT)) return true; return false; } + static final private boolean jj_3_3() { + if (jj_scan_token(LABEL)) return true; + return false; + } + + static final private boolean jj_3R_88() { + if (jj_3R_33()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_96()) { jj_scanpos = xsp; break; } + } + return false; + } + static final private boolean jj_3_2() { if (jj_scan_token(LABEL)) return true; if (jj_scan_token(DQUOTE)) return true; @@ -3514,13 +3505,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_5() { - if (jj_scan_token(DQUOTE)) return true; + static final private boolean jj_3R_32() { + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } - static final private boolean jj_3R_32() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + static final private boolean jj_3R_141() { + if (jj_scan_token(R)) return true; + return false; + } + + static final private boolean jj_3R_140() { + if (jj_scan_token(W)) return true; return false; } @@ -3529,12 +3525,32 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_139() { + if (jj_scan_token(U)) return true; + return false; + } + + static final private boolean jj_3_5() { + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static final private boolean jj_3R_134() { + if (jj_scan_token(G)) return true; + return false; + } + static final private boolean jj_3R_38() { if (jj_scan_token(IMPLIES)) return true; if (jj_3R_37()) return true; return false; } + static final private boolean jj_3R_133() { + if (jj_scan_token(F)) return true; + return false; + } + static final private boolean jj_3R_35() { if (jj_3R_37()) return true; Token xsp; @@ -3550,13 +3566,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_134() { - if (jj_scan_token(G)) return true; + static final private boolean jj_3R_27() { + if (jj_scan_token(REG_IDENT)) return true; return false; } - static final private boolean jj_3R_133() { - if (jj_scan_token(F)) return true; + static final private boolean jj_3R_136() { + if (jj_3R_33()) return true; return false; } @@ -3573,19 +3589,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_132() { - if (jj_3R_33()) return true; - if (jj_scan_token(U)) return true; - return false; - } - - static final private boolean jj_3R_27() { - if (jj_scan_token(REG_IDENT)) return true; + static final private boolean jj_3R_135() { + if (jj_3R_142()) return true; return false; } - static final private boolean jj_3R_136() { + static final private boolean jj_3R_132() { if (jj_3R_33()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_139()) { + jj_scanpos = xsp; + if (jj_3R_140()) { + jj_scanpos = xsp; + if (jj_3R_141()) return true; + } + } return false; } @@ -3594,11 +3613,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_135() { - if (jj_3R_139()) return true; - return false; - } - static final private boolean jj_3R_36() { if (jj_scan_token(QMARK)) return true; if (jj_3R_35()) return true; @@ -3622,14 +3636,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_76() { - if (jj_3R_27()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_85()) jj_scanpos = xsp; - return false; - } - static final private boolean jj_3R_100() { if (jj_scan_token(DQUOTE)) return true; Token xsp; @@ -3642,11 +3648,44 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_76() { + if (jj_3R_27()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_85()) jj_scanpos = xsp; + return false; + } + static final private boolean jj_3R_113() { if (jj_3R_121()) return true; return false; } + static final private boolean jj_3_9() { + if (jj_scan_token(DQUOTE)) return true; + return false; + } + + static final private boolean jj_3R_120() { + Token xsp; + xsp = jj_scanpos; + 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()) return true; + } + } + } + xsp = jj_scanpos; + if (jj_3R_135()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_136()) jj_scanpos = xsp; + return false; + } + static private boolean jj_initialized_once = false; static public PrismParserTokenManager token_source; static SimpleCharStream jj_input_stream; @@ -3657,7 +3696,7 @@ public class PrismParser implements PrismParserConstants { static public boolean lookingAhead = false; static private boolean jj_semLA; static private int jj_gen; - static final private int[] jj_la1 = new int[77]; + static final private int[] jj_la1 = new int[78]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; @@ -3667,13 +3706,13 @@ public class PrismParser implements PrismParserConstants { jj_la1_2(); } private static void jj_la1_0() { - jj_la1_0 = new int[] {0x154a4130,0x11424130,0x4080000,0xe2c0a010,0x0,0xe2c0a010,0xe2c0a010,0x0,0xe2c0a010,0x11000120,0x200088,0x200088,0x0,0x10,0x0,0x80000,0x80000,0x8,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x2800000,0x2800000,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0xe280a000,0x0,0x2800000,0x2800000,0x0,0x2000,0xe0000000,0x2800000,0xe0000000,0x0,0x0,0x2800000,0xea85a000,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x2800000,0x0,0x0,0xe280a000,0x110040,0x80000,0x0,0x0,0x0,}; + jj_la1_0 = new int[] {0x154a4130,0x11424130,0x4080000,0xe2c0a010,0x0,0xe2c0a010,0xe2c0a010,0x0,0xe2c0a010,0x11000120,0x200088,0x200088,0x0,0x10,0x0,0x80000,0x80000,0x8,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x2800000,0x2800000,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0xe280a000,0x0,0x2800000,0x2800000,0x0,0x2000,0xe0000000,0x2800000,0xe0000000,0x0,0x0,0x2800000,0x0,0xea85a000,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x2800000,0x0,0x0,0xe280a000,0x110040,0x80000,0x0,0x0,0x0,}; } private static void jj_la1_1() { - jj_la1_1 = new int[] {0x30f,0x107,0x208,0x2014f6,0x40000,0x2014f6,0x2014f6,0x40000,0x2014f6,0x101,0x0,0x0,0x6,0x6,0x8000000,0x0,0x0,0x800000,0x0,0x800000,0x0,0x0,0x2014f0,0x2000,0x200400,0x80000,0x0,0x0,0xa014f0,0x0,0x800000,0x80000,0x2000000,0x80000,0x80000,0x2000000,0x200000,0x0,0x8000,0x4000,0x2000,0x2014f0,0x18000000,0xe0000000,0x0,0x0,0x0,0x0,0x2004f0,0x2004f0,0x200000,0x0,0x0,0x80000,0x400,0xf0,0xe8000000,0x0,0x2000000,0x2000000,0x0,0x2014f0,0x80800000,0x2014f0,0x80800000,0xe8000000,0x2000000,0x2000000,0xe8000000,0x70,0x2000000,0x2014f0,0x80,0x0,0x18000000,0xe0000000,0x20000,}; + jj_la1_1 = new int[] {0x30f,0x107,0x208,0x4024f6,0x80000,0x4024f6,0x4024f6,0x80000,0x4024f6,0x101,0x0,0x0,0x6,0x6,0x10000000,0x0,0x0,0x1000000,0x0,0x1000000,0x0,0x0,0x4024f0,0x4000,0x400400,0x100000,0x0,0x0,0x14024f0,0x0,0x1000000,0x100000,0x4000000,0x100000,0x100000,0x4000000,0x400000,0x0,0x10000,0x8000,0x4000,0x4024f0,0x30000000,0xc0000000,0x0,0x0,0x0,0x0,0x4004f0,0x4004f0,0x400000,0x0,0x0,0x100000,0x400,0xf0,0xd0000000,0x0,0x4000000,0x4000000,0x0,0x1840,0x4024f0,0x1000000,0x4024f0,0x1000000,0xd0000000,0x4000000,0x4000000,0xd0000000,0x70,0x4000000,0x4024f0,0x80,0x0,0x30000000,0xc0000000,0x40000,}; } private static void jj_la1_2() { - jj_la1_2 = new int[] {0x0,0x0,0x0,0x1704,0x0,0x1704,0x1704,0x0,0x1704,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1000,0x0,0x1000,0x2,0x1704,0x0,0x0,0x0,0x1000,0x1000,0x1704,0x1000,0x0,0x0,0x10,0x0,0x0,0x10,0x1000,0x80,0x0,0x0,0x0,0x1704,0x0,0x1,0x6,0x6,0x18,0x18,0x1704,0x1700,0x0,0x0,0x1000,0x0,0x600,0x100,0x1,0x0,0x0,0x0,0x0,0x1704,0x1,0x1704,0x1,0x1,0x0,0x0,0x1,0x0,0x0,0x1704,0x0,0x1000,0x0,0x1,0x0,}; + jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08,0x0,0x2e08,0x2e08,0x0,0x2e08,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x2000,0x0,0x2000,0x4,0x2e08,0x0,0x0,0x0,0x2000,0x2000,0x2e08,0x2000,0x0,0x0,0x20,0x0,0x0,0x20,0x2000,0x100,0x0,0x0,0x0,0x2e08,0x0,0x3,0xc,0xc,0x30,0x30,0x2e08,0x2e00,0x0,0x0,0x2000,0x0,0xc00,0x200,0x3,0x0,0x0,0x0,0x0,0x0,0x2e08,0x3,0x2e08,0x3,0x3,0x0,0x0,0x3,0x0,0x0,0x2e08,0x0,0x2000,0x0,0x3,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[9]; static private boolean jj_rescan = false; @@ -3695,7 +3734,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3708,7 +3747,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3725,7 +3764,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3735,7 +3774,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3751,7 +3790,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3760,7 +3799,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 77; i++) jj_la1[i] = -1; + for (int i = 0; i < 78; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -3871,15 +3910,15 @@ public class PrismParser implements PrismParserConstants { static public ParseException generateParseException() { jj_expentries.removeAllElements(); - boolean[] la1tokens = new boolean[79]; - for (int i = 0; i < 79; i++) { + boolean[] la1tokens = new boolean[80]; + for (int i = 0; i < 80; i++) { la1tokens[i] = false; } if (jj_kind >= 0) { la1tokens[jj_kind] = true; jj_kind = -1; } - for (int i = 0; i < 77; i++) { + for (int i = 0; i < 78; i++) { if (jj_la1[i] == jj_gen) { for (int j = 0; j < 32; j++) { if ((jj_la1_0[i] & (1< | < TRUE: "true" > | < U: "U" > +| < W: "W" > // Punctuation, etc. // Note that "NOT" must be the first item of punctuation in this list // (PrismSyntaxHighlighter relies on this fact) @@ -1314,7 +1315,7 @@ PathExpression ExpressionProbContents() : { return pe; } } -// Temporal operarors (X, U, F, G) +// Temporal operarors (X, U, F, G, W, R) PathExpression PathExpressionTemporal() : { @@ -1328,7 +1329,11 @@ PathExpression PathExpressionTemporal() : { begin = getToken(0); } ( { pe.setOperator(PathExpressionTemporal.P_X); } - | expr1 = Expression() { pe.setOperator(PathExpressionTemporal.P_U); } + | ( expr1 = Expression() + ( { pe.setOperator(PathExpressionTemporal.P_U); } + | { pe.setOperator(PathExpressionTemporal.P_W); } + | { pe.setOperator(PathExpressionTemporal.P_R); } ) + ) | { pe.setOperator(PathExpressionTemporal.P_F); } | { pe.setOperator(PathExpressionTemporal.P_G); } ) diff --git a/prism/src/parser/PrismParserConstants.java b/prism/src/parser/PrismParserConstants.java index 62063283..65a03e88 100644 --- a/prism/src/parser/PrismParserConstants.java +++ b/prism/src/parser/PrismParserConstants.java @@ -47,41 +47,42 @@ public interface PrismParserConstants { int SYSTEM = 41; int TRUE = 42; int U = 43; - int NOT = 44; - int AND = 45; - int OR = 46; - int IMPLIES = 47; - int RARROW = 48; - int COLON = 49; - int SEMICOLON = 50; - int COMMA = 51; - int DOTS = 52; - int LPARENTH = 53; - int RPARENTH = 54; - int LBRACKET = 55; - int RBRACKET = 56; - int LBRACE = 57; - int RBRACE = 58; - int EQ = 59; - int NE = 60; - int LT = 61; - int GT = 62; - int LE = 63; - int GE = 64; - int PLUS = 65; - int MINUS = 66; - int TIMES = 67; - int DIVIDE = 68; - int PRIME = 69; - int RENAME = 70; - int QMARK = 71; - int DQUOTE = 72; - int REG_INT = 73; - int REG_DOUBLE = 74; - int REG_IDENTPRIME = 75; - int REG_IDENT = 76; - int PREPROC = 77; - int LEXICAL_ERROR = 78; + int W = 44; + int NOT = 45; + int AND = 46; + int OR = 47; + int IMPLIES = 48; + int RARROW = 49; + int COLON = 50; + int SEMICOLON = 51; + int COMMA = 52; + int DOTS = 53; + int LPARENTH = 54; + int RPARENTH = 55; + int LBRACKET = 56; + int RBRACKET = 57; + int LBRACE = 58; + int RBRACE = 59; + int EQ = 60; + int NE = 61; + int LT = 62; + int GT = 63; + int LE = 64; + int GE = 65; + int PLUS = 66; + int MINUS = 67; + int TIMES = 68; + int DIVIDE = 69; + int PRIME = 70; + int RENAME = 71; + int QMARK = 72; + int DQUOTE = 73; + int REG_INT = 74; + int REG_DOUBLE = 75; + int REG_IDENTPRIME = 76; + int REG_IDENT = 77; + int PREPROC = 78; + int LEXICAL_ERROR = 79; int DEFAULT = 0; @@ -130,6 +131,7 @@ public interface PrismParserConstants { "\"system\"", "\"true\"", "\"U\"", + "\"W\"", "\"!\"", "\"&\"", "\"|\"", diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index 36da6d75..3e65f62a 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -14,22 +14,22 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac switch (pos) { case 0: - if ((active0 & 0x8f0e8150040L) != 0L) + if ((active0 & 0x18f0e8150040L) != 0L) return 23; + if ((active1 & 0x20L) != 0L) + return 1; + if ((active0 & 0x20000000000000L) != 0L) + return 11; if ((active0 & 0x70f17eaffb8L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; return 23; } - if ((active1 & 0x10L) != 0L) - return 1; - if ((active0 & 0x10000000000000L) != 0L) - return 11; return -1; case 1: if ((active0 & 0x73f77eaffb8L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 1; return 23; } @@ -39,7 +39,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x73f744affb8L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 2; return 23; } @@ -51,7 +51,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac { if (jjmatchedPos != 3) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 3; } return 23; @@ -62,7 +62,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x30914025e80L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 4; return 23; } @@ -72,7 +72,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x10910005e00L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 5; return 23; } @@ -82,7 +82,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x10110001c00L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 6; return 23; } @@ -90,7 +90,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac case 7: if ((active0 & 0x10110001c00L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 7; return 23; } @@ -100,7 +100,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x10110000800L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 8; return 23; } @@ -110,7 +110,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac return 23; if ((active0 & 0x110000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 9; return 23; } @@ -118,7 +118,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac case 10: if ((active0 & 0x110000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 10; return 23; } @@ -126,25 +126,25 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac case 11: if ((active0 & 0x110000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 11; return 23; } return -1; case 12: + if ((active0 & 0x100000000L) != 0L) + return 23; if ((active0 & 0x10000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 12; return 23; } - if ((active0 & 0x100000000L) != 0L) - return 23; return -1; case 13: if ((active0 & 0x10000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 13; return 23; } @@ -152,7 +152,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac case 14: if ((active0 & 0x10000000L) != 0L) { - jjmatchedKind = 76; + jjmatchedKind = 77; jjmatchedPos = 14; return 23; } @@ -184,46 +184,46 @@ static private final int jjMoveStringLiteralDfa0_0() switch(curChar) { case 33: - jjmatchedKind = 44; - return jjMoveStringLiteralDfa1_0(0x1000000000000000L, 0x0L); + jjmatchedKind = 45; + return jjMoveStringLiteralDfa1_0(0x2000000000000000L, 0x0L); case 34: - return jjStopAtPos(0, 72); + return jjStopAtPos(0, 73); case 38: - return jjStopAtPos(0, 45); + return jjStopAtPos(0, 46); case 39: - return jjStopAtPos(0, 69); + return jjStopAtPos(0, 70); case 40: - return jjStopAtPos(0, 53); - case 41: return jjStopAtPos(0, 54); + case 41: + return jjStopAtPos(0, 55); case 42: - return jjStopAtPos(0, 67); + return jjStopAtPos(0, 68); case 43: - return jjStopAtPos(0, 65); + return jjStopAtPos(0, 66); case 44: - return jjStopAtPos(0, 51); + return jjStopAtPos(0, 52); case 45: - jjmatchedKind = 66; - return jjMoveStringLiteralDfa1_0(0x1000000000000L, 0x0L); + jjmatchedKind = 67; + return jjMoveStringLiteralDfa1_0(0x2000000000000L, 0x0L); case 46: - return jjMoveStringLiteralDfa1_0(0x10000000000000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x20000000000000L, 0x0L); case 47: - return jjStartNfaWithStates_0(0, 68, 1); + return jjStartNfaWithStates_0(0, 69, 1); case 58: - return jjStopAtPos(0, 49); - case 59: return jjStopAtPos(0, 50); + case 59: + return jjStopAtPos(0, 51); case 60: - jjmatchedKind = 61; - return jjMoveStringLiteralDfa1_0(0x8000000000000000L, 0x40L); + jjmatchedKind = 62; + return jjMoveStringLiteralDfa1_0(0x0L, 0x81L); case 61: - jjmatchedKind = 59; - return jjMoveStringLiteralDfa1_0(0x800000000000L, 0x0L); + jjmatchedKind = 60; + return jjMoveStringLiteralDfa1_0(0x1000000000000L, 0x0L); case 62: - jjmatchedKind = 62; - return jjMoveStringLiteralDfa1_0(0x0L, 0x1L); + jjmatchedKind = 63; + return jjMoveStringLiteralDfa1_0(0x0L, 0x2L); case 63: - return jjStopAtPos(0, 71); + return jjStopAtPos(0, 72); case 67: return jjStartNfaWithStates_0(0, 6, 23); case 70: @@ -242,12 +242,14 @@ static private final int jjMoveStringLiteralDfa0_0() return jjStartNfaWithStates_0(0, 39, 23); case 85: return jjStartNfaWithStates_0(0, 43, 23); + case 87: + return jjStartNfaWithStates_0(0, 44, 23); case 88: return jjStartNfaWithStates_0(0, 27, 23); case 91: - return jjStopAtPos(0, 55); - case 93: return jjStopAtPos(0, 56); + case 93: + return jjStopAtPos(0, 57); case 98: return jjMoveStringLiteralDfa1_0(0x8L, 0x0L); case 99: @@ -277,11 +279,11 @@ static private final int jjMoveStringLiteralDfa0_0() case 116: return jjMoveStringLiteralDfa1_0(0x40000000000L, 0x0L); case 123: - return jjStopAtPos(0, 57); + return jjStopAtPos(0, 58); case 124: - return jjStopAtPos(0, 46); + return jjStopAtPos(0, 47); case 125: - return jjStopAtPos(0, 58); + return jjStopAtPos(0, 59); default : return jjMoveNfa_0(0, 0); } @@ -296,26 +298,26 @@ static private final int jjMoveStringLiteralDfa1_0(long active0, long active1) switch(curChar) { case 45: - if ((active1 & 0x40L) != 0L) - return jjStopAtPos(1, 70); + if ((active1 & 0x80L) != 0L) + return jjStopAtPos(1, 71); break; case 46: - if ((active0 & 0x10000000000000L) != 0L) - return jjStopAtPos(1, 52); + if ((active0 & 0x20000000000000L) != 0L) + return jjStopAtPos(1, 53); break; case 61: - if ((active0 & 0x1000000000000000L) != 0L) - return jjStopAtPos(1, 60); - else if ((active0 & 0x8000000000000000L) != 0L) - return jjStopAtPos(1, 63); + if ((active0 & 0x2000000000000000L) != 0L) + return jjStopAtPos(1, 61); else if ((active1 & 0x1L) != 0L) return jjStopAtPos(1, 64); + else if ((active1 & 0x2L) != 0L) + return jjStopAtPos(1, 65); break; case 62: - if ((active0 & 0x800000000000L) != 0L) - return jjStopAtPos(1, 47); - else if ((active0 & 0x1000000000000L) != 0L) + if ((active0 & 0x1000000000000L) != 0L) return jjStopAtPos(1, 48); + else if ((active0 & 0x2000000000000L) != 0L) + return jjStopAtPos(1, 49); break; case 97: return jjMoveStringLiteralDfa2_0(active0, 0x400c02000L, active1, 0L); @@ -840,14 +842,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 23: if ((0x3ff000000000000L & l) != 0L) { - if (kind > 76) - kind = 76; + if (kind > 77) + kind = 77; jjCheckNAdd(22); } else if (curChar == 39) { - if (kind > 75) - kind = 75; + if (kind > 76) + kind = 76; } if ((0x3ff000000000000L & l) != 0L) jjCheckNAddTwoStates(20, 21); @@ -855,8 +857,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 0: if ((0x3ff000000000000L & l) != 0L) { - if (kind > 74) - kind = 74; + if (kind > 75) + kind = 75; jjCheckNAddStates(0, 3); } else if ((0x100002600L & l) != 0L) @@ -872,14 +874,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjstateSet[jjnewStateCnt++] = 1; if ((0x3fe000000000000L & l) != 0L) { - if (kind > 73) - kind = 73; + if (kind > 74) + kind = 74; jjCheckNAdd(8); } else if (curChar == 48) { - if (kind > 73) - kind = 73; + if (kind > 74) + kind = 74; } break; case 1: @@ -909,20 +911,20 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 7: if ((0x3fe000000000000L & l) == 0L) break; - if (kind > 73) - kind = 73; + if (kind > 74) + kind = 74; jjCheckNAdd(8); break; case 8: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 73) - kind = 73; + if (kind > 74) + kind = 74; jjCheckNAdd(8); break; case 9: - if (curChar == 48 && kind > 73) - kind = 73; + if (curChar == 48 && kind > 74) + kind = 74; break; case 10: if (curChar == 46) @@ -931,8 +933,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 11: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 74) - kind = 74; + if (kind > 75) + kind = 75; jjCheckNAddTwoStates(11, 12); break; case 13: @@ -942,8 +944,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 14: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 74) - kind = 74; + if (kind > 75) + kind = 75; jjCheckNAdd(14); break; case 15: @@ -955,14 +957,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjCheckNAddTwoStates(16, 17); break; case 17: - if (curChar == 35 && kind > 77) - kind = 77; + if (curChar == 35 && kind > 78) + kind = 78; break; case 18: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 74) - kind = 74; + if (kind > 75) + kind = 75; jjCheckNAddStates(0, 3); break; case 20: @@ -970,14 +972,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjCheckNAddTwoStates(20, 21); break; case 21: - if (curChar == 39 && kind > 75) - kind = 75; + if (curChar == 39 && kind > 76) + kind = 76; break; case 22: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 76) - kind = 76; + if (kind > 77) + kind = 77; jjCheckNAdd(22); break; default : break; @@ -994,8 +996,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 23: if ((0x7fffffe87fffffeL & l) != 0L) { - if (kind > 76) - kind = 76; + if (kind > 77) + kind = 77; jjCheckNAdd(22); } if ((0x7fffffe87fffffeL & l) != 0L) @@ -1004,8 +1006,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 0: if ((0x7fffffe87fffffeL & l) == 0L) break; - if (kind > 76) - kind = 76; + if (kind > 77) + kind = 77; jjCheckNAddStates(7, 9); break; case 2: @@ -1025,8 +1027,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 22: if ((0x7fffffe87fffffeL & l) == 0L) break; - if (kind > 76) - kind = 76; + if (kind > 77) + kind = 77; jjCheckNAdd(22); break; default : break; @@ -1080,15 +1082,16 @@ public static final String[] jjstrLiteralImages = { "\156\157\156\144\145\164\145\162\155\151\156\151\163\164\151\143", "\120\155\141\170", "\120\155\151\156", "\120", "\160\162\157\142\141\142\151\154\151\163\164\151\143", "\160\162\157\142", "\162\141\164\145", "\162\145\167\141\162\144\163", "\122\155\141\170", "\122\155\151\156", "\122", "\123", -"\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\41", "\46", "\174", -"\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133", "\135", "\173", -"\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53", "\55", "\52", "\57", -"\47", "\74\55", "\77", "\42", null, null, null, null, null, null, }; +"\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\127", "\41", "\46", +"\174", "\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133", +"\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53", +"\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, null, +null, }; public static final String[] lexStateNames = { "DEFAULT", }; static final long[] jjtoToken = { - 0xfffffffffffffff9L, 0x7fffL, + 0xfffffffffffffff9L, 0xffffL, }; static final long[] jjtoSkip = { 0x6L, 0x0L, @@ -1181,9 +1184,9 @@ public static Token getNextToken() jjmatchedKind = 0x7fffffff; jjmatchedPos = 0; curPos = jjMoveStringLiteralDfa0_0(); - if (jjmatchedPos == 0 && jjmatchedKind > 78) + if (jjmatchedPos == 0 && jjmatchedKind > 79) { - jjmatchedKind = 78; + jjmatchedKind = 79; } if (jjmatchedKind != 0x7fffffff) { diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 4a40a8a8..9c25a359 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -164,6 +164,10 @@ public abstract class Expression extends ASTElement public static Expression Int(int i) { return new ExpressionLiteral(Expression.INT, i); } public static Expression Double(double d) { return new ExpressionLiteral(Expression.DOUBLE, d); } public static Expression Not(Expression expr) { return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr); } + public static Expression And(Expression expr1, Expression expr2) + { return new ExpressionBinaryOp(ExpressionBinaryOp.AND, expr1, expr2); } + public static Expression Or(Expression expr1, Expression expr2) + { return new ExpressionBinaryOp(ExpressionBinaryOp.OR, expr1, expr2); } public static Expression Parenth(Expression expr) { return new ExpressionUnaryOp(ExpressionUnaryOp.PARENTH, expr); } } diff --git a/prism/src/parser/ast/PathExpressionTemporal.java b/prism/src/parser/ast/PathExpressionTemporal.java index f89f68ff..4d5f2228 100644 --- a/prism/src/parser/ast/PathExpressionTemporal.java +++ b/prism/src/parser/ast/PathExpressionTemporal.java @@ -36,13 +36,15 @@ public class PathExpressionTemporal extends PathExpression public static final int P_U = 2; // Until (for P operator) public static final int P_F = 3; // Future (for P operator) public static final int P_G = 4; // Globally (for P operator) + public static final int P_W = 5; // Weak until (for P operator) + public static final int P_R = 6; // Release (for P operator) public static final int R_C = 11; // Cumulative (for R operator) public static final int R_I = 12; // Instantaneous (for R operator) public static final int R_F = 13; // Reachability (for R operator) public static final int R_S = 14; // Steady-state (for R operator) // Operator symbols public static final String opSymbols[] = { "", - "X", "U", "F", "G", "", "", "", "", "", "", + "X", "U", "F", "G", "W", "", "", "", "", "", "C", "I", "F", "S" }; @@ -199,12 +201,12 @@ public class PathExpressionTemporal extends PathExpression // Other useful methods /** - * Convert (P operator) path formula to until form - * (using standard equivalences: F a=true U a, G a=!(true U!a) + * Convert (P operator) path formula to untils, using standard equivalences. */ public PathExpression convertToUntilForm() throws PrismLangException { PathExpression op1, op2, ret = null; + Expression a, b; if (operand1 != null && !(operand1 instanceof PathExpressionExpr)) { throw new PrismLangException("Cannot convert "+getOperatorSymbol()+" to until form"); } @@ -216,15 +218,35 @@ public class PathExpressionTemporal extends PathExpression ret = this; break; case P_F: + // F a == true U a op1 = new PathExpressionExpr(Expression.True()); ret = new PathExpressionTemporal(P_U, op1, operand2, lBound, uBound); break; case P_G: + // G a == !(true U !a) op1 = new PathExpressionExpr(Expression.True()); op2 = new PathExpressionExpr(Expression.Not(((PathExpressionExpr)operand2).getExpression())); ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound); ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret); break; + case P_W: + // a W b == !(a&!b U !a&!b) + a = ((PathExpressionExpr)operand1).getExpression(); + b = ((PathExpressionExpr)operand2).getExpression(); + op1 = new PathExpressionExpr(Expression.And(a, Expression.Not(b))); + op2 = new PathExpressionExpr(Expression.And(Expression.Not(a), Expression.Not(b))); + ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound); + ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret); + break; + case P_R: + // a R b == !(!a U !b) + a = ((PathExpressionExpr)operand1).getExpression(); + b = ((PathExpressionExpr)operand2).getExpression(); + op1 = new PathExpressionExpr(Expression.Not(a)); + op2 = new PathExpressionExpr(Expression.Not(b)); + ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound); + ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret); + break; default: throw new PrismLangException("Cannot convert "+getOperatorSymbol()+" to until form"); } diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index f3a22ce1..dee60f1a 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -406,6 +406,8 @@ public class TypeCheck extends ASTTraverse case PathExpressionTemporal.P_U: case PathExpressionTemporal.P_F: case PathExpressionTemporal.P_G: + case PathExpressionTemporal.P_W: + case PathExpressionTemporal.P_R: e.setType(Expression.BOOLEAN); break; case PathExpressionTemporal.R_C: