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

Add ratio reward objectives to the property parser (copied from prism-frac) but no model checking support yet. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8810 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
31690047fa
commit
bbbe3311d1
8 changed files with 344 additions and 199 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. 472
      prism/src/parser/PrismParser.java
  2. 18
      prism/src/parser/PrismParser.jj
  3. 27
      prism/src/parser/ast/ExpressionReward.java
  4. 1
      prism/src/parser/visitor/ASTTraverse.java
  5. 2
      prism/src/parser/visitor/ASTTraverseModify.java
  6. 2
      prism/src/parser/visitor/CheckValid.java
  7. 13
      prism/src/parser/visitor/SemanticCheck.java
  8. 8
      prism/src/parser/visitor/TypeCheck.java

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

@ -2595,7 +2595,6 @@ public class PrismParser implements PrismParserConstants {
// (Property) expression: expected reward operator R
static final public Expression ExpressionReward(boolean prop, boolean pathprop) throws ParseException {
int r;
Object index = null;
String relOp = null;
Expression rew = null;
Expression expr;
@ -2609,7 +2608,7 @@ public class PrismParser implements PrismParserConstants {
begin = jj_consume_token(R);
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case LBRACE:
index = RewardIndex();
RewardIndex(ret);
break;
default:
jj_la1[75] = jj_gen;
@ -2675,7 +2674,6 @@ public class PrismParser implements PrismParserConstants {
;
}
jj_consume_token(RBRACKET);
ret.setRewardStructIndex(index);
ret.setRelOp(relOp);
ret.setReward(rew);
ret.setExpression(expr);
@ -2694,8 +2692,9 @@ public class PrismParser implements PrismParserConstants {
}
// Reward struct index for R operator
static final public Object RewardIndex() throws ParseException {
Object index;
static final public void RewardIndex(ExpressionReward exprRew) throws ParseException {
Object index = null;
Object indexDiv = null;
jj_consume_token(LBRACE);
if (jj_2_15(2147483647)) {
jj_consume_token(DQUOTE);
@ -2737,8 +2736,59 @@ public class PrismParser implements PrismParserConstants {
}
}
jj_consume_token(RBRACE);
{if (true) return index;}
throw new Error("Missing return statement in function");
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case DIVIDE:
jj_consume_token(DIVIDE);
jj_consume_token(LBRACE);
if (jj_2_16(2147483647)) {
jj_consume_token(DQUOTE);
indexDiv = Identifier();
jj_consume_token(DQUOTE);
} else {
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
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 MINUS:
case DQUOTE:
case REG_INT:
case REG_DOUBLE:
case REG_IDENT:
indexDiv = Expression(false, false);
break;
default:
jj_la1[80] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
}
jj_consume_token(RBRACE);
break;
default:
jj_la1[81] = jj_gen;
;
}
exprRew.setRewardStructIndex(index);
if (indexDiv != null) {
exprRew.setRewardStructIndexDiv(indexDiv);
}
}
// Contents of an R operator
@ -2746,7 +2796,7 @@ public class PrismParser implements PrismParserConstants {
Expression expr = null;
ExpressionTemporal ret = null;
Token begin;
if (jj_2_16(2147483647)) {
if (jj_2_17(2147483647)) {
begin = jj_consume_token(C);
jj_consume_token(LE);
expr = Expression(false, false);
@ -2773,7 +2823,7 @@ public class PrismParser implements PrismParserConstants {
ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
break;
default:
jj_la1[80] = jj_gen;
jj_la1[82] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2830,7 +2880,7 @@ public class PrismParser implements PrismParserConstants {
s = "init";
break;
default:
jj_la1[81] = jj_gen;
jj_la1[83] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2875,7 +2925,7 @@ public class PrismParser implements PrismParserConstants {
op = Identifier();
break;
default:
jj_la1[82] = jj_gen;
jj_la1[84] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2887,7 +2937,7 @@ public class PrismParser implements PrismParserConstants {
filter = Expression(prop, pathprop);
break;
default:
jj_la1[83] = jj_gen;
jj_la1[85] = jj_gen;
;
}
jj_consume_token(RPARENTH);
@ -2932,7 +2982,7 @@ public class PrismParser implements PrismParserConstants {
ident="max";
break;
default:
jj_la1[84] = jj_gen;
jj_la1[86] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2965,7 +3015,7 @@ public class PrismParser implements PrismParserConstants {
{if (true) return ExpressionBinaryOp.NE;}
break;
default:
jj_la1[85] = jj_gen;
jj_la1[87] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2992,7 +3042,7 @@ public class PrismParser implements PrismParserConstants {
{if (true) return ExpressionBinaryOp.LE;}
break;
default:
jj_la1[86] = jj_gen;
jj_la1[88] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -3017,7 +3067,7 @@ public class PrismParser implements PrismParserConstants {
step = Expression(false, false);
break;
default:
jj_la1[87] = jj_gen;
jj_la1[89] = jj_gen;
;
}
jj_consume_token(0);
@ -3142,6 +3192,13 @@ public class PrismParser implements PrismParserConstants {
finally { jj_save(15, xla); }
}
static private boolean jj_2_17(int xla) {
jj_la = xla; jj_lastpos = jj_scanpos = token;
try { return !jj_3_17(); }
catch(LookaheadSuccess ls) { return true; }
finally { jj_save(16, xla); }
}
static private boolean jj_3_13() {
if (jj_3R_31()) return true;
if (jj_scan_token(LPARENTH)) return true;
@ -3543,6 +3600,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_113() {
if (jj_scan_token(LE)) return true;
return false;
}
static private boolean jj_3R_58() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_30()) return true;
@ -3550,6 +3612,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_112() {
if (jj_scan_token(GE)) return true;
return false;
}
static private boolean jj_3R_111() {
if (jj_scan_token(LT)) return true;
return false;
}
static private boolean jj_3R_57() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
@ -3557,6 +3629,27 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_103() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_110()) {
jj_scanpos = xsp;
if (jj_3R_111()) {
jj_scanpos = xsp;
if (jj_3R_112()) {
jj_scanpos = xsp;
if (jj_3R_113()) return true;
}
}
}
return false;
}
static private boolean jj_3R_110() {
if (jj_scan_token(GT)) return true;
return false;
}
static private boolean jj_3R_143() {
if (jj_scan_token(REG_INT)) return true;
return false;
@ -3589,21 +3682,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_113() {
if (jj_scan_token(LE)) return true;
return false;
}
static private boolean jj_3R_112() {
if (jj_scan_token(GE)) return true;
return false;
}
static private boolean jj_3R_111() {
if (jj_scan_token(LT)) return true;
return false;
}
static private boolean jj_3R_47() {
Token xsp;
xsp = jj_scanpos;
@ -3622,24 +3700,23 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_103() {
static private boolean jj_3R_105() {
if (jj_scan_token(NE)) return true;
return false;
}
static private boolean jj_3R_100() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_110()) {
jj_scanpos = xsp;
if (jj_3R_111()) {
jj_scanpos = xsp;
if (jj_3R_112()) {
if (jj_3R_104()) {
jj_scanpos = xsp;
if (jj_3R_113()) return true;
}
}
if (jj_3R_105()) return true;
}
return false;
}
static private boolean jj_3R_110() {
if (jj_scan_token(GT)) return true;
static private boolean jj_3R_104() {
if (jj_scan_token(EQ)) return true;
return false;
}
@ -3668,26 +3745,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_105() {
if (jj_scan_token(NE)) return true;
return false;
}
static private boolean jj_3R_100() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_104()) {
jj_scanpos = xsp;
if (jj_3R_105()) return true;
}
return false;
}
static private boolean jj_3R_104() {
if (jj_scan_token(EQ)) return true;
return false;
}
static private boolean jj_3R_60() {
if (jj_scan_token(LBRACE)) return true;
if (jj_3R_28()) return true;
@ -3728,6 +3785,11 @@ 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_59() {
if (jj_scan_token(DIVIDE)) return true;
if (jj_scan_token(LBRACE)) return true;
@ -3761,8 +3823,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_38() {
if (jj_scan_token(REG_IDENTPRIME)) return true;
static private boolean jj_3R_172() {
if (jj_scan_token(OR)) return true;
return false;
}
@ -3790,11 +3852,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_172() {
if (jj_scan_token(OR)) return true;
return false;
}
static private boolean jj_3_2() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
@ -3823,6 +3880,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_132() {
if (jj_3R_28()) return true;
Token xsp;
@ -3831,8 +3893,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_171() {
if (jj_scan_token(AND)) return true;
return false;
}
static private boolean jj_3R_169() {
if (jj_scan_token(MAX)) return true;
return false;
}
@ -3851,6 +3918,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_28() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static private boolean jj_3R_40() {
if (jj_3R_43()) return true;
Token xsp;
@ -3859,18 +3931,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_171() {
if (jj_scan_token(AND)) return true;
return false;
}
static private boolean jj_3R_169() {
if (jj_scan_token(MAX)) return true;
return false;
}
static private boolean jj_3R_28() {
if (jj_scan_token(REG_IDENT)) return true;
static private boolean jj_3R_167() {
if (jj_scan_token(INIT)) return true;
return false;
}
@ -3884,11 +3946,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_167() {
if (jj_scan_token(INIT)) return true;
return false;
}
static private boolean jj_3R_128() {
if (jj_3R_140()) return true;
return false;
@ -3899,6 +3956,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_174() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_39()) return true;
return false;
}
static private boolean jj_3R_117() {
if (jj_scan_token(DIVIDE)) return true;
return false;
@ -3914,34 +3977,38 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_124() {
if (jj_3R_136()) return true;
static private boolean jj_3R_173() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_174() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_39()) return true;
static private boolean jj_3R_170() {
if (jj_scan_token(PLUS)) return true;
return false;
}
static private boolean jj_3R_123() {
if (jj_3R_135()) return true;
static private boolean jj_3R_124() {
if (jj_3R_136()) return true;
return false;
}
static private boolean jj_3R_173() {
static private boolean jj_3R_168() {
if (jj_scan_token(MIN)) return true;
return false;
}
static private boolean jj_3R_166() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_122() {
if (jj_3R_134()) return true;
static private boolean jj_3R_123() {
if (jj_3R_135()) return true;
return false;
}
static private boolean jj_3R_170() {
if (jj_scan_token(PLUS)) return true;
static private boolean jj_3R_122() {
if (jj_3R_134()) return true;
return false;
}
@ -3955,33 +4022,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_168() {
if (jj_scan_token(MIN)) return true;
return false;
}
static private boolean jj_3R_121() {
if (jj_3R_133()) return true;
return false;
}
static private boolean jj_3R_166() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_120() {
if (jj_3R_132()) return true;
return false;
}
static private boolean jj_3R_119() {
if (jj_3R_131()) return true;
return false;
}
static private boolean jj_3R_109() {
if (jj_scan_token(MINUS)) return true;
static private boolean jj_3R_199() {
if (jj_3R_39()) return true;
return false;
}
@ -4014,6 +4061,21 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_120() {
if (jj_3R_132()) return true;
return false;
}
static private boolean jj_3R_119() {
if (jj_3R_131()) return true;
return false;
}
static private boolean jj_3R_109() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static private boolean jj_3R_118() {
Token xsp;
xsp = jj_scanpos;
@ -4064,6 +4126,18 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_141() {
if (jj_scan_token(DQUOTE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_166()) {
jj_scanpos = xsp;
if (jj_3R_167()) return true;
}
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3R_114() {
if (jj_scan_token(MINUS)) return true;
if (jj_3R_106()) return true;
@ -4080,18 +4154,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_141() {
if (jj_scan_token(DQUOTE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_166()) {
jj_scanpos = xsp;
if (jj_3R_167()) return true;
}
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3R_106() {
Token xsp;
xsp = jj_scanpos;
@ -4123,6 +4185,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_140() {
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_3_7() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
@ -4138,14 +4208,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_140() {
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_101() {
if (jj_3R_106()) return true;
Token xsp;
@ -4172,8 +4234,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_165() {
if (jj_3R_180()) return true;
static private boolean jj_3R_139() {
if (jj_scan_token(E)) 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_3_16() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
@ -4187,26 +4257,20 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_139() {
if (jj_scan_token(E)) 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_3_6() {
if (jj_scan_token(DQUOTE)) return true;
static private boolean jj_3R_165() {
if (jj_3R_180()) return true;
return false;
}
static private boolean jj_3_16() {
static private boolean jj_3_17() {
if (jj_scan_token(C)) return true;
if (jj_scan_token(LE)) return true;
return false;
}
static private boolean jj_3_15() {
static private boolean jj_3R_198() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
if (jj_scan_token(DQUOTE)) return true;
return false;
}
@ -4216,6 +4280,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_6() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3R_189() {
if (jj_scan_token(F)) return true;
if (jj_3R_39()) return true;
@ -4234,6 +4303,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_15() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3R_186() {
if (jj_scan_token(C)) return true;
if (jj_scan_token(LE)) return true;
@ -4241,19 +4315,6 @@ public class PrismParser implements PrismParserConstants {
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_195() {
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_164() {
Token xsp;
xsp = jj_scanpos;
@ -4273,6 +4334,19 @@ public class PrismParser implements PrismParserConstants {
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_195() {
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_96() {
if (jj_3R_98()) return true;
Token xsp;
@ -4283,13 +4357,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_192() {
static private boolean jj_3R_197() {
if (jj_scan_token(DIVIDE)) return true;
if (jj_scan_token(LBRACE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_195()) {
if (jj_3R_198()) {
jj_scanpos = xsp;
if (jj_3R_196()) return true;
if (jj_3R_199()) return true;
}
if (jj_scan_token(RBRACE)) return true;
return false;
@ -4301,6 +4376,20 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_192() {
if (jj_scan_token(LBRACE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_195()) {
jj_scanpos = xsp;
if (jj_3R_196()) return true;
}
if (jj_scan_token(RBRACE)) return true;
xsp = jj_scanpos;
if (jj_3R_197()) jj_scanpos = xsp;
return false;
}
static private boolean jj_3R_95() {
if (jj_3R_96()) return true;
Token xsp;
@ -4382,6 +4471,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_92() {
if (jj_scan_token(AND)) return true;
if (jj_3R_91()) return true;
return false;
}
static private boolean jj_3R_184() {
if (jj_scan_token(MIN)) return true;
if (jj_scan_token(EQ)) return true;
@ -4396,12 +4491,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_92() {
if (jj_scan_token(AND)) return true;
if (jj_3R_91()) return true;
return false;
}
static private boolean jj_3R_183() {
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
@ -4597,7 +4686,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[88];
static final private int[] jj_la1 = new int[90];
static private int[] jj_la1_0;
static private int[] jj_la1_1;
static private int[] jj_la1_2;
@ -4607,15 +4696,15 @@ 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,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,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,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x4200100,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,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x4012783a,0x4000,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,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
}
private static void jj_la1_init_2() {
jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e0800,0x0,0x2e0800,0x2e0800,0x0,0x2e0800,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x10,0x0,0x1,0x200000,0x0,0x1,0x200000,0x400,0x2e0800,0x0,0x0,0x0,0x2e0801,0x200000,0x1,0x0,0x2004,0x0,0x0,0x2004,0x220000,0x0,0x3d1,0x0,0x0,0x3d1,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x3d1,0x10000,0x0,0x0,0x0,0x0,0x2e0800,0x30,0x3c0,0xc00,0xc00,0x3000,0x3000,0x2e0800,0x2e0000,0x0,0x0,0x200000,0x0,0xc0000,0x3d0,0x0,0x4,0x4,0x0,0x3d0,0x4,0x4,0x3d0,0x0,0x4,0x2e0800,0x0,0x200000,0x200400,0x0,0x200000,0x30,0x3c0,0x0,};
jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e0800,0x0,0x2e0800,0x2e0800,0x0,0x2e0800,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x10,0x0,0x1,0x200000,0x0,0x1,0x200000,0x400,0x2e0800,0x0,0x0,0x0,0x2e0801,0x200000,0x1,0x0,0x2004,0x0,0x0,0x2004,0x220000,0x0,0x3d1,0x0,0x0,0x3d1,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x3d1,0x10000,0x0,0x0,0x0,0x0,0x2e0800,0x30,0x3c0,0xc00,0xc00,0x3000,0x3000,0x2e0800,0x2e0000,0x0,0x0,0x200000,0x0,0xc0000,0x3d0,0x0,0x4,0x4,0x0,0x3d0,0x4,0x4,0x3d0,0x0,0x4,0x2e0800,0x2e0800,0x2000,0x0,0x200000,0x200400,0x0,0x200000,0x30,0x3c0,0x0,};
}
static final private JJCalls[] jj_2_rtns = new JJCalls[16];
static final private JJCalls[] jj_2_rtns = new JJCalls[17];
static private boolean jj_rescan = false;
static private int jj_gc = 0;
@ -4637,7 +4726,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4652,7 +4741,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4670,7 +4759,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4681,7 +4770,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4698,7 +4787,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4708,7 +4797,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 88; i++) jj_la1[i] = -1;
for (int i = 0; i < 90; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -4825,7 +4914,7 @@ public class PrismParser implements PrismParserConstants {
la1tokens[jj_kind] = true;
jj_kind = -1;
}
for (int i = 0; i < 88; i++) {
for (int i = 0; i < 90; i++) {
if (jj_la1[i] == jj_gen) {
for (int j = 0; j < 32; j++) {
if ((jj_la1_0[i] & (1<<j)) != 0) {
@ -4867,7 +4956,7 @@ public class PrismParser implements PrismParserConstants {
static private void jj_rescan_token() {
jj_rescan = true;
for (int i = 0; i < 16; i++) {
for (int i = 0; i < 17; i++) {
try {
JJCalls p = jj_2_rtns[i];
do {
@ -4890,6 +4979,7 @@ public class PrismParser implements PrismParserConstants {
case 13: jj_3_14(); break;
case 14: jj_3_15(); break;
case 15: jj_3_16(); break;
case 16: jj_3_17(); break;
}
}
p = p.next;

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

@ -1551,7 +1551,6 @@ Expression ExpressionSS(boolean prop, boolean pathprop) :
Expression ExpressionReward(boolean prop, boolean pathprop) :
{
int r;
Object index = null;
String relOp = null;
Expression rew = null;
Expression expr;
@ -1564,7 +1563,7 @@ 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 = <R> (index = RewardIndex())?
(( begin = <R> (RewardIndex(ret))?
(( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } )
|( <EQ> <QMARK> { relOp = "="; isBool = false; } )
|( <MIN> <EQ> <QMARK> { relOp = "min="; isBool = false; } )
@ -1575,7 +1574,6 @@ Expression ExpressionReward(boolean prop, boolean pathprop) :
// Path formula, optional filter
<LBRACKET> expr = ExpressionRewardContents(prop, pathprop) (filter = Filter())? <RBRACKET>
{
ret.setRewardStructIndex(index);
ret.setRelOp(relOp);
ret.setReward(rew);
ret.setExpression(expr);
@ -1595,14 +1593,22 @@ Expression ExpressionReward(boolean prop, boolean pathprop) :
// Reward struct index for R operator
Object RewardIndex() :
void RewardIndex(ExpressionReward exprRew) :
{
Object index;
Object index = null;
Object indexDiv = null;
}
{
// Lookahead here is to ensure that "id" is not misdetected as an ExpressionLabel
( <LBRACE> ( LOOKAHEAD(<DQUOTE>) ( <DQUOTE> index = Identifier() <DQUOTE> ) | index = Expression(false, false) ) <RBRACE> )
{ return index; }
// Optional second reward structure index (for ratio objectives)
( <DIVIDE> ( <LBRACE> ( LOOKAHEAD(<DQUOTE>) ( <DQUOTE> indexDiv = Identifier() <DQUOTE> ) | indexDiv = Expression(false, false) ) <RBRACE> ))?
{
exprRew.setRewardStructIndex(index);
if (indexDiv != null) {
exprRew.setRewardStructIndexDiv(indexDiv);
}
}
}
// Contents of an R operator

27
prism/src/parser/ast/ExpressionReward.java
View File

@ -34,6 +34,7 @@ import prism.PrismLangException;
public class ExpressionReward extends Expression
{
Object rewardStructIndex = null;
Object rewardStructIndexDiv = null;
RelOp relOp = null;
Expression reward = null;
Expression expression = null;
@ -61,6 +62,11 @@ public class ExpressionReward extends Expression
rewardStructIndex = o;
}
public void setRewardStructIndexDiv(Object o)
{
rewardStructIndexDiv = o;
}
public void setRelOp(RelOp relOp)
{
this.relOp = relOp;
@ -93,6 +99,11 @@ public class ExpressionReward extends Expression
return rewardStructIndex;
}
public Object getRewardStructIndexDiv()
{
return rewardStructIndexDiv;
}
public RelOp getRelOp()
{
return relOp;
@ -186,7 +197,14 @@ public class ExpressionReward extends Expression
if (relOp == RelOp.MIN) s = "Minimum e";
else if (relOp == RelOp.MAX) s = "Maximum e";
else s = "E";
if (rewardStructIndex instanceof String) s += "xpected "+rewardStructIndex;
if (rewardStructIndex instanceof String) {
if (rewardStructIndexDiv instanceof String)
s += "xpected "+rewardStructIndex + "/" + rewardStructIndexDiv;
else if (rewardStructIndexDiv == null)
s += "xpected "+rewardStructIndex;
else
s += "xpected reward";
}
// Or just call it "Expected reward"
else s += "xpected reward";
return s;
@ -224,6 +242,11 @@ public class ExpressionReward extends Expression
if (rewardStructIndex != null) {
if (rewardStructIndex instanceof Expression) s += "{"+rewardStructIndex+"}";
else if (rewardStructIndex instanceof String) s += "{\""+rewardStructIndex+"\"}";
if (rewardStructIndexDiv != null) {
s += "/";
if (rewardStructIndexDiv instanceof Expression) s += "{"+rewardStructIndexDiv+"}";
else if (rewardStructIndexDiv instanceof String) s += "{\""+rewardStructIndexDiv+"\"}";
}
}
s += relOp;
s += (reward==null) ? "?" : reward.toString();
@ -245,6 +268,8 @@ public class ExpressionReward extends Expression
expr.setReward(reward == null ? null : reward.deepCopy());
if (rewardStructIndex != null && rewardStructIndex instanceof Expression) expr.setRewardStructIndex(((Expression)rewardStructIndex).deepCopy());
else expr.setRewardStructIndex(rewardStructIndex);
if (rewardStructIndexDiv != null && rewardStructIndexDiv instanceof Expression) expr.setRewardStructIndexDiv(((Expression)rewardStructIndexDiv).deepCopy());
else expr.setRewardStructIndexDiv(rewardStructIndexDiv);
expr.setFilter(filter == null ? null : (Filter)filter.deepCopy());
expr.setType(type);
expr.setPosition(this);

1
prism/src/parser/visitor/ASTTraverse.java
View File

@ -501,6 +501,7 @@ public class ASTTraverse implements ASTVisitor
{
visitPre(e);
if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression) ((Expression)e.getRewardStructIndex()).accept(this);
if (e.getRewardStructIndexDiv() != null && e.getRewardStructIndexDiv() instanceof Expression) ((Expression)e.getRewardStructIndexDiv()).accept(this);
if (e.getReward() != null) e.getReward().accept(this);
if (e.getExpression() != null) e.getExpression().accept(this);
if (e.getFilter() != null) e.getFilter().accept(this);

2
prism/src/parser/visitor/ASTTraverseModify.java
View File

@ -513,6 +513,8 @@ public class ASTTraverseModify implements ASTVisitor
visitPre(e);
if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression)
e.setRewardStructIndex((Expression)(((Expression)e.getRewardStructIndex()).accept(this)));
if (e.getRewardStructIndexDiv() != null && e.getRewardStructIndexDiv() instanceof Expression)
e.setRewardStructIndexDiv((Expression)(((Expression)e.getRewardStructIndexDiv()).accept(this)));
if (e.getReward() != null) e.setReward((Expression)(e.getReward().accept(this)));
if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this)));
if (e.getFilter() != null) e.setFilter((Filter)(e.getFilter().accept(this)));

2
prism/src/parser/visitor/CheckValid.java
View File

@ -100,6 +100,8 @@ public class CheckValid extends ASTTraverse
{
if (modelType.nondeterministic() && e.getRelOp() == RelOp.EQ)
throw new PrismLangException("Can't use \"R=?\" for nondeterministic models; use \"Rmin=?\" or \"Rmax=?\"");
if (e.getRewardStructIndexDiv() != null)
throw new PrismLangException("No support for ratio reward objectives yet");
}
public void visitPost(ExpressionSS e) throws PrismLangException

13
prism/src/parser/visitor/SemanticCheck.java
View File

@ -461,6 +461,19 @@ public class SemanticCheck extends ASTTraverse
}
}
}
if (e.getRewardStructIndexDiv() != null) {
if (e.getRewardStructIndexDiv() instanceof Expression) {
Expression rsi = (Expression) e.getRewardStructIndexDiv();
if (!(rsi.isConstant())) {
throw new PrismLangException("R operator reward struct index is not constant", rsi);
}
} else if (e.getRewardStructIndexDiv() instanceof String) {
String s = (String) e.getRewardStructIndexDiv();
if (modulesFile != null && modulesFile.getRewardStructIndex(s) == -1) {
throw new PrismLangException("R operator reward struct index \"" + s + "\" does not exist", e);
}
}
}
if (e.getReward() != null && !e.getReward().isConstant()) {
throw new PrismLangException("R operator reward bound is not constant", e.getReward());
}

8
prism/src/parser/visitor/TypeCheck.java
View File

@ -488,13 +488,19 @@ public class TypeCheck extends ASTTraverse
public void visitPost(ExpressionReward e) throws PrismLangException
{
// Check reward struct ref
// Check reward struct ref(s)
if (e.getRewardStructIndex() != null && e.getRewardStructIndex() instanceof Expression) {
Expression rsi = (Expression) e.getRewardStructIndex();
if (!(rsi.getType() instanceof TypeInt)) {
throw new PrismLangException("Type error: Reward structure index must be string or integer", rsi);
}
}
if (e.getRewardStructIndexDiv() != null && e.getRewardStructIndexDiv() instanceof Expression) {
Expression rsi = (Expression) e.getRewardStructIndexDiv();
if (!(rsi.getType() instanceof TypeInt)) {
throw new PrismLangException("Type error: Reward structure index must be string or integer", rsi);
}
}
// Check reward bound
if (e.getReward() != null && !TypeDouble.getInstance().canAssign(e.getReward().getType())) {
throw new PrismLangException("Type error: R operator reward bound is not a double", e.getReward());

Write Preview
Loading…
Cancel
Save