s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Fix parser tweak from previous commit. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10364 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
cfa767ec0d
commit
234fe87e31
2 changed files with 261 additions and 225 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 463
      prism/src/parser/PrismParser.java
  2. 23
      prism/src/parser/PrismParser.jj

463
prism/src/parser/PrismParser.java
View File

@ -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<<j)) != 0) {

23
prism/src/parser/PrismParser.jj
View File

@ -1629,12 +1629,9 @@ void RewardIndex(ExpressionReward exprRew) :
// Contents of an R operator
// (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.
Expression ExpressionRewardContents(boolean prop, boolean pathprop) :
{
@ -1646,15 +1643,17 @@ Expression ExpressionRewardContents(boolean prop, boolean pathprop) :
{
{ begin = getToken(1); }
(
// Path formula (including F "target")
// NB: Lookahead used to avoid 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
LOOKAHEAD(ExpressionSS(prop, pathprop)) expr = Expression(prop, true) { ret = expr; }
// Normal reward operators
// First look for cases where it starts with "S" (see above)
LOOKAHEAD(ExpressionSS(prop, pathprop)) expr = ExpressionSS(prop, true) { ret = expr; }
| <S> { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); }
// Normal reward operators (excluding S; see above)
| LOOKAHEAD(<C> <LE>) begin = <C> <LE> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
| <C> { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); }
| <I> <EQ> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
| <S> { 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; }
}

Write Preview
Loading…
Cancel
Save