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

Added weak until (W) and release (R) to properties language. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@700 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
ffc6437a7e
commit
e572ad0b2d
7 changed files with 471 additions and 394 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. 543
      prism/src/parser/PrismParser.java
  2. 9
      prism/src/parser/PrismParser.jj
  3. 72
      prism/src/parser/PrismParserConstants.java
  4. 207
      prism/src/parser/PrismParserTokenManager.java
  5. 4
      prism/src/parser/ast/Expression.java
  6. 28
      prism/src/parser/ast/PathExpressionTemporal.java
  7. 2
      prism/src/parser/visitor/TypeCheck.java

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

@ -2072,7 +2072,7 @@ public class PrismParser implements PrismParserConstants {
throw new Error("Missing return statement in function");
}
// Temporal operarors (X, U, F, G)
// Temporal operarors (X, U, F, G, W, R)
static final public PathExpression PathExpressionTemporal() throws ParseException {
PathExpressionTemporal pe = new PathExpressionTemporal();
Expression expr1 = null, expr2 = null;
@ -2104,8 +2104,24 @@ public class PrismParser implements PrismParserConstants {
case REG_DOUBLE:
case REG_IDENT:
expr1 = Expression();
jj_consume_token(U);
pe.setOperator(PathExpressionTemporal.P_U);
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case U:
jj_consume_token(U);
pe.setOperator(PathExpressionTemporal.P_U);
break;
case W:
jj_consume_token(W);
pe.setOperator(PathExpressionTemporal.P_W);
break;
case R:
jj_consume_token(R);
pe.setOperator(PathExpressionTemporal.P_R);
break;
default:
jj_la1[61] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
break;
case F:
jj_consume_token(F);
@ -2116,7 +2132,7 @@ public class PrismParser implements PrismParserConstants {
pe.setOperator(PathExpressionTemporal.P_G);
break;
default:
jj_la1[61] = jj_gen;
jj_la1[62] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2127,7 +2143,7 @@ public class PrismParser implements PrismParserConstants {
tb = TimeBound();
break;
default:
jj_la1[62] = jj_gen;
jj_la1[63] = jj_gen;
;
}
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
@ -2153,7 +2169,7 @@ public class PrismParser implements PrismParserConstants {
expr2 = Expression();
break;
default:
jj_la1[63] = jj_gen;
jj_la1[64] = jj_gen;
;
}
if (tb != null) pe.setLowerBound(tb.lBound);
@ -2245,7 +2261,7 @@ public class PrismParser implements PrismParserConstants {
jj_consume_token(RBRACKET);
break;
default:
jj_la1[64] = jj_gen;
jj_la1[65] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2279,7 +2295,7 @@ public class PrismParser implements PrismParserConstants {
relOp = "=";
break;
default:
jj_la1[65] = jj_gen;
jj_la1[66] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2290,7 +2306,7 @@ public class PrismParser implements PrismParserConstants {
filter = Filter();
break;
default:
jj_la1[66] = jj_gen;
jj_la1[67] = jj_gen;
;
}
jj_consume_token(RBRACKET);
@ -2321,7 +2337,7 @@ public class PrismParser implements PrismParserConstants {
index = RewardIndex();
break;
default:
jj_la1[67] = jj_gen;
jj_la1[68] = jj_gen;
;
}
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
@ -2351,7 +2367,7 @@ public class PrismParser implements PrismParserConstants {
relOp = "max=";
break;
default:
jj_la1[68] = jj_gen;
jj_la1[69] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2369,7 +2385,7 @@ public class PrismParser implements PrismParserConstants {
relOp = "max=";
break;
default:
jj_la1[69] = jj_gen;
jj_la1[70] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2380,7 +2396,7 @@ public class PrismParser implements PrismParserConstants {
filter = Filter();
break;
default:
jj_la1[70] = jj_gen;
jj_la1[71] = jj_gen;
;
}
jj_consume_token(RBRACKET);
@ -2426,7 +2442,7 @@ public class PrismParser implements PrismParserConstants {
index = Expression();
break;
default:
jj_la1[71] = jj_gen;
jj_la1[72] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2464,7 +2480,7 @@ public class PrismParser implements PrismParserConstants {
pe = new PathExpressionTemporal(PathExpressionTemporal.R_S, null, null);
break;
default:
jj_la1[72] = jj_gen;
jj_la1[73] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2487,7 +2503,7 @@ public class PrismParser implements PrismParserConstants {
s = "init";
break;
default:
jj_la1[73] = jj_gen;
jj_la1[74] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2532,7 +2548,7 @@ public class PrismParser implements PrismParserConstants {
{if (true) return ExpressionBinaryOp.NE;}
break;
default:
jj_la1[74] = jj_gen;
jj_la1[75] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2559,7 +2575,7 @@ public class PrismParser implements PrismParserConstants {
{if (true) return ExpressionBinaryOp.LE;}
break;
default:
jj_la1[75] = jj_gen;
jj_la1[76] = jj_gen;
jj_consume_token(-1);
throw new ParseException();
}
@ -2584,7 +2600,7 @@ public class PrismParser implements PrismParserConstants {
step = Expression();
break;
default:
jj_la1[76] = jj_gen;
jj_la1[77] = jj_gen;
;
}
jj_consume_token(0);
@ -2660,28 +2676,8 @@ public class PrismParser implements PrismParserConstants {
finally { jj_save(8, xla); }
}
static final private boolean jj_3R_120() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_131()) {
jj_scanpos = xsp;
if (jj_3R_132()) {
jj_scanpos = xsp;
if (jj_3R_133()) {
jj_scanpos = xsp;
if (jj_3R_134()) return true;
}
}
}
xsp = jj_scanpos;
if (jj_3R_135()) jj_scanpos = xsp;
xsp = jj_scanpos;
if (jj_3R_136()) jj_scanpos = xsp;
return false;
}
static final private boolean jj_3_9() {
if (jj_scan_token(DQUOTE)) return true;
static final private boolean jj_3R_130() {
if (jj_scan_token(S)) return true;
return false;
}
@ -2695,22 +2691,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_130() {
if (jj_scan_token(S)) return true;
return false;
}
static final private boolean jj_3R_129() {
if (jj_scan_token(F)) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_74() {
if (jj_3R_80()) return true;
return false;
}
static final private boolean jj_3R_128() {
if (jj_scan_token(I)) return true;
if (jj_scan_token(EQ)) return true;
@ -2718,11 +2704,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_105() {
if (jj_3R_121()) return true;
return false;
}
static final private boolean jj_3R_127() {
if (jj_scan_token(C)) return true;
if (jj_scan_token(LE)) return true;
@ -2730,12 +2711,7 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_73() {
if (jj_3R_79()) return true;
return false;
}
static final private boolean jj_3R_142() {
static final private boolean jj_3R_145() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_27()) return true;
if (jj_scan_token(DQUOTE)) return true;
@ -2758,6 +2734,21 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_74() {
if (jj_3R_80()) return true;
return false;
}
static final private boolean jj_3R_105() {
if (jj_3R_121()) return true;
return false;
}
static final private boolean jj_3R_73() {
if (jj_3R_79()) return true;
return false;
}
static final private boolean jj_3R_31() {
if (jj_scan_token(AND)) return true;
if (jj_3R_30()) return true;
@ -2784,12 +2775,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_141() {
static final private boolean jj_3R_144() {
if (jj_scan_token(MAX)) return true;
return false;
}
static final private boolean jj_3R_140() {
static final private boolean jj_3R_143() {
if (jj_scan_token(MIN)) return true;
return false;
}
@ -2799,23 +2790,23 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_59() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static final private boolean jj_3R_138() {
if (jj_scan_token(LBRACE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_142()) {
if (jj_3R_145()) {
jj_scanpos = xsp;
if (jj_3R_143()) return true;
if (jj_3R_146()) return true;
}
if (jj_scan_token(RBRACE)) return true;
return false;
}
static final private boolean jj_3R_59() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static final private boolean jj_3R_30() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_32()) return true;
@ -2829,9 +2820,9 @@ public class PrismParser implements PrismParserConstants {
if (jj_scan_token(LBRACE)) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_140()) {
if (jj_3R_143()) {
jj_scanpos = xsp;
if (jj_3R_141()) return true;
if (jj_3R_144()) return true;
}
if (jj_scan_token(RBRACE)) return true;
return false;
@ -2883,14 +2874,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_64() {
if (jj_scan_token(MINUS)) return true;
if (jj_3R_56()) return true;
static final private boolean jj_3R_122() {
if (jj_3R_138()) return true;
return false;
}
static final private boolean jj_3R_122() {
if (jj_3R_138()) return true;
static final private boolean jj_3R_64() {
if (jj_scan_token(MINUS)) return true;
if (jj_3R_56()) return true;
return false;
}
@ -2919,22 +2910,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_116() {
if (jj_3R_53()) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_56() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_64()) {
jj_scanpos = xsp;
if (jj_3R_65()) return true;
}
return false;
}
static final private boolean jj_3R_126() {
if (jj_scan_token(MAX)) return true;
if (jj_scan_token(EQ)) return true;
@ -2956,21 +2931,20 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_110() {
if (jj_scan_token(RMIN)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
static final private boolean jj_3R_116() {
if (jj_3R_53()) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_124() {
static final private boolean jj_3R_110() {
if (jj_scan_token(RMIN)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
}
static final private boolean jj_3R_119() {
if (jj_scan_token(MAX)) return true;
static final private boolean jj_3R_124() {
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
@ -2981,49 +2955,36 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_66() {
if (jj_scan_token(TIMES)) return true;
static final private boolean jj_3R_56() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_64()) {
jj_scanpos = xsp;
if (jj_3R_65()) return true;
}
return false;
}
static final private boolean jj_3R_118() {
if (jj_scan_token(MIN)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
static final private boolean jj_3R_123() {
if (jj_3R_53()) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_117() {
static final private boolean jj_3R_119() {
if (jj_scan_token(MAX)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
}
static final private boolean jj_3R_57() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_66()) {
jj_scanpos = xsp;
if (jj_3R_67()) return true;
}
if (jj_3R_56()) return true;
return false;
}
static final private boolean jj_3_6() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
return false;
}
static final private boolean jj_3R_123() {
if (jj_3R_53()) return true;
if (jj_3R_33()) return true;
static final private boolean jj_3R_66() {
if (jj_scan_token(TIMES)) return true;
return false;
}
static final private boolean jj_3R_103() {
if (jj_scan_token(PMAX)) return true;
static final private boolean jj_3R_118() {
if (jj_scan_token(MIN)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
@ -3048,8 +3009,7 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_102() {
if (jj_scan_token(PMIN)) return true;
static final private boolean jj_3R_117() {
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
@ -3073,6 +3033,37 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_57() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_66()) {
jj_scanpos = xsp;
if (jj_3R_67()) return true;
}
if (jj_3R_56()) return true;
return false;
}
static final private boolean jj_3_6() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
return false;
}
static final private boolean jj_3R_103() {
if (jj_scan_token(PMAX)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
}
static final private boolean jj_3R_102() {
if (jj_scan_token(PMIN)) return true;
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
return false;
}
static final private boolean jj_3R_101() {
if (jj_scan_token(P)) return true;
Token xsp;
@ -3145,16 +3136,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_94() {
if (jj_3R_99()) return true;
return false;
}
static final private boolean jj_3R_93() {
if (jj_3R_98()) return true;
return false;
}
static final private boolean jj_3R_107() {
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
@ -3167,6 +3148,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_94() {
if (jj_3R_99()) return true;
return false;
}
static final private boolean jj_3R_93() {
if (jj_3R_98()) return true;
return false;
}
static final private boolean jj_3R_92() {
if (jj_3R_97()) return true;
return false;
@ -3182,11 +3173,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_91() {
if (jj_3R_27()) return true;
return false;
}
static final private boolean jj_3R_98() {
if (jj_scan_token(S)) return true;
Token xsp;
@ -3203,6 +3189,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_91() {
if (jj_3R_27()) return true;
return false;
}
static final private boolean jj_3R_80() {
Token xsp;
xsp = jj_scanpos;
@ -3231,6 +3222,21 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_149() {
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(COMMA)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static final private boolean jj_3R_148() {
if (jj_scan_token(GE)) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_46() {
if (jj_3R_48()) return true;
Token xsp;
@ -3241,18 +3247,22 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_146() {
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(COMMA)) return true;
static final private boolean jj_3R_147() {
if (jj_scan_token(LE)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static final private boolean jj_3R_145() {
if (jj_scan_token(GE)) return true;
if (jj_3R_33()) return true;
static final private boolean jj_3R_142() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_147()) {
jj_scanpos = xsp;
if (jj_3R_148()) {
jj_scanpos = xsp;
if (jj_3R_149()) return true;
}
}
return false;
}
@ -3270,25 +3280,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_144() {
if (jj_scan_token(LE)) return true;
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_139() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_144()) {
jj_scanpos = xsp;
if (jj_3R_145()) {
jj_scanpos = xsp;
if (jj_3R_146()) return true;
}
}
return false;
}
static final private boolean jj_3R_90() {
if (jj_scan_token(MAX)) return true;
return false;
@ -3362,6 +3353,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_63() {
if (jj_scan_token(LE)) return true;
return false;
}
static final private boolean jj_3R_41() {
Token xsp;
xsp = jj_scanpos;
@ -3372,11 +3368,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_63() {
if (jj_scan_token(LE)) return true;
return false;
}
static final private boolean jj_3R_62() {
if (jj_scan_token(GE)) return true;
return false;
@ -3408,13 +3399,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_87() {
if (jj_scan_token(MAX)) return true;
static final private boolean jj_3R_146() {
if (jj_3R_33()) return true;
return false;
}
static final private boolean jj_3R_143() {
if (jj_3R_33()) return true;
static final private boolean jj_3R_87() {
if (jj_scan_token(MAX)) return true;
return false;
}
@ -3424,31 +3415,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_39() {
if (jj_3R_41()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_42()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3_3() {
if (jj_scan_token(LABEL)) return true;
return false;
}
static final private boolean jj_3R_88() {
if (jj_3R_33()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_96()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3R_55() {
if (jj_scan_token(NE)) return true;
return false;
@ -3469,11 +3435,36 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_39() {
if (jj_3R_41()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_42()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3R_115() {
if (jj_scan_token(INIT)) return true;
return false;
}
static final private boolean jj_3_3() {
if (jj_scan_token(LABEL)) return true;
return false;
}
static final private boolean jj_3R_88() {
if (jj_3R_33()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_96()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3_2() {
if (jj_scan_token(LABEL)) return true;
if (jj_scan_token(DQUOTE)) return true;
@ -3514,13 +3505,18 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_5() {
if (jj_scan_token(DQUOTE)) return true;
static final private boolean jj_3R_32() {
if (jj_scan_token(REG_IDENTPRIME)) return true;
return false;
}
static final private boolean jj_3R_32() {
if (jj_scan_token(REG_IDENTPRIME)) return true;
static final private boolean jj_3R_141() {
if (jj_scan_token(R)) return true;
return false;
}
static final private boolean jj_3R_140() {
if (jj_scan_token(W)) return true;
return false;
}
@ -3529,12 +3525,32 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_139() {
if (jj_scan_token(U)) return true;
return false;
}
static final private boolean jj_3_5() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static final private boolean jj_3R_134() {
if (jj_scan_token(G)) return true;
return false;
}
static final private boolean jj_3R_38() {
if (jj_scan_token(IMPLIES)) return true;
if (jj_3R_37()) return true;
return false;
}
static final private boolean jj_3R_133() {
if (jj_scan_token(F)) return true;
return false;
}
static final private boolean jj_3R_35() {
if (jj_3R_37()) return true;
Token xsp;
@ -3550,13 +3566,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_134() {
if (jj_scan_token(G)) return true;
static final private boolean jj_3R_27() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static final private boolean jj_3R_133() {
if (jj_scan_token(F)) return true;
static final private boolean jj_3R_136() {
if (jj_3R_33()) return true;
return false;
}
@ -3573,19 +3589,22 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_132() {
if (jj_3R_33()) return true;
if (jj_scan_token(U)) return true;
return false;
}
static final private boolean jj_3R_27() {
if (jj_scan_token(REG_IDENT)) return true;
static final private boolean jj_3R_135() {
if (jj_3R_142()) return true;
return false;
}
static final private boolean jj_3R_136() {
static final private boolean jj_3R_132() {
if (jj_3R_33()) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_139()) {
jj_scanpos = xsp;
if (jj_3R_140()) {
jj_scanpos = xsp;
if (jj_3R_141()) return true;
}
}
return false;
}
@ -3594,11 +3613,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_135() {
if (jj_3R_139()) return true;
return false;
}
static final private boolean jj_3R_36() {
if (jj_scan_token(QMARK)) return true;
if (jj_3R_35()) return true;
@ -3622,14 +3636,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_76() {
if (jj_3R_27()) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_85()) jj_scanpos = xsp;
return false;
}
static final private boolean jj_3R_100() {
if (jj_scan_token(DQUOTE)) return true;
Token xsp;
@ -3642,11 +3648,44 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_76() {
if (jj_3R_27()) return true;
Token xsp;
xsp = jj_scanpos;
if (jj_3R_85()) jj_scanpos = xsp;
return false;
}
static final private boolean jj_3R_113() {
if (jj_3R_121()) return true;
return false;
}
static final private boolean jj_3_9() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static final private boolean jj_3R_120() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_131()) {
jj_scanpos = xsp;
if (jj_3R_132()) {
jj_scanpos = xsp;
if (jj_3R_133()) {
jj_scanpos = xsp;
if (jj_3R_134()) return true;
}
}
}
xsp = jj_scanpos;
if (jj_3R_135()) jj_scanpos = xsp;
xsp = jj_scanpos;
if (jj_3R_136()) jj_scanpos = xsp;
return false;
}
static private boolean jj_initialized_once = false;
static public PrismParserTokenManager token_source;
static SimpleCharStream jj_input_stream;
@ -3657,7 +3696,7 @@ public class PrismParser implements PrismParserConstants {
static public boolean lookingAhead = false;
static private boolean jj_semLA;
static private int jj_gen;
static final private int[] jj_la1 = new int[77];
static final private int[] jj_la1 = new int[78];
static private int[] jj_la1_0;
static private int[] jj_la1_1;
static private int[] jj_la1_2;
@ -3667,13 +3706,13 @@ public class PrismParser implements PrismParserConstants {
jj_la1_2();
}
private static void jj_la1_0() {
jj_la1_0 = new int[] {0x154a4130,0x11424130,0x4080000,0xe2c0a010,0x0,0xe2c0a010,0xe2c0a010,0x0,0xe2c0a010,0x11000120,0x200088,0x200088,0x0,0x10,0x0,0x80000,0x80000,0x8,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x2800000,0x2800000,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0xe280a000,0x0,0x2800000,0x2800000,0x0,0x2000,0xe0000000,0x2800000,0xe0000000,0x0,0x0,0x2800000,0xea85a000,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x2800000,0x0,0x0,0xe280a000,0x110040,0x80000,0x0,0x0,0x0,};
jj_la1_0 = new int[] {0x154a4130,0x11424130,0x4080000,0xe2c0a010,0x0,0xe2c0a010,0xe2c0a010,0x0,0xe2c0a010,0x11000120,0x200088,0x200088,0x0,0x10,0x0,0x80000,0x80000,0x8,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x2800000,0x2800000,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0xe280a000,0x0,0x2800000,0x2800000,0x0,0x2000,0xe0000000,0x2800000,0xe0000000,0x0,0x0,0x2800000,0x0,0xea85a000,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x2800000,0x0,0x0,0xe280a000,0x110040,0x80000,0x0,0x0,0x0,};
}
private static void jj_la1_1() {
jj_la1_1 = new int[] {0x30f,0x107,0x208,0x2014f6,0x40000,0x2014f6,0x2014f6,0x40000,0x2014f6,0x101,0x0,0x0,0x6,0x6,0x8000000,0x0,0x0,0x800000,0x0,0x800000,0x0,0x0,0x2014f0,0x2000,0x200400,0x80000,0x0,0x0,0xa014f0,0x0,0x800000,0x80000,0x2000000,0x80000,0x80000,0x2000000,0x200000,0x0,0x8000,0x4000,0x2000,0x2014f0,0x18000000,0xe0000000,0x0,0x0,0x0,0x0,0x2004f0,0x2004f0,0x200000,0x0,0x0,0x80000,0x400,0xf0,0xe8000000,0x0,0x2000000,0x2000000,0x0,0x2014f0,0x80800000,0x2014f0,0x80800000,0xe8000000,0x2000000,0x2000000,0xe8000000,0x70,0x2000000,0x2014f0,0x80,0x0,0x18000000,0xe0000000,0x20000,};
jj_la1_1 = new int[] {0x30f,0x107,0x208,0x4024f6,0x80000,0x4024f6,0x4024f6,0x80000,0x4024f6,0x101,0x0,0x0,0x6,0x6,0x10000000,0x0,0x0,0x1000000,0x0,0x1000000,0x0,0x0,0x4024f0,0x4000,0x400400,0x100000,0x0,0x0,0x14024f0,0x0,0x1000000,0x100000,0x4000000,0x100000,0x100000,0x4000000,0x400000,0x0,0x10000,0x8000,0x4000,0x4024f0,0x30000000,0xc0000000,0x0,0x0,0x0,0x0,0x4004f0,0x4004f0,0x400000,0x0,0x0,0x100000,0x400,0xf0,0xd0000000,0x0,0x4000000,0x4000000,0x0,0x1840,0x4024f0,0x1000000,0x4024f0,0x1000000,0xd0000000,0x4000000,0x4000000,0xd0000000,0x70,0x4000000,0x4024f0,0x80,0x0,0x30000000,0xc0000000,0x40000,};
}
private static void jj_la1_2() {
jj_la1_2 = new int[] {0x0,0x0,0x0,0x1704,0x0,0x1704,0x1704,0x0,0x1704,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x1000,0x0,0x1000,0x2,0x1704,0x0,0x0,0x0,0x1000,0x1000,0x1704,0x1000,0x0,0x0,0x10,0x0,0x0,0x10,0x1000,0x80,0x0,0x0,0x0,0x1704,0x0,0x1,0x6,0x6,0x18,0x18,0x1704,0x1700,0x0,0x0,0x1000,0x0,0x600,0x100,0x1,0x0,0x0,0x0,0x0,0x1704,0x1,0x1704,0x1,0x1,0x0,0x0,0x1,0x0,0x0,0x1704,0x0,0x1000,0x0,0x1,0x0,};
jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08,0x0,0x2e08,0x2e08,0x0,0x2e08,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x2000,0x0,0x2000,0x4,0x2e08,0x0,0x0,0x0,0x2000,0x2000,0x2e08,0x2000,0x0,0x0,0x20,0x0,0x0,0x20,0x2000,0x100,0x0,0x0,0x0,0x2e08,0x0,0x3,0xc,0xc,0x30,0x30,0x2e08,0x2e00,0x0,0x0,0x2000,0x0,0xc00,0x200,0x3,0x0,0x0,0x0,0x0,0x0,0x2e08,0x3,0x2e08,0x3,0x3,0x0,0x0,0x3,0x0,0x0,0x2e08,0x0,0x2000,0x0,0x3,0x0,};
}
static final private JJCalls[] jj_2_rtns = new JJCalls[9];
static private boolean jj_rescan = false;
@ -3695,7 +3734,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3708,7 +3747,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3725,7 +3764,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3735,7 +3774,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3751,7 +3790,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3760,7 +3799,7 @@ public class PrismParser implements PrismParserConstants {
token = new Token();
jj_ntk = -1;
jj_gen = 0;
for (int i = 0; i < 77; i++) jj_la1[i] = -1;
for (int i = 0; i < 78; i++) jj_la1[i] = -1;
for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
}
@ -3871,15 +3910,15 @@ public class PrismParser implements PrismParserConstants {
static public ParseException generateParseException() {
jj_expentries.removeAllElements();
boolean[] la1tokens = new boolean[79];
for (int i = 0; i < 79; i++) {
boolean[] la1tokens = new boolean[80];
for (int i = 0; i < 80; i++) {
la1tokens[i] = false;
}
if (jj_kind >= 0) {
la1tokens[jj_kind] = true;
jj_kind = -1;
}
for (int i = 0; i < 77; i++) {
for (int i = 0; i < 78; i++) {
if (jj_la1[i] == jj_gen) {
for (int j = 0; j < 32; j++) {
if ((jj_la1_0[i] & (1<<j)) != 0) {
@ -3894,7 +3933,7 @@ public class PrismParser implements PrismParserConstants {
}
}
}
for (int i = 0; i < 79; i++) {
for (int i = 0; i < 80; i++) {
if (la1tokens[i]) {
jj_expentry = new int[1];
jj_expentry[0] = i;

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

@ -373,6 +373,7 @@ TOKEN :
| < SYSTEM: "system" >
| < TRUE: "true" >
| < U: "U" >
| < W: "W" >
// Punctuation, etc.
// Note that "NOT" must be the first item of punctuation in this list
// (PrismSyntaxHighlighter relies on this fact)
@ -1314,7 +1315,7 @@ PathExpression ExpressionProbContents() :
{ return pe; }
}
// Temporal operarors (X, U, F, G)
// Temporal operarors (X, U, F, G, W, R)
PathExpression PathExpressionTemporal() :
{
@ -1328,7 +1329,11 @@ PathExpression PathExpressionTemporal() :
{ begin = getToken(0); }
(
<X> { pe.setOperator(PathExpressionTemporal.P_X); }
| expr1 = Expression() <U> { pe.setOperator(PathExpressionTemporal.P_U); }
| ( expr1 = Expression()
( <U> { pe.setOperator(PathExpressionTemporal.P_U); }
| <W> { pe.setOperator(PathExpressionTemporal.P_W); }
| <R> { pe.setOperator(PathExpressionTemporal.P_R); } )
)
| <F> { pe.setOperator(PathExpressionTemporal.P_F); }
| <G> { pe.setOperator(PathExpressionTemporal.P_G); }
)

72
prism/src/parser/PrismParserConstants.java
View File

@ -47,41 +47,42 @@ public interface PrismParserConstants {
int SYSTEM = 41;
int TRUE = 42;
int U = 43;
int NOT = 44;
int AND = 45;
int OR = 46;
int IMPLIES = 47;
int RARROW = 48;
int COLON = 49;
int SEMICOLON = 50;
int COMMA = 51;
int DOTS = 52;
int LPARENTH = 53;
int RPARENTH = 54;
int LBRACKET = 55;
int RBRACKET = 56;
int LBRACE = 57;
int RBRACE = 58;
int EQ = 59;
int NE = 60;
int LT = 61;
int GT = 62;
int LE = 63;
int GE = 64;
int PLUS = 65;
int MINUS = 66;
int TIMES = 67;
int DIVIDE = 68;
int PRIME = 69;
int RENAME = 70;
int QMARK = 71;
int DQUOTE = 72;
int REG_INT = 73;
int REG_DOUBLE = 74;
int REG_IDENTPRIME = 75;
int REG_IDENT = 76;
int PREPROC = 77;
int LEXICAL_ERROR = 78;
int W = 44;
int NOT = 45;
int AND = 46;
int OR = 47;
int IMPLIES = 48;
int RARROW = 49;
int COLON = 50;
int SEMICOLON = 51;
int COMMA = 52;
int DOTS = 53;
int LPARENTH = 54;
int RPARENTH = 55;
int LBRACKET = 56;
int RBRACKET = 57;
int LBRACE = 58;
int RBRACE = 59;
int EQ = 60;
int NE = 61;
int LT = 62;
int GT = 63;
int LE = 64;
int GE = 65;
int PLUS = 66;
int MINUS = 67;
int TIMES = 68;
int DIVIDE = 69;
int PRIME = 70;
int RENAME = 71;
int QMARK = 72;
int DQUOTE = 73;
int REG_INT = 74;
int REG_DOUBLE = 75;
int REG_IDENTPRIME = 76;
int REG_IDENT = 77;
int PREPROC = 78;
int LEXICAL_ERROR = 79;
int DEFAULT = 0;
@ -130,6 +131,7 @@ public interface PrismParserConstants {
"\"system\"",
"\"true\"",
"\"U\"",
"\"W\"",
"\"!\"",
"\"&\"",
"\"|\"",

207
prism/src/parser/PrismParserTokenManager.java
View File

@ -14,22 +14,22 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
switch (pos)
{
case 0:
if ((active0 & 0x8f0e8150040L) != 0L)
if ((active0 & 0x18f0e8150040L) != 0L)
return 23;
if ((active1 & 0x20L) != 0L)
return 1;
if ((active0 & 0x20000000000000L) != 0L)
return 11;
if ((active0 & 0x70f17eaffb8L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
return 23;
}
if ((active1 & 0x10L) != 0L)
return 1;
if ((active0 & 0x10000000000000L) != 0L)
return 11;
return -1;
case 1:
if ((active0 & 0x73f77eaffb8L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 1;
return 23;
}
@ -39,7 +39,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x73f744affb8L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 2;
return 23;
}
@ -51,7 +51,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
{
if (jjmatchedPos != 3)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 3;
}
return 23;
@ -62,7 +62,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x30914025e80L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 4;
return 23;
}
@ -72,7 +72,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x10910005e00L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 5;
return 23;
}
@ -82,7 +82,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x10110001c00L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 6;
return 23;
}
@ -90,7 +90,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 7:
if ((active0 & 0x10110001c00L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 7;
return 23;
}
@ -100,7 +100,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x10110000800L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 8;
return 23;
}
@ -110,7 +110,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
return 23;
if ((active0 & 0x110000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 9;
return 23;
}
@ -118,7 +118,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 10:
if ((active0 & 0x110000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 10;
return 23;
}
@ -126,25 +126,25 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 11:
if ((active0 & 0x110000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 11;
return 23;
}
return -1;
case 12:
if ((active0 & 0x100000000L) != 0L)
return 23;
if ((active0 & 0x10000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 12;
return 23;
}
if ((active0 & 0x100000000L) != 0L)
return 23;
return -1;
case 13:
if ((active0 & 0x10000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 13;
return 23;
}
@ -152,7 +152,7 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac
case 14:
if ((active0 & 0x10000000L) != 0L)
{
jjmatchedKind = 76;
jjmatchedKind = 77;
jjmatchedPos = 14;
return 23;
}
@ -184,46 +184,46 @@ static private final int jjMoveStringLiteralDfa0_0()
switch(curChar)
{
case 33:
jjmatchedKind = 44;
return jjMoveStringLiteralDfa1_0(0x1000000000000000L, 0x0L);
jjmatchedKind = 45;
return jjMoveStringLiteralDfa1_0(0x2000000000000000L, 0x0L);
case 34:
return jjStopAtPos(0, 72);
return jjStopAtPos(0, 73);
case 38:
return jjStopAtPos(0, 45);
return jjStopAtPos(0, 46);
case 39:
return jjStopAtPos(0, 69);
return jjStopAtPos(0, 70);
case 40:
return jjStopAtPos(0, 53);
case 41:
return jjStopAtPos(0, 54);
case 41:
return jjStopAtPos(0, 55);
case 42:
return jjStopAtPos(0, 67);
return jjStopAtPos(0, 68);
case 43:
return jjStopAtPos(0, 65);
return jjStopAtPos(0, 66);
case 44:
return jjStopAtPos(0, 51);
return jjStopAtPos(0, 52);
case 45:
jjmatchedKind = 66;
return jjMoveStringLiteralDfa1_0(0x1000000000000L, 0x0L);
jjmatchedKind = 67;
return jjMoveStringLiteralDfa1_0(0x2000000000000L, 0x0L);
case 46:
return jjMoveStringLiteralDfa1_0(0x10000000000000L, 0x0L);
return jjMoveStringLiteralDfa1_0(0x20000000000000L, 0x0L);
case 47:
return jjStartNfaWithStates_0(0, 68, 1);
return jjStartNfaWithStates_0(0, 69, 1);
case 58:
return jjStopAtPos(0, 49);
case 59:
return jjStopAtPos(0, 50);
case 59:
return jjStopAtPos(0, 51);
case 60:
jjmatchedKind = 61;
return jjMoveStringLiteralDfa1_0(0x8000000000000000L, 0x40L);
jjmatchedKind = 62;
return jjMoveStringLiteralDfa1_0(0x0L, 0x81L);
case 61:
jjmatchedKind = 59;
return jjMoveStringLiteralDfa1_0(0x800000000000L, 0x0L);
jjmatchedKind = 60;
return jjMoveStringLiteralDfa1_0(0x1000000000000L, 0x0L);
case 62:
jjmatchedKind = 62;
return jjMoveStringLiteralDfa1_0(0x0L, 0x1L);
jjmatchedKind = 63;
return jjMoveStringLiteralDfa1_0(0x0L, 0x2L);
case 63:
return jjStopAtPos(0, 71);
return jjStopAtPos(0, 72);
case 67:
return jjStartNfaWithStates_0(0, 6, 23);
case 70:
@ -242,12 +242,14 @@ static private final int jjMoveStringLiteralDfa0_0()
return jjStartNfaWithStates_0(0, 39, 23);
case 85:
return jjStartNfaWithStates_0(0, 43, 23);
case 87:
return jjStartNfaWithStates_0(0, 44, 23);
case 88:
return jjStartNfaWithStates_0(0, 27, 23);
case 91:
return jjStopAtPos(0, 55);
case 93:
return jjStopAtPos(0, 56);
case 93:
return jjStopAtPos(0, 57);
case 98:
return jjMoveStringLiteralDfa1_0(0x8L, 0x0L);
case 99:
@ -277,11 +279,11 @@ static private final int jjMoveStringLiteralDfa0_0()
case 116:
return jjMoveStringLiteralDfa1_0(0x40000000000L, 0x0L);
case 123:
return jjStopAtPos(0, 57);
return jjStopAtPos(0, 58);
case 124:
return jjStopAtPos(0, 46);
return jjStopAtPos(0, 47);
case 125:
return jjStopAtPos(0, 58);
return jjStopAtPos(0, 59);
default :
return jjMoveNfa_0(0, 0);
}
@ -296,26 +298,26 @@ static private final int jjMoveStringLiteralDfa1_0(long active0, long active1)
switch(curChar)
{
case 45:
if ((active1 & 0x40L) != 0L)
return jjStopAtPos(1, 70);
if ((active1 & 0x80L) != 0L)
return jjStopAtPos(1, 71);
break;
case 46:
if ((active0 & 0x10000000000000L) != 0L)
return jjStopAtPos(1, 52);
if ((active0 & 0x20000000000000L) != 0L)
return jjStopAtPos(1, 53);
break;
case 61:
if ((active0 & 0x1000000000000000L) != 0L)
return jjStopAtPos(1, 60);
else if ((active0 & 0x8000000000000000L) != 0L)
return jjStopAtPos(1, 63);
if ((active0 & 0x2000000000000000L) != 0L)
return jjStopAtPos(1, 61);
else if ((active1 & 0x1L) != 0L)
return jjStopAtPos(1, 64);
else if ((active1 & 0x2L) != 0L)
return jjStopAtPos(1, 65);
break;
case 62:
if ((active0 & 0x800000000000L) != 0L)
return jjStopAtPos(1, 47);
else if ((active0 & 0x1000000000000L) != 0L)
if ((active0 & 0x1000000000000L) != 0L)
return jjStopAtPos(1, 48);
else if ((active0 & 0x2000000000000L) != 0L)
return jjStopAtPos(1, 49);
break;
case 97:
return jjMoveStringLiteralDfa2_0(active0, 0x400c02000L, active1, 0L);
@ -840,14 +842,14 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 23:
if ((0x3ff000000000000L & l) != 0L)
{
if (kind > 76)
kind = 76;
if (kind > 77)
kind = 77;
jjCheckNAdd(22);
}
else if (curChar == 39)
{
if (kind > 75)
kind = 75;
if (kind > 76)
kind = 76;
}
if ((0x3ff000000000000L & l) != 0L)
jjCheckNAddTwoStates(20, 21);
@ -855,8 +857,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 0:
if ((0x3ff000000000000L & l) != 0L)
{
if (kind > 74)
kind = 74;
if (kind > 75)
kind = 75;
jjCheckNAddStates(0, 3);
}
else if ((0x100002600L & l) != 0L)
@ -872,14 +874,14 @@ static private final int jjMoveNfa_0(int startState, int curPos)
jjstateSet[jjnewStateCnt++] = 1;
if ((0x3fe000000000000L & l) != 0L)
{
if (kind > 73)
kind = 73;
if (kind > 74)
kind = 74;
jjCheckNAdd(8);
}
else if (curChar == 48)
{
if (kind > 73)
kind = 73;
if (kind > 74)
kind = 74;
}
break;
case 1:
@ -909,20 +911,20 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 7:
if ((0x3fe000000000000L & l) == 0L)
break;
if (kind > 73)
kind = 73;
if (kind > 74)
kind = 74;
jjCheckNAdd(8);
break;
case 8:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 73)
kind = 73;
if (kind > 74)
kind = 74;
jjCheckNAdd(8);
break;
case 9:
if (curChar == 48 && kind > 73)
kind = 73;
if (curChar == 48 && kind > 74)
kind = 74;
break;
case 10:
if (curChar == 46)
@ -931,8 +933,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 11:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 74)
kind = 74;
if (kind > 75)
kind = 75;
jjCheckNAddTwoStates(11, 12);
break;
case 13:
@ -942,8 +944,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 14:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 74)
kind = 74;
if (kind > 75)
kind = 75;
jjCheckNAdd(14);
break;
case 15:
@ -955,14 +957,14 @@ static private final int jjMoveNfa_0(int startState, int curPos)
jjCheckNAddTwoStates(16, 17);
break;
case 17:
if (curChar == 35 && kind > 77)
kind = 77;
if (curChar == 35 && kind > 78)
kind = 78;
break;
case 18:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 74)
kind = 74;
if (kind > 75)
kind = 75;
jjCheckNAddStates(0, 3);
break;
case 20:
@ -970,14 +972,14 @@ static private final int jjMoveNfa_0(int startState, int curPos)
jjCheckNAddTwoStates(20, 21);
break;
case 21:
if (curChar == 39 && kind > 75)
kind = 75;
if (curChar == 39 && kind > 76)
kind = 76;
break;
case 22:
if ((0x3ff000000000000L & l) == 0L)
break;
if (kind > 76)
kind = 76;
if (kind > 77)
kind = 77;
jjCheckNAdd(22);
break;
default : break;
@ -994,8 +996,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 23:
if ((0x7fffffe87fffffeL & l) != 0L)
{
if (kind > 76)
kind = 76;
if (kind > 77)
kind = 77;
jjCheckNAdd(22);
}
if ((0x7fffffe87fffffeL & l) != 0L)
@ -1004,8 +1006,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 0:
if ((0x7fffffe87fffffeL & l) == 0L)
break;
if (kind > 76)
kind = 76;
if (kind > 77)
kind = 77;
jjCheckNAddStates(7, 9);
break;
case 2:
@ -1025,8 +1027,8 @@ static private final int jjMoveNfa_0(int startState, int curPos)
case 22:
if ((0x7fffffe87fffffeL & l) == 0L)
break;
if (kind > 76)
kind = 76;
if (kind > 77)
kind = 77;
jjCheckNAdd(22);
break;
default : break;
@ -1080,15 +1082,16 @@ public static final String[] jjstrLiteralImages = {
"\156\157\156\144\145\164\145\162\155\151\156\151\163\164\151\143", "\120\155\141\170", "\120\155\151\156", "\120",
"\160\162\157\142\141\142\151\154\151\163\164\151\143", "\160\162\157\142", "\162\141\164\145", "\162\145\167\141\162\144\163",
"\122\155\141\170", "\122\155\151\156", "\122", "\123",
"\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\41", "\46", "\174",
"\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133", "\135", "\173",
"\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53", "\55", "\52", "\57",
"\47", "\74\55", "\77", "\42", null, null, null, null, null, null, };
"\163\164\157\143\150\141\163\164\151\143", "\163\171\163\164\145\155", "\164\162\165\145", "\125", "\127", "\41", "\46",
"\174", "\75\76", "\55\76", "\72", "\73", "\54", "\56\56", "\50", "\51", "\133",
"\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53",
"\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, null,
null, };
public static final String[] lexStateNames = {
"DEFAULT",
};
static final long[] jjtoToken = {
0xfffffffffffffff9L, 0x7fffL,
0xfffffffffffffff9L, 0xffffL,
};
static final long[] jjtoSkip = {
0x6L, 0x0L,
@ -1181,9 +1184,9 @@ public static Token getNextToken()
jjmatchedKind = 0x7fffffff;
jjmatchedPos = 0;
curPos = jjMoveStringLiteralDfa0_0();
if (jjmatchedPos == 0 && jjmatchedKind > 78)
if (jjmatchedPos == 0 && jjmatchedKind > 79)
{
jjmatchedKind = 78;
jjmatchedKind = 79;
}
if (jjmatchedKind != 0x7fffffff)
{

4
prism/src/parser/ast/Expression.java
View File

@ -164,6 +164,10 @@ public abstract class Expression extends ASTElement
public static Expression Int(int i) { return new ExpressionLiteral(Expression.INT, i); }
public static Expression Double(double d) { return new ExpressionLiteral(Expression.DOUBLE, d); }
public static Expression Not(Expression expr) { return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr); }
public static Expression And(Expression expr1, Expression expr2)
{ return new ExpressionBinaryOp(ExpressionBinaryOp.AND, expr1, expr2); }
public static Expression Or(Expression expr1, Expression expr2)
{ return new ExpressionBinaryOp(ExpressionBinaryOp.OR, expr1, expr2); }
public static Expression Parenth(Expression expr) { return new ExpressionUnaryOp(ExpressionUnaryOp.PARENTH, expr); }
}

28
prism/src/parser/ast/PathExpressionTemporal.java
View File

@ -36,13 +36,15 @@ public class PathExpressionTemporal extends PathExpression
public static final int P_U = 2; // Until (for P operator)
public static final int P_F = 3; // Future (for P operator)
public static final int P_G = 4; // Globally (for P operator)
public static final int P_W = 5; // Weak until (for P operator)
public static final int P_R = 6; // Release (for P operator)
public static final int R_C = 11; // Cumulative (for R operator)
public static final int R_I = 12; // Instantaneous (for R operator)
public static final int R_F = 13; // Reachability (for R operator)
public static final int R_S = 14; // Steady-state (for R operator)
// Operator symbols
public static final String opSymbols[] = { "",
"X", "U", "F", "G", "", "", "", "", "", "",
"X", "U", "F", "G", "W", "", "", "", "", "",
"C", "I", "F", "S"
};
@ -199,12 +201,12 @@ public class PathExpressionTemporal extends PathExpression
// Other useful methods
/**
* Convert (P operator) path formula to until form
* (using standard equivalences: F a=true U a, G a=!(true U!a)
* Convert (P operator) path formula to untils, using standard equivalences.
*/
public PathExpression convertToUntilForm() throws PrismLangException
{
PathExpression op1, op2, ret = null;
Expression a, b;
if (operand1 != null && !(operand1 instanceof PathExpressionExpr)) {
throw new PrismLangException("Cannot convert "+getOperatorSymbol()+" to until form");
}
@ -216,15 +218,35 @@ public class PathExpressionTemporal extends PathExpression
ret = this;
break;
case P_F:
// F a == true U a
op1 = new PathExpressionExpr(Expression.True());
ret = new PathExpressionTemporal(P_U, op1, operand2, lBound, uBound);
break;
case P_G:
// G a == !(true U !a)
op1 = new PathExpressionExpr(Expression.True());
op2 = new PathExpressionExpr(Expression.Not(((PathExpressionExpr)operand2).getExpression()));
ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound);
ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret);
break;
case P_W:
// a W b == !(a&!b U !a&!b)
a = ((PathExpressionExpr)operand1).getExpression();
b = ((PathExpressionExpr)operand2).getExpression();
op1 = new PathExpressionExpr(Expression.And(a, Expression.Not(b)));
op2 = new PathExpressionExpr(Expression.And(Expression.Not(a), Expression.Not(b)));
ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound);
ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret);
break;
case P_R:
// a R b == !(!a U !b)
a = ((PathExpressionExpr)operand1).getExpression();
b = ((PathExpressionExpr)operand2).getExpression();
op1 = new PathExpressionExpr(Expression.Not(a));
op2 = new PathExpressionExpr(Expression.Not(b));
ret = new PathExpressionTemporal(P_U, op1, op2, lBound, uBound);
ret = new PathExpressionLogical(PathExpressionLogical.NOT, null, ret);
break;
default:
throw new PrismLangException("Cannot convert "+getOperatorSymbol()+" to until form");
}

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

@ -406,6 +406,8 @@ public class TypeCheck extends ASTTraverse
case PathExpressionTemporal.P_U:
case PathExpressionTemporal.P_F:
case PathExpressionTemporal.P_G:
case PathExpressionTemporal.P_W:
case PathExpressionTemporal.P_R:
e.setType(Expression.BOOLEAN);
break;
case PathExpressionTemporal.R_C:

Write Preview
Loading…
Cancel
Save