From f19cb029d79b4b133bc4127ddd9497147f2157c3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Jun 2015 09:14:31 +0000 Subject: [PATCH] Parse modifiers on R and S operators as well as P. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10037 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 618 ++++++++++++++++-------------- prism/src/parser/PrismParser.jj | 11 +- 2 files changed, 340 insertions(+), 289 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index cf2b1405..5f4ab92a 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -2576,6 +2576,7 @@ public class PrismParser implements PrismParserConstants { // (Property) expression: steady-state operator S static final public Expression ExpressionSS(boolean prop, boolean pathprop) throws ParseException { + ExpressionIdent modifier = null; int r; String relOp = null; Expression prob = null; @@ -2588,10 +2589,21 @@ public class PrismParser implements PrismParserConstants { // Various options for "S" keyword and attached symbols begin = jj_consume_token(S); switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case LPARENTH: case LT: case GT: case LE: case GE: + switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case LPARENTH: + jj_consume_token(LPARENTH); + modifier = IdentifierExpression(); + jj_consume_token(RPARENTH); + break; + default: + jj_la1[74] = jj_gen; + ; + } r = LtGt(); prob = Expression(false, false); relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; @@ -2602,7 +2614,7 @@ public class PrismParser implements PrismParserConstants { relOp = "="; isBool = false; break; default: - jj_la1[74] = jj_gen; + jj_la1[75] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2613,10 +2625,11 @@ public class PrismParser implements PrismParserConstants { filter = Filter(); break; default: - jj_la1[75] = jj_gen; + jj_la1[76] = jj_gen; ; } jj_consume_token(RBRACKET); + ret.setModifier(modifier == null ? null : modifier.getName()); ret.setRelOp(relOp); ret.setProb(prob); ret.setExpression(expr); @@ -2636,6 +2649,7 @@ public class PrismParser implements PrismParserConstants { // (Property) expression: expected reward operator R static final public Expression ExpressionReward(boolean prop, boolean pathprop) throws ParseException { + ExpressionIdent modifier = null; int r; String relOp = null; Expression rew = null; @@ -2649,11 +2663,21 @@ public class PrismParser implements PrismParserConstants { case R: begin = jj_consume_token(R); switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case LPARENTH: + jj_consume_token(LPARENTH); + modifier = IdentifierExpression(); + jj_consume_token(RPARENTH); + break; + default: + jj_la1[77] = jj_gen; + ; + } + switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { case LBRACE: RewardIndex(ret); break; default: - jj_la1[76] = jj_gen; + jj_la1[78] = jj_gen; ; } switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { @@ -2663,7 +2687,7 @@ public class PrismParser implements PrismParserConstants { case GE: r = LtGt(); rew = Expression(false, false); - relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; + relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; break; case EQ: jj_consume_token(EQ); @@ -2683,7 +2707,7 @@ public class PrismParser implements PrismParserConstants { relOp = "max="; isBool = false; break; default: - jj_la1[77] = jj_gen; + jj_la1[79] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2701,7 +2725,7 @@ public class PrismParser implements PrismParserConstants { relOp = "max="; isBool = false; break; default: - jj_la1[78] = jj_gen; + jj_la1[80] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2712,10 +2736,11 @@ public class PrismParser implements PrismParserConstants { filter = Filter(); break; default: - jj_la1[79] = jj_gen; + jj_la1[81] = jj_gen; ; } jj_consume_token(RBRACKET); + ret.setModifier(modifier == null ? null : modifier.getName()); ret.setRelOp(relOp); ret.setReward(rew); ret.setExpression(expr); @@ -2774,7 +2799,7 @@ public class PrismParser implements PrismParserConstants { index = Expression(false, false); break; default: - jj_la1[80] = jj_gen; + jj_la1[82] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2820,7 +2845,7 @@ public class PrismParser implements PrismParserConstants { indexDiv = Expression(false, false); break; default: - jj_la1[81] = jj_gen; + jj_la1[83] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2828,7 +2853,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(RBRACE); break; default: - jj_la1[82] = jj_gen; + jj_la1[84] = jj_gen; ; } exprRew.setRewardStructIndex(index); @@ -2869,7 +2894,7 @@ public class PrismParser implements PrismParserConstants { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); break; default: - jj_la1[83] = jj_gen; + jj_la1[85] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2928,7 +2953,7 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(DRBRACKET); break; default: - jj_la1[84] = jj_gen; + jj_la1[86] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2950,7 +2975,7 @@ public class PrismParser implements PrismParserConstants { expr = ExpressionFuncOrIdent(prop, pathprop); break; default: - jj_la1[85] = jj_gen; + jj_la1[87] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -2976,7 +3001,7 @@ public class PrismParser implements PrismParserConstants { s = "init"; break; default: - jj_la1[86] = jj_gen; + jj_la1[88] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3021,7 +3046,7 @@ public class PrismParser implements PrismParserConstants { op = Identifier(); break; default: - jj_la1[87] = jj_gen; + jj_la1[89] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3033,7 +3058,7 @@ public class PrismParser implements PrismParserConstants { filter = Expression(prop, pathprop); break; default: - jj_la1[88] = jj_gen; + jj_la1[90] = jj_gen; ; } jj_consume_token(RPARENTH); @@ -3078,7 +3103,7 @@ public class PrismParser implements PrismParserConstants { ident="max"; break; default: - jj_la1[89] = jj_gen; + jj_la1[91] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3111,7 +3136,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.NE;} break; default: - jj_la1[90] = jj_gen; + jj_la1[92] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3138,7 +3163,7 @@ public class PrismParser implements PrismParserConstants { {if (true) return ExpressionBinaryOp.LE;} break; default: - jj_la1[91] = jj_gen; + jj_la1[93] = jj_gen; jj_consume_token(-1); throw new ParseException(); } @@ -3163,7 +3188,7 @@ public class PrismParser implements PrismParserConstants { step = Expression(false, false); break; default: - jj_la1[92] = jj_gen; + jj_la1[94] = jj_gen; ; } jj_consume_token(0); @@ -3295,7 +3320,7 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(16, xla); } } - static private boolean jj_3R_203() { + static private boolean jj_3R_205() { if (jj_scan_token(MAX)) return true; return false; } @@ -3305,7 +3330,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_202() { + static private boolean jj_3R_204() { if (jj_scan_token(MIN)) return true; return false; } @@ -3338,13 +3363,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_200() { + static private boolean jj_3R_202() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_202()) { + if (jj_3R_204()) { jj_scanpos = xsp; - if (jj_3R_203()) return true; + if (jj_3R_205()) return true; } if (jj_scan_token(RBRACE)) return true; return false; @@ -3363,7 +3388,7 @@ public class PrismParser implements PrismParserConstants { Token xsp; while (true) { xsp = jj_scanpos; - if (jj_3R_200()) { jj_scanpos = xsp; break; } + if (jj_3R_202()) { jj_scanpos = xsp; break; } } return false; } @@ -3639,13 +3664,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_136() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_39()) return true; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - static private boolean jj_3R_113() { if (jj_scan_token(LE)) return true; return false; @@ -3656,6 +3674,13 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_136() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_39()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + static private boolean jj_3R_111() { if (jj_scan_token(LT)) return true; return false; @@ -3682,28 +3707,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_154() { - if (jj_scan_token(MAX)) return true; - return false; - } - - static private boolean jj_3R_148() { - if (jj_scan_token(FALSE)) return true; - return false; - } - - static private boolean jj_3R_147() { - if (jj_scan_token(TRUE)) return true; - return false; - } - static private boolean jj_3R_105() { if (jj_scan_token(NE)) return true; return false; } - static private boolean jj_3R_39() { - if (jj_3R_42()) return true; + static private boolean jj_3R_154() { + if (jj_scan_token(MAX)) return true; return false; } @@ -3722,6 +3732,21 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_148() { + if (jj_scan_token(FALSE)) return true; + return false; + } + + static private boolean jj_3R_147() { + if (jj_scan_token(TRUE)) return true; + return false; + } + + static private boolean jj_3R_39() { + if (jj_3R_42()) return true; + return false; + } + static private boolean jj_3_4() { if (jj_scan_token(LABEL)) return true; return false; @@ -3738,13 +3763,18 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_38() { + if (jj_scan_token(REG_IDENTPRIME)) return true; + return false; + } + static private boolean jj_3R_153() { if (jj_scan_token(MIN)) return true; return false; } - static private boolean jj_3R_38() { - if (jj_scan_token(REG_IDENTPRIME)) return true; + static private boolean jj_3R_180() { + if (jj_scan_token(OR)) return true; return false; } @@ -3794,11 +3824,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_180() { - if (jj_scan_token(OR)) return true; - return false; - } - static private boolean jj_3R_151() { if (jj_scan_token(MAX)) return true; return false; @@ -3835,6 +3860,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_3_9() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; @@ -3842,8 +3872,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_31() { - if (jj_3R_28()) return true; + static private boolean jj_3R_179() { + if (jj_scan_token(AND)) return true; + return false; + } + + static private boolean jj_3R_177() { + if (jj_scan_token(MAX)) return true; return false; } @@ -3887,18 +3922,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_179() { - if (jj_scan_token(AND)) return true; - return false; - } - - static private boolean jj_3R_177() { - if (jj_scan_token(MAX)) return true; + static private boolean jj_3R_28() { + if (jj_scan_token(REG_IDENT)) return true; return false; } - static private boolean jj_3R_28() { - if (jj_scan_token(REG_IDENT)) return true; + static private boolean jj_3R_175() { + if (jj_scan_token(INIT)) return true; return false; } @@ -3935,11 +3965,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_175() { - if (jj_scan_token(INIT)) return true; - return false; - } - static private boolean jj_3_8() { if (jj_scan_token(OR)) return true; if (jj_scan_token(OR)) return true; @@ -3951,6 +3976,12 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_182() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_39()) return true; + return false; + } + static private boolean jj_3R_134() { Token xsp; xsp = jj_scanpos; @@ -3964,6 +3995,21 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_181() { + if (jj_3R_28()) return true; + return false; + } + + static private boolean jj_3R_178() { + if (jj_scan_token(PLUS)) return true; + return false; + } + + static private boolean jj_3R_173() { + if (jj_3R_133()) return true; + return false; + } + static private boolean jj_3_2() { if (jj_scan_token(DQUOTE)) return true; if (jj_3R_28()) return true; @@ -3972,9 +4018,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_182() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_39()) return true; + static private boolean jj_3R_176() { + if (jj_scan_token(MIN)) return true; + return false; + } + + static private boolean jj_3R_174() { + if (jj_3R_28()) return true; return false; } @@ -3985,8 +4035,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_181() { - if (jj_3R_28()) return true; + static private boolean jj_3R_171() { + if (jj_3R_139()) return true; return false; } @@ -4003,39 +4053,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_178() { - if (jj_scan_token(PLUS)) return true; - return false; - } - - static private boolean jj_3R_173() { - if (jj_3R_133()) return true; - return false; - } - - static private boolean jj_3R_176() { - if (jj_scan_token(MIN)) return true; - return false; - } - - static private boolean jj_3R_174() { - if (jj_3R_28()) return true; - return false; - } - - static private boolean jj_3R_133() { - if (jj_3R_28()) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_149()) jj_scanpos = xsp; - return false; - } - - static private boolean jj_3R_171() { - if (jj_3R_139()) return true; - return false; - } - static private boolean jj_3R_144() { if (jj_scan_token(FILTER)) return true; if (jj_scan_token(LPARENTH)) return true; @@ -4065,6 +4082,14 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_133() { + if (jj_3R_28()) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_149()) jj_scanpos = xsp; + return false; + } + static private boolean jj_3R_44() { if (jj_scan_token(OR)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -4098,6 +4123,18 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_143() { + if (jj_scan_token(DQUOTE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_174()) { + jj_scanpos = xsp; + if (jj_3R_175()) return true; + } + if (jj_scan_token(DQUOTE)) return true; + return false; + } + static private boolean jj_3R_129() { if (jj_3R_142()) return true; return false; @@ -4118,15 +4155,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_143() { - if (jj_scan_token(DQUOTE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_174()) { - jj_scanpos = xsp; - if (jj_3R_175()) return true; - } - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_210() { + if (jj_3R_39()) return true; return false; } @@ -4145,12 +4175,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_208() { - if (jj_3R_39()) return true; + static private boolean jj_3R_123() { + if (jj_3R_136()) return true; return false; } - static private boolean jj_3R_123() { + static private boolean jj_3R_172() { if (jj_3R_136()) return true; return false; } @@ -4160,6 +4190,11 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_170() { + if (jj_3R_137()) return true; + return false; + } + static private boolean jj_3R_36() { if (jj_3R_40()) return true; Token xsp; @@ -4175,23 +4210,30 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_169() { + if (jj_scan_token(DLBRACKET)) return true; + if (jj_scan_token(DRBRACKET)) return true; + return false; + } + static private boolean jj_3R_120() { if (jj_3R_133()) return true; return false; } - static private boolean jj_3R_119() { - if (jj_3R_132()) return true; + static private boolean jj_3R_168() { + if (jj_scan_token(DLT)) return true; + if (jj_scan_token(DGT)) return true; return false; } - static private boolean jj_3R_172() { - if (jj_3R_136()) return true; + static private boolean jj_3R_119() { + if (jj_3R_132()) return true; return false; } - static private boolean jj_3R_170() { - if (jj_3R_137()) return true; + static private boolean jj_3R_207() { + if (jj_3R_39()) return true; return false; } @@ -4200,20 +4242,24 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_169() { - if (jj_scan_token(DLBRACKET)) return true; - if (jj_scan_token(DRBRACKET)) return true; - return false; - } - - static private boolean jj_3R_168() { - if (jj_scan_token(DLT)) return true; - if (jj_scan_token(DGT)) return true; - return false; - } - - static private boolean jj_3R_205() { - if (jj_3R_39()) return true; + static private boolean jj_3R_142() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_168()) { + jj_scanpos = xsp; + if (jj_3R_169()) return true; + } + xsp = jj_scanpos; + if (jj_3R_170()) { + jj_scanpos = xsp; + if (jj_3R_171()) { + jj_scanpos = xsp; + if (jj_3R_172()) { + jj_scanpos = xsp; + if (jj_3R_173()) return true; + } + } + } return false; } @@ -4260,27 +4306,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_142() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_168()) { - jj_scanpos = xsp; - if (jj_3R_169()) return true; - } - xsp = jj_scanpos; - if (jj_3R_170()) { - jj_scanpos = xsp; - if (jj_3R_171()) { - jj_scanpos = xsp; - if (jj_3R_172()) { - jj_scanpos = xsp; - if (jj_3R_173()) return true; - } - } - } - return false; - } - static private boolean jj_3R_115() { if (jj_3R_118()) return true; return false; @@ -4302,6 +4327,14 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_141() { + if (jj_scan_token(A)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_39()) return true; + if (jj_scan_token(RBRACKET)) return true; + return false; + } + static private boolean jj_3R_106() { Token xsp; xsp = jj_scanpos; @@ -4317,14 +4350,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_141() { - if (jj_scan_token(A)) return true; - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_39()) return true; - if (jj_scan_token(RBRACKET)) return true; - return false; - } - static private boolean jj_3R_30() { if (jj_3R_33()) return true; return false; @@ -4366,22 +4391,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_108() { - if (jj_scan_token(PLUS)) return true; - return false; - } - - static private boolean jj_3R_102() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_108()) { - jj_scanpos = xsp; - if (jj_3R_109()) return true; - } - if (jj_3R_101()) return true; - return false; - } - static private boolean jj_3R_140() { if (jj_scan_token(E)) return true; if (jj_scan_token(LBRACKET)) return true; @@ -4395,8 +4404,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_167() { - if (jj_3R_189()) return true; + static private boolean jj_3R_108() { + if (jj_scan_token(PLUS)) return true; return false; } @@ -4406,42 +4415,48 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_98() { - if (jj_3R_101()) return true; + static private boolean jj_3R_167() { + if (jj_3R_189()) return true; + return false; + } + + static private boolean jj_3R_102() { Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_102()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_108()) { + jj_scanpos = xsp; + if (jj_3R_109()) return true; } + if (jj_3R_101()) return true; return false; } - static private boolean jj_3R_207() { + static private boolean jj_3R_209() { 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_199() { + static private boolean jj_3R_201() { if (jj_scan_token(S)) return true; return false; } - static private boolean jj_3R_198() { + static private boolean jj_3R_200() { if (jj_scan_token(F)) return true; if (jj_3R_39()) return true; return false; } - static private boolean jj_3R_197() { + static private boolean jj_3R_199() { if (jj_scan_token(I)) return true; if (jj_scan_token(EQ)) return true; if (jj_3R_39()) return true; return false; } - static private boolean jj_3R_196() { + static private boolean jj_3R_198() { if (jj_scan_token(C)) return true; return false; } @@ -4451,30 +4466,35 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_195() { + static private boolean jj_3R_197() { if (jj_scan_token(C)) return true; if (jj_scan_token(LE)) return true; if (jj_3R_39()) return true; return false; } - static private boolean jj_3_6() { - if (jj_scan_token(DQUOTE)) return true; + static private boolean jj_3R_98() { + if (jj_3R_101()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_102()) { jj_scanpos = xsp; break; } + } return false; } static private boolean jj_3R_166() { Token xsp; xsp = jj_scanpos; - if (jj_3R_195()) { - jj_scanpos = xsp; - if (jj_3R_196()) { - jj_scanpos = xsp; if (jj_3R_197()) { jj_scanpos = xsp; if (jj_3R_198()) { jj_scanpos = xsp; - if (jj_3R_199()) return true; + if (jj_3R_199()) { + jj_scanpos = xsp; + if (jj_3R_200()) { + jj_scanpos = xsp; + if (jj_3R_201()) return true; } } } @@ -4482,53 +4502,58 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_204() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_28()) return true; + static private boolean jj_3_6() { if (jj_scan_token(DQUOTE)) return true; return false; } - static private boolean jj_3R_99() { - if (jj_3R_103()) return true; - if (jj_3R_98()) return true; - return false; - } - - static private boolean jj_3R_96() { - if (jj_3R_98()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_99()) { jj_scanpos = xsp; break; } - } + static private boolean jj_3R_206() { + 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_206() { + static private boolean jj_3R_208() { if (jj_scan_token(DIVIDE)) return true; if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_207()) { + if (jj_3R_209()) { jj_scanpos = xsp; - if (jj_3R_208()) return true; + if (jj_3R_210()) return true; } if (jj_scan_token(RBRACE)) return true; return false; } - static private boolean jj_3R_201() { + static private boolean jj_3R_99() { + if (jj_3R_103()) return true; + if (jj_3R_98()) return true; + return false; + } + + static private boolean jj_3R_203() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_204()) { + if (jj_3R_206()) { jj_scanpos = xsp; - if (jj_3R_205()) return true; + if (jj_3R_207()) return true; } if (jj_scan_token(RBRACE)) return true; xsp = jj_scanpos; - if (jj_3R_206()) jj_scanpos = xsp; + if (jj_3R_208()) jj_scanpos = xsp; + return false; + } + + static private boolean jj_3R_96() { + if (jj_3R_98()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_99()) { jj_scanpos = xsp; break; } + } return false; } @@ -4579,33 +4604,31 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_190() { - if (jj_3R_201()) return true; + static private boolean jj_3R_193() { + if (jj_3R_103()) return true; + if (jj_3R_39()) return true; return false; } - static private boolean jj_3R_35() { - if (jj_scan_token(AND)) return true; - if (jj_3R_34()) return true; + static private boolean jj_3R_192() { + if (jj_3R_203()) return true; return false; } - static private boolean jj_3R_91() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_93()) { - jj_scanpos = xsp; - if (jj_3R_94()) return true; - } + static private boolean jj_3R_191() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_31()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static private boolean jj_3R_162() { - if (jj_3R_189()) return true; + static private boolean jj_3R_35() { + if (jj_scan_token(AND)) return true; + if (jj_3R_34()) return true; return false; } - static private boolean jj_3R_194() { + static private boolean jj_3R_196() { if (jj_scan_token(MAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -4619,7 +4642,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_193() { + static private boolean jj_3R_195() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -4633,21 +4656,24 @@ public class PrismParser implements PrismParserConstants { return false; } - static private boolean jj_3R_192() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static private boolean jj_3R_91() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_93()) { + jj_scanpos = xsp; + if (jj_3R_94()) return true; + } return false; } - static private boolean jj_3R_92() { - if (jj_scan_token(AND)) return true; - if (jj_3R_91()) return true; + static private boolean jj_3R_194() { + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } - static private boolean jj_3R_191() { - if (jj_3R_103()) return true; - if (jj_3R_39()) return true; + static private boolean jj_3R_162() { + if (jj_3R_189()) return true; return false; } @@ -4655,37 +4681,26 @@ public class PrismParser implements PrismParserConstants { if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_190()) jj_scanpos = xsp; + if (jj_3R_191()) jj_scanpos = xsp; + xsp = jj_scanpos; + if (jj_3R_192()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_191()) { + if (jj_3R_193()) { jj_scanpos = xsp; - if (jj_3R_192()) { + if (jj_3R_194()) { jj_scanpos = xsp; - if (jj_3R_193()) { + if (jj_3R_195()) { jj_scanpos = xsp; - if (jj_3R_194()) return true; + if (jj_3R_196()) return true; } } } return false; } - static private boolean jj_3R_34() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_38()) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_39()) return true; - if (jj_scan_token(RPARENTH)) return true; - return false; - } - - static private boolean jj_3R_89() { + static private boolean jj_3R_92() { + if (jj_scan_token(AND)) return true; if (jj_3R_91()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_92()) { jj_scanpos = xsp; break; } - } return false; } @@ -4707,6 +4722,25 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_34() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_38()) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_39()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + + static private boolean jj_3R_89() { + if (jj_3R_91()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_92()) { jj_scanpos = xsp; break; } + } + return false; + } + static private boolean jj_3R_90() { if (jj_scan_token(OR)) return true; if (jj_3R_89()) return true; @@ -4764,6 +4798,13 @@ public class PrismParser implements PrismParserConstants { return false; } + static private boolean jj_3R_190() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_31()) return true; + if (jj_scan_token(RPARENTH)) return true; + return false; + } + static private boolean jj_3R_161() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; @@ -4771,6 +4812,9 @@ public class PrismParser implements PrismParserConstants { } static private boolean jj_3R_160() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_190()) jj_scanpos = xsp; if (jj_3R_103()) return true; if (jj_3R_39()) return true; return false; @@ -4852,7 +4896,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[93]; + static final private int[] jj_la1 = new int[95]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; @@ -4862,13 +4906,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,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x4200100,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,0x4200100,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,0x0,0x0,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,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,0x3340,0x10,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,0x404,0x2000000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[17]; static private boolean jj_rescan = false; @@ -4892,7 +4936,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4907,7 +4951,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4925,7 +4969,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4936,7 +4980,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4953,7 +4997,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -4963,7 +5007,7 @@ public class PrismParser implements PrismParserConstants { token = new Token(); jj_ntk = -1; jj_gen = 0; - for (int i = 0; i < 93; i++) jj_la1[i] = -1; + for (int i = 0; i < 95; i++) jj_la1[i] = -1; for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } @@ -5080,7 +5124,7 @@ public class PrismParser implements PrismParserConstants { la1tokens[jj_kind] = true; jj_kind = -1; } - for (int i = 0; i < 93; i++) { + for (int i = 0; i < 95; i++) { if (jj_la1[i] == jj_gen) { for (int j = 0; j < 32; j++) { if ((jj_la1_0[i] & (1< ( + ( modifier = IdentifierExpression() )? ( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) | ( { relOp = "="; isBool = false; } ) ) // Expression, optional filter expr = Expression(prop, pathprop) (filter = Filter())? { + ret.setModifier(modifier == null ? null : modifier.getName()); ret.setRelOp(relOp); ret.setProb(prob); ret.setExpression(expr); @@ -1559,6 +1562,7 @@ Expression ExpressionSS(boolean prop, boolean pathprop) : Expression ExpressionReward(boolean prop, boolean pathprop) : { + ExpressionIdent modifier = null; int r; String relOp = null; Expression rew = null; @@ -1572,8 +1576,10 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : // This production is only allowed in expressions if the "prop" parameter is true { if (!prop) throw generateParseException(); } // Various options for "R" keyword and attached symbols - (( begin = (RewardIndex(ret))? - (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) + (( begin = + ( modifier = IdentifierExpression() )? + (RewardIndex(ret))? + (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) |( { relOp = "="; isBool = false; } ) |( { relOp = "min="; isBool = false; } ) |( { relOp = "max="; isBool = false; } ))) @@ -1583,6 +1589,7 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : // Path formula, optional filter expr = ExpressionRewardContents(prop, pathprop) (filter = Filter())? { + ret.setModifier(modifier == null ? null : modifier.getName()); ret.setRelOp(relOp); ret.setReward(rew); ret.setExpression(expr);