From 234fe87e310297572d4bb482e2db58c46123a379 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 20 Jul 2015 10:28:09 +0000 Subject: [PATCH] Fix parser tweak from previous commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10364 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 463 ++++++++++++++++-------------- prism/src/parser/PrismParser.jj | 23 +- 2 files changed, 261 insertions(+), 225 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 30be8a49..7de84f1a 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -2864,16 +2864,9 @@ public class PrismParser implements PrismParserConstants { // Contents of an R operator -// JavaCC warns about lookahead for this function. This is because there is a -// conflict between R [ S ], where "S" is the long-run reward operator, and -// R [ S [ ] ] where "S [ ]" is a treated as an LTL formula comprising a single -// atomic proposition which is a nested S operator. Both are technically valid. - -// (bounded temporal operators and semicolon-less properties files) -// (see the relevant productions for details) -// we allow two or more successive expressions resulting in potential ambiguities -// e.g. "-a-b" = "(-a)-b" = "-a" "-b" -// Ignoring the warning results in the largest match being taken. +// JavaCC warns about lookahead for this function. This is because there is a possible conflict between +// R [ S ], where "S" is the long-run reward operator, and R [ S [ ] ], where "S [ ]" is an LTL formula +// comprising a single atomic proposition. We use lookahead to resolve the ambiguity. static final public Expression ExpressionRewardContents(boolean prop, boolean pathprop) throws ParseException { Expression expr = null; ExpressionTemporal exprTemp = null; @@ -2881,33 +2874,69 @@ public class PrismParser implements PrismParserConstants { Token begin; begin = getToken(1); if (jj_2_17(2147483647)) { - expr = Expression(prop, true); - ret = expr; - } else if (jj_2_18(2147483647)) { - begin = jj_consume_token(C); - jj_consume_token(LE); - expr = Expression(false, false); - exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; + expr = ExpressionSS(prop, true); + ret = expr; } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { - case C: - jj_consume_token(C); - ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); - break; - case I: - jj_consume_token(I); - jj_consume_token(EQ); - expr = Expression(false, false); - exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; - break; case S: jj_consume_token(S); ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); break; default: jj_la1[85] = jj_gen; - jj_consume_token(-1); - throw new ParseException(); + if (jj_2_18(2147483647)) { + begin = jj_consume_token(C); + jj_consume_token(LE); + expr = Expression(false, false); + exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; + } else { + switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case C: + jj_consume_token(C); + ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); + break; + case I: + jj_consume_token(I); + jj_consume_token(EQ); + expr = Expression(false, false); + exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; + break; + case A: + case E: + case FALSE: + case FILTER: + case FUNC: + case F: + case G: + case MAX: + case MIN: + case X: + case PMAX: + case PMIN: + case P: + case RMAX: + case RMIN: + case R: + case S: + case TRUE: + case NOT: + case LPARENTH: + case DLBRACKET: + case DLT: + case MINUS: + case DQUOTE: + case REG_INT: + case REG_DOUBLE: + case REG_IDENT: + expr = Expression(prop, true); + ret = expr; + break; + default: + jj_la1[86] = jj_gen; + jj_consume_token(-1); + throw new ParseException(); + } + } } } ret.setPosition(begin, getToken(0)); {if (true) return ret;} @@ -2964,7 +2993,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(DRBRACKET); break; default: - jj_la1[86] = jj_gen; + jj_la1[87] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2986,7 +3015,7 @@ public class PrismParser implements PrismParserConstants { expr = ExpressionFuncOrIdent(prop, pathprop); break; default: - jj_la1[87] = jj_gen; + jj_la1[88] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3012,7 +3041,7 @@ public class PrismParser implements PrismParserConstants { s = "init"; break; default: - jj_la1[88] = jj_gen; + jj_la1[89] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3057,7 +3086,7 @@ public class PrismParser implements PrismParserConstants { op = Identifier(); break; default: - jj_la1[89] = jj_gen; + jj_la1[90] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3069,7 +3098,7 @@ public class PrismParser implements PrismParserConstants { filter = Expression(prop, pathprop); break; default: - jj_la1[90] = jj_gen; + jj_la1[91] = jj_gen; ; } jj_consume_token(RPARENTH); @@ -3114,7 +3143,7 @@ public class PrismParser implements PrismParserConstants { ident="max"; break; default: - jj_la1[91] = jj_gen; + jj_la1[92] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3147,7 +3176,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.NE;} break; default: - jj_la1[92] = jj_gen; + jj_la1[93] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3174,7 +3203,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.LE;} break; default: - jj_la1[93] = jj_gen; + jj_la1[94] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3199,7 +3228,7 @@ public class PrismParser implements PrismParserConstants { step = Expression(false, false); break; default: - jj_la1[94] = jj_gen; + jj_la1[95] = jj_gen; ; } jj_consume_token(0); @@ -3672,6 +3701,12 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_188() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_37()) return true; + return false; + } + static private boolean jj_3R_50() { if (jj_scan_token(GT)) return true; return false; @@ -3693,12 +3728,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_188() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_37()) return true; - return false; - } - static private boolean jj_3R_163() { if (jj_3R_28()) return true; return false; @@ -3712,6 +3741,12 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_89() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_28()) return true; + return false; + } + static private boolean jj_3R_118() { if (jj_scan_token(NE)) return true; return false; @@ -3732,12 +3767,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_89() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_28()) return true; - return false; - } - static private boolean jj_3R_145() { if (jj_scan_token(LPARENTH)) return true; if (jj_3R_37()) return true; @@ -3750,11 +3779,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_47() { - if (jj_scan_token(REG_IDENTPRIME)) return true; - return false; - } - static private boolean jj_3R_156() { if (jj_scan_token(FALSE)) return true; return false; @@ -3765,13 +3789,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_37() { - if (jj_3R_45()) return true; + static private boolean jj_3R_47() { + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } - static private boolean jj_3R_185() { - if (jj_scan_token(OR)) return true; + static private boolean jj_3R_37() { + if (jj_3R_45()) return true; return false; } @@ -3780,6 +3804,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_185() { + if (jj_scan_token(OR)) return true; + return false; + } + static private boolean jj_3R_154() { if (jj_scan_token(REG_DOUBLE)) return true; return false; @@ -3796,11 +3825,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_31() { - if (jj_3R_28()) return true; - return false; - } - static private boolean jj_3R_78() { if (jj_scan_token(LPARENTH)) return true; if (jj_3R_30()) return true; @@ -3808,6 +3832,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_31() { + if (jj_3R_28()) return true; + return false; + } + static private boolean jj_3R_153() { if (jj_scan_token(REG_INT)) return true; return false; @@ -3836,16 +3865,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_184() { - if (jj_scan_token(AND)) return true; - return false; - } - - static private boolean jj_3R_182() { - if (jj_scan_token(MAX)) return true; - return false; - } - static private boolean jj_3R_76() { if (jj_3R_28()) return true; return false; @@ -3862,6 +3881,16 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_184() { + if (jj_scan_token(AND)) return true; + return false; + } + + static private boolean jj_3R_182() { + if (jj_scan_token(MAX)) return true; + return false; + } + static private boolean jj_3R_67() { Token xsp; xsp = jj_scanpos; @@ -3880,11 +3909,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_180() { - if (jj_scan_token(INIT)) return true; - return false; - } - static private boolean jj_3R_160() { if (jj_3R_37()) return true; Token xsp; @@ -3910,6 +3934,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_180() { + if (jj_scan_token(INIT)) return true; + return false; + } + static private boolean jj_3R_187() { if (jj_scan_token(COMMA)) return true; if (jj_3R_37()) return true; @@ -3981,11 +4010,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_176() { - if (jj_3R_147()) return true; - return false; - } - static private boolean jj_3R_79() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; @@ -4009,6 +4033,32 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_176() { + if (jj_3R_147()) return true; + return false; + } + + static private boolean jj_3R_57() { + if (jj_3R_67()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_68()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_158() { + if (jj_scan_token(MIN)) return true; + return false; + } + + 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_152() { if (jj_scan_token(FILTER)) return true; if (jj_scan_token(LPARENTH)) return true; @@ -4038,27 +4088,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_57() { - if (jj_3R_67()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_68()) { jj_scanpos = xsp; break; } - } - return false; - } - - static private boolean jj_3R_158() { - if (jj_scan_token(MIN)) return true; - return false; - } - - 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_143() { Token xsp; xsp = jj_scanpos; @@ -4100,6 +4129,14 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_142() { + if (jj_3R_28()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_157()) jj_scanpos = xsp; + return false; + } + static private boolean jj_3R_151() { if (jj_scan_token(DQUOTE)) return true; Token xsp; @@ -4112,14 +4149,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_142() { - if (jj_3R_28()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_157()) jj_scanpos = xsp; - return false; - } - static private boolean jj_3R_58() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -4148,29 +4177,23 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_177() { - if (jj_3R_145()) return true; - return false; - } - static private boolean jj_3R_139() { if (jj_3R_151()) return true; return false; } - static private boolean jj_3R_175() { - if (jj_3R_146()) return true; + static private boolean jj_3R_138() { + if (jj_3R_150()) return true; return false; } - static private boolean jj_3R_138() { - if (jj_3R_150()) return true; + static private boolean jj_3R_177() { + if (jj_3R_145()) return true; return false; } - static private boolean jj_3R_174() { - if (jj_scan_token(DLBRACKET)) return true; - if (jj_scan_token(DRBRACKET)) return true; + static private boolean jj_3R_175() { + if (jj_3R_146()) return true; return false; } @@ -4179,9 +4202,9 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_173() { - if (jj_scan_token(DLT)) return true; - if (jj_scan_token(DGT)) return true; + static private boolean jj_3R_174() { + if (jj_scan_token(DLBRACKET)) return true; + if (jj_scan_token(DRBRACKET)) return true; return false; } @@ -4195,16 +4218,32 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_210() { + static private boolean jj_3R_211() { if (jj_3R_37()) return true; return false; } + static private boolean jj_3R_173() { + if (jj_scan_token(DLT)) return true; + if (jj_scan_token(DGT)) return true; + return false; + } + static private boolean jj_3R_135() { if (jj_3R_147()) return true; return false; } + static private boolean jj_3R_134() { + if (jj_3R_32()) return true; + return false; + } + + static private boolean jj_3R_133() { + if (jj_3R_146()) return true; + return false; + } + static private boolean jj_3R_150() { Token xsp; xsp = jj_scanpos; @@ -4226,16 +4265,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_134() { - if (jj_3R_32()) return true; - return false; - } - - static private boolean jj_3R_133() { - if (jj_3R_146()) return true; - return false; - } - static private boolean jj_3R_132() { if (jj_3R_145()) return true; return false; @@ -4271,7 +4300,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_207() { + static private boolean jj_3R_208() { if (jj_3R_37()) return true; return false; } @@ -4353,14 +4382,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_148() { - if (jj_scan_token(E)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_37()) return true; - if (jj_scan_token(RBRACKET)) return true; - return false; - } - static private boolean jj_3R_119() { Token xsp; xsp = jj_scanpos; @@ -4371,14 +4392,16 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_125() { - if (jj_scan_token(TIMES)) return true; + static private boolean jj_3R_148() { + if (jj_scan_token(E)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_37()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static private boolean jj_3_18() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; + static private boolean jj_3R_125() { + if (jj_scan_token(TIMES)) return true; return false; } @@ -4398,11 +4421,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3_17() { - if (jj_3R_32()) return true; - return false; - } - static private boolean jj_3_7() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_28()) return true; @@ -4411,15 +4429,9 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_204() { - if (jj_scan_token(S)) return true; - return false; - } - - static private boolean jj_3R_203() { - if (jj_scan_token(I)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_37()) return true; + static private boolean jj_3_18() { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; return false; } @@ -4430,14 +4442,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_202() { - if (jj_scan_token(C)) return true; - return false; - } - - static private boolean jj_3R_201() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; + static private boolean jj_3R_205() { if (jj_3R_37()) return true; return false; } @@ -4452,12 +4457,31 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3_17() { + if (jj_3R_32()) return true; + return false; + } + + static private boolean jj_3R_204() { + if (jj_scan_token(I)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_37()) return true; + return false; + } + static private boolean jj_3_16() { if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_200() { + static private boolean jj_3R_203() { + if (jj_scan_token(C)) return true; + return false; + } + + static private boolean jj_3R_202() { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; if (jj_3R_37()) return true; return false; } @@ -4467,22 +4491,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_171() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_200()) { - jj_scanpos = xsp; - 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()) return true; - } - } - } - } + static private boolean jj_3R_201() { + if (jj_scan_token(S)) return true; return false; } @@ -4502,13 +4512,40 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_209() { + static private boolean jj_3R_200() { + if (jj_3R_32()) return true; + return false; + } + + static private boolean jj_3R_210() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_28()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } + static private boolean jj_3R_171() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_200()) { + jj_scanpos = xsp; + 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()) return true; + } + } + } + } + } + return false; + } + static private boolean jj_3_15() { if (jj_scan_token(DQUOTE)) return true; return false; @@ -4529,21 +4566,21 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_206() { + static private boolean jj_3R_207() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_28()) return true; if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_208() { + static private boolean jj_3R_209() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_209()) { + if (jj_3R_210()) { jj_scanpos = xsp; - if (jj_3R_210()) return true; + if (jj_3R_211()) return true; } if (jj_scan_token(RBRACE)) return true; return false; @@ -4555,17 +4592,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_205() { + static private boolean jj_3R_206() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_206()) { + if (jj_3R_207()) { jj_scanpos = xsp; - if (jj_3R_207()) return true; + if (jj_3R_208()) return true; } if (jj_scan_token(RBRACE)) return true; xsp = jj_scanpos; - if (jj_3R_208()) jj_scanpos = xsp; + if (jj_3R_209()) jj_scanpos = xsp; return false; } @@ -4633,7 +4670,7 @@ public class PrismParser implements PrismParserConstants { } static private boolean jj_3R_195() { - if (jj_3R_205()) return true; + if (jj_3R_206()) return true; return false; } @@ -4918,7 +4955,7 @@ public class PrismParser implements PrismParserConstants { static private Token jj_scanpos, jj_lastpos; static private int jj_la; static private int jj_gen; - static final private int[] jj_la1 = new int[95]; + static final private int[] jj_la1 = new int[96]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; @@ -4928,13 +4965,13 @@ public class PrismParser implements PrismParserConstants { jj_la1_init_2(); } private static void jj_la1_init_0() { - jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x4000100,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,}; + jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,}; } private static void jj_la1_init_1() { - jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x0,0x40003838,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,}; + jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x40003838,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,}; } private static void jj_la1_init_2() { - jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x404,0x2000000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,}; + jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x2e08404,0x404,0x2000000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[18]; static private boolean jj_rescan = false; @@ -4958,7 +4995,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4973,7 +5010,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4991,7 +5028,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5002,7 +5039,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5019,7 +5056,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5029,7 +5066,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 95; i++) jj_la1[i] = -1; + for (int i = 0; i < 96; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5146,7 +5183,7 @@ public class PrismParser implements PrismParserConstants { la1tokens[jj_kind] = true; jj_kind = -1; } - for (int i = 0; i < 95; i++) { + for (int i = 0; i < 96; i++) { if (jj_la1[i] == jj_gen) { for (int j = 0; j < 32; j++) { if ((jj_la1_0[i] & (1< { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } + + // Normal reward operators (excluding S; see above) | LOOKAHEAD( ) begin = expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } | { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); } | expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; } - | { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } + + // Path formula (including F "target") + | expr = Expression(prop, true) { ret = expr; } ) { ret.setPosition(begin, getToken(0)); return ret; } }