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

Slightly improved version of just-improved parsing of bounded temporal operators. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@712 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
f8de8dbda3
commit
39085ddc40
2 changed files with 109 additions and 107 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. 210
      prism/src/parser/PrismParser.java
  2. 6
      prism/src/parser/PrismParser.jj

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

@ -2097,7 +2097,7 @@ public class PrismParser implements PrismParserConstants {
// To prevent (very common) cases such as "F<=t (b)", "F<=t (b)&(c)", etc.
// being mis-parsed ("t(b)" would always be taken over "t"), we catch this case
// separately. This means that more complex time-bounds, especially those that
// include an identifier should be parenthesised, e.g. "F<=(t1+t2)".
// start/end with an identifier should be parenthesised, e.g. "F<=(t1+t2)".
static final public Expression ExpressionTemporal() throws ParseException {
ExpressionTemporal expr = new ExpressionTemporal();
Expression expr1 = null, expr2 = null;
@ -2244,7 +2244,7 @@ public class PrismParser implements PrismParserConstants {
case REG_INT:
case REG_DOUBLE:
case REG_IDENT:
tb.uBound = Expression();
tb.lBound = Expression();
break;
default:
jj_la1[65] = jj_gen;
@ -2690,16 +2690,6 @@ public class PrismParser implements PrismParserConstants {
finally { jj_save(10, xla); }
}
static final private boolean jj_3R_60() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static final private boolean jj_3R_27() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static final private boolean jj_3R_137() {
if (jj_scan_token(LBRACE)) return true;
Token xsp;
@ -2734,22 +2724,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_31() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(EQ)) return true;
if (jj_3R_34()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static final private boolean jj_3_7() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
return false;
}
static final private boolean jj_3R_122() {
if (jj_scan_token(LBRACE)) return true;
if (jj_3R_34()) return true;
@ -2773,6 +2747,22 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_31() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_33()) return true;
if (jj_scan_token(EQ)) return true;
if (jj_3R_34()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static final private boolean jj_3_7() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
return false;
}
static final private boolean jj_3R_101() {
if (jj_scan_token(DQUOTE)) return true;
Token xsp;
@ -2785,21 +2775,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_30() {
if (jj_3R_31()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_32()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3_4() {
if (jj_3R_28()) return true;
return false;
}
static final private boolean jj_3R_117() {
if (jj_3R_54()) return true;
if (jj_3R_34()) return true;
@ -2811,16 +2786,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_28() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_30()) {
jj_scanpos = xsp;
if (jj_scan_token(42)) return true;
}
return false;
}
static final private boolean jj_3R_57() {
Token xsp;
xsp = jj_scanpos;
@ -2843,6 +2808,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_30() {
if (jj_3R_31()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_32()) { jj_scanpos = xsp; break; }
}
return false;
}
static final private boolean jj_3R_67() {
if (jj_scan_token(TIMES)) return true;
return false;
@ -2855,6 +2830,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_4() {
if (jj_3R_28()) return true;
return false;
}
static final private boolean jj_3R_118() {
if (jj_scan_token(EQ)) return true;
if (jj_scan_token(QMARK)) return true;
@ -2877,9 +2857,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_6() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
static final private boolean jj_3R_28() {
Token xsp;
xsp = jj_scanpos;
if (jj_3R_30()) {
jj_scanpos = xsp;
if (jj_scan_token(42)) return true;
}
return false;
}
@ -2975,6 +2959,12 @@ public class PrismParser implements PrismParserConstants {
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_52() {
if (jj_3R_57()) return true;
Token xsp;
@ -2985,14 +2975,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_8() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(LBRACKET)) return true;
static final private boolean jj_3R_59() {
if (jj_scan_token(PLUS)) return true;
return false;
}
static final private boolean jj_3R_59() {
if (jj_scan_token(PLUS)) return true;
static final private boolean jj_3R_153() {
if (jj_3R_34()) return true;
return false;
}
@ -3007,6 +2996,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_151() {
if (jj_3R_34()) return true;
return false;
}
static final private boolean jj_3R_138() {
if (jj_scan_token(LBRACE)) return true;
Token xsp;
@ -3029,6 +3023,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_8() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(LBRACKET)) return true;
return false;
}
static final private boolean jj_3R_94() {
if (jj_3R_99()) return true;
return false;
@ -3049,16 +3049,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_153() {
if (jj_3R_34()) return true;
return false;
}
static final private boolean jj_3R_151() {
if (jj_3R_34()) return true;
return false;
}
static final private boolean jj_3R_123() {
if (jj_3R_138()) return true;
return false;
@ -3201,13 +3191,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_1() {
if (jj_scan_token(MODULE)) return true;
if (jj_3R_27()) return true;
if (jj_scan_token(EQ)) return true;
return false;
}
static final private boolean jj_3R_48() {
if (jj_3R_51()) return true;
if (jj_3R_47()) return true;
@ -3224,6 +3207,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_1() {
if (jj_scan_token(MODULE)) return true;
if (jj_3R_27()) return true;
if (jj_scan_token(EQ)) return true;
return false;
}
static final private boolean jj_3R_85() {
if (jj_scan_token(FALSE)) return true;
return false;
@ -3304,6 +3294,12 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_10() {
if (jj_3R_29()) return true;
if (jj_scan_token(LPARENTH)) return true;
return false;
}
static final private boolean jj_3R_42() {
Token xsp;
xsp = jj_scanpos;
@ -3314,13 +3310,9 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_10() {
if (jj_3R_29()) return true;
return false;
}
static final private boolean jj_3_9() {
if (jj_3R_29()) return true;
if (jj_scan_token(LPARENTH)) return true;
return false;
}
@ -3401,11 +3393,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_3() {
if (jj_scan_token(LABEL)) return true;
return false;
}
static final private boolean jj_3R_141() {
if (jj_scan_token(R)) return true;
return false;
@ -3434,12 +3421,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_2() {
if (jj_scan_token(LABEL)) return true;
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static final private boolean jj_3R_41() {
if (jj_scan_token(OR)) return true;
if (jj_3R_40()) return true;
@ -3456,6 +3437,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_3() {
if (jj_scan_token(LABEL)) return true;
return false;
}
static final private boolean jj_3R_38() {
if (jj_3R_40()) return true;
Token xsp;
@ -3503,13 +3489,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_132() {
if (jj_scan_token(X)) return true;
static final private boolean jj_3_2() {
if (jj_scan_token(LABEL)) return true;
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static final private boolean jj_3_5() {
if (jj_scan_token(DQUOTE)) return true;
static final private boolean jj_3R_132() {
if (jj_scan_token(X)) return true;
return false;
}
@ -3534,6 +3521,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3_5() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static final private boolean jj_3R_78() {
Token xsp;
xsp = jj_scanpos;
@ -3693,12 +3685,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_32() {
if (jj_scan_token(AND)) return true;
if (jj_3R_31()) return true;
return false;
}
static final private boolean jj_3R_72() {
if (jj_3R_78()) return true;
return false;
@ -3739,6 +3725,22 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static final private boolean jj_3R_32() {
if (jj_scan_token(AND)) return true;
if (jj_3R_31()) return true;
return false;
}
static final private boolean jj_3R_60() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static final private boolean jj_3R_27() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static private boolean jj_initialized_once = false;
static public PrismParserTokenManager token_source;
static SimpleCharStream jj_input_stream;

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

@ -1344,7 +1344,7 @@ Expression ExpressionProbContents() :
// To prevent (very common) cases such as "F<=t (b)", "F<=t (b)&(c)", etc.
// being mis-parsed ("t(b)" would always be taken over "t"), we catch this case
// separately. This means that more complex time-bounds, especially those that
// include an identifier should be parenthesised, e.g. "F<=(t1+t2)".
// start/end with an identifier should be parenthesised, e.g. "F<=(t1+t2)".
Expression ExpressionTemporal() :
{
@ -1386,8 +1386,8 @@ TimeBound TimeBound() :
TimeBound tb = new TimeBound();
}
{
( <LE> ( LOOKAHEAD(ExpressionIdent()) tb.uBound = ExpressionIdent() | tb.uBound = Expression() )
| <GE> ( LOOKAHEAD(ExpressionIdent()) tb.lBound = ExpressionIdent() | tb.uBound = Expression() )
( <LE> ( LOOKAHEAD(ExpressionIdent() <LPARENTH>) tb.uBound = ExpressionIdent() | tb.uBound = Expression() )
| <GE> ( LOOKAHEAD(ExpressionIdent() <LPARENTH>) tb.lBound = ExpressionIdent() | tb.lBound = Expression() )
| <LBRACKET> tb.lBound = Expression() <COMMA> tb.uBound = Expression() <RBRACKET> )
{ return tb; }
}

Write Preview
Loading…
Cancel
Save