From 9ecd00a5496e9cc1054023596ab5f1ab44d9f566 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 28 Nov 2008 10:53:58 +0000 Subject: [PATCH] Added CTL operators to the parser. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@830 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 774 ++++++++++-------- prism/src/parser/PrismParser.jj | 46 +- prism/src/parser/PrismParserConstants.java | 158 ++-- prism/src/parser/PrismParserTokenManager.java | 580 ++++++------- prism/src/parser/ast/ExpressionExists.java | 115 +++ prism/src/parser/ast/ExpressionForAll.java | 115 +++ prism/src/parser/visitor/ASTTraverse.java | 20 + .../src/parser/visitor/ASTTraverseModify.java | 20 + prism/src/parser/visitor/ASTVisitor.java | 2 + prism/src/parser/visitor/Rename.java | 14 + prism/src/parser/visitor/TypeCheck.java | 10 + 11 files changed, 1148 insertions(+), 706 deletions(-) create mode 100644 prism/src/parser/ast/ExpressionExists.java create mode 100644 prism/src/parser/ast/ExpressionForAll.java diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 416513b2..af4c33ae 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -444,7 +444,9 @@ public class PrismParser implements PrismParserConstants { label_2: while (true) { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: case CONST: + case E: case FALSE: case FUNC: case LABEL: @@ -474,6 +476,8 @@ public class PrismParser implements PrismParserConstants { break label_2; } switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case MAX: @@ -537,7 +541,9 @@ public class PrismParser implements PrismParserConstants { label_4: while (true) { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: case CONST: + case E: case FALSE: case FUNC: case LABEL: @@ -567,6 +573,8 @@ public class PrismParser implements PrismParserConstants { break label_4; } switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case MAX: @@ -925,6 +933,8 @@ public class PrismParser implements PrismParserConstants { updates.addUpdate(null, update); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case F: @@ -1112,6 +1122,8 @@ public class PrismParser implements PrismParserConstants { label_11: while (true) { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case F: @@ -1541,6 +1553,8 @@ public class PrismParser implements PrismParserConstants { expr = ExpressionTemporalUnary(prop, pathprop); exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; break; + case A: + case E: case FALSE: case FUNC: case MAX: @@ -1582,6 +1596,8 @@ public class PrismParser implements PrismParserConstants { tb.uBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case F: @@ -1619,6 +1635,8 @@ public class PrismParser implements PrismParserConstants { tb.lBound = IdentifierExpression(); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case F: @@ -1770,6 +1788,8 @@ public class PrismParser implements PrismParserConstants { expr = ExpressionNot(prop, pathprop); ret = new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr); ret.setPosition(begin, getToken(0)); break; + case A: + case E: case FALSE: case FUNC: case MAX: @@ -1948,6 +1968,8 @@ public class PrismParser implements PrismParserConstants { expr = ExpressionUnaryMinus(prop, pathprop); ret = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, expr); ret.setPosition(begin, getToken(0)); break; + case A: + case E: case FALSE: case FUNC: case MAX: @@ -2013,6 +2035,12 @@ public class PrismParser implements PrismParserConstants { case R: ret = ExpressionReward(prop, pathprop); break; + case E: + ret = ExpressionExists(prop, pathprop); + break; + case A: + ret = ExpressionForAll(prop, pathprop); + break; case DQUOTE: ret = ExpressionLabel(prop, pathprop); break; @@ -2468,6 +2496,8 @@ public class PrismParser implements PrismParserConstants { jj_consume_token(DQUOTE); } else { switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { + case A: + case E: case FALSE: case FUNC: case F: @@ -2539,6 +2569,38 @@ public class PrismParser implements PrismParserConstants { throw new Error("Missing return statement in function"); } +// (Property) expression: CTL existential operator E + static final public Expression ExpressionExists(boolean prop, boolean pathprop) throws ParseException { + ExpressionExists ret = new ExpressionExists(); + Expression expr; + Token begin = null; + if (!prop) {if (true) throw generateParseException();} + begin = jj_consume_token(E); + jj_consume_token(LBRACKET); + expr = Expression(prop, true); + jj_consume_token(RBRACKET); + ret.setExpression(expr); + ret.setPosition(begin, getToken(0)); + {if (true) return ret;} + throw new Error("Missing return statement in function"); + } + +// (Property) expression: CTL universal operator A + static final public Expression ExpressionForAll(boolean prop, boolean pathprop) throws ParseException { + ExpressionForAll ret = new ExpressionForAll(); + Expression expr; + Token begin = null; + if (!prop) {if (true) throw generateParseException();} + begin = jj_consume_token(A); + jj_consume_token(LBRACKET); + expr = Expression(prop, true); + jj_consume_token(RBRACKET); + ret.setExpression(expr); + ret.setPosition(begin, getToken(0)); + {if (true) return ret;} + throw new Error("Missing return statement in function"); + } + // (Property) expression: label (including "init") static final public Expression ExpressionLabel(boolean prop, boolean pathprop) throws ParseException { String s; @@ -2751,25 +2813,8 @@ public class PrismParser implements PrismParserConstants { finally { jj_save(10, xla); } } - static final private boolean jj_3R_67() { - if (jj_3R_68()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_69()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3R_108() { - if (jj_scan_token(DQUOTE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_132()) { - jj_scanpos = xsp; - if (jj_3R_133()) return true; - } - if (jj_scan_token(DQUOTE)) return true; + static final private boolean jj_3R_114() { + if (jj_scan_token(REG_DOUBLE)) return true; return false; } @@ -2789,8 +2834,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_110() { - if (jj_scan_token(REG_DOUBLE)) return true; + static final private boolean jj_3R_121() { + if (jj_scan_token(MIN)) return true; return false; } @@ -2799,29 +2844,65 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3_11() { + if (jj_scan_token(DQUOTE)) return true; + return false; + } + static final private boolean jj_3R_65() { if (jj_scan_token(NOT)) return true; if (jj_3R_63()) return true; return false; } - static final private boolean jj_3R_117() { - if (jj_scan_token(MIN)) return true; + static final private boolean jj_3R_152() { + if (jj_scan_token(S)) return true; return false; } - static final private boolean jj_3_11() { - if (jj_scan_token(DQUOTE)) return true; + static final private boolean jj_3R_113() { + if (jj_scan_token(REG_INT)) return true; return false; } - static final private boolean jj_3R_148() { - if (jj_scan_token(S)) return true; + static final private boolean jj_3R_151() { + if (jj_scan_token(F)) return true; + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_109() { - if (jj_scan_token(REG_INT)) return true; + static final private boolean jj_3R_102() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_113()) { + jj_scanpos = xsp; + if (jj_3R_114()) { + jj_scanpos = xsp; + if (jj_3R_115()) { + jj_scanpos = xsp; + if (jj_3R_116()) return true; + } + } + } + return false; + } + + static final private boolean jj_3R_150() { + if (jj_scan_token(I)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_3R_34()) return true; + return false; + } + + static final private boolean jj_3R_149() { + if (jj_scan_token(C)) return true; + if (jj_scan_token(LE)) return true; + if (jj_3R_34()) return true; + return false; + } + + static final private boolean jj_3R_119() { + if (jj_scan_token(MAX)) return true; return false; } @@ -2835,22 +2916,23 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_147() { - if (jj_scan_token(F)) return true; - if (jj_3R_34()) return true; + static final private boolean jj_3R_157() { + if (jj_scan_token(DQUOTE)) return true; + if (jj_3R_27()) return true; + if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3R_100() { + static final private boolean jj_3R_134() { Token xsp; xsp = jj_scanpos; - if (jj_3R_109()) { + if (jj_3R_149()) { jj_scanpos = xsp; - if (jj_3R_110()) { + if (jj_3R_150()) { jj_scanpos = xsp; - if (jj_3R_111()) { + if (jj_3R_151()) { jj_scanpos = xsp; - if (jj_3R_112()) return true; + if (jj_3R_152()) return true; } } } @@ -2862,13 +2944,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_146() { - if (jj_scan_token(I)) return true; - if (jj_scan_token(EQ)) return true; - if (jj_3R_34()) return true; - return false; - } - static final private boolean jj_3R_63() { Token xsp; xsp = jj_scanpos; @@ -2879,47 +2954,22 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_145() { - if (jj_scan_token(C)) return true; - if (jj_scan_token(LE)) return true; - if (jj_3R_34()) return true; - 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; + if (jj_scan_token(44)) return true; } return false; } - static final private boolean jj_3R_115() { - if (jj_scan_token(MAX)) return true; - return false; - } - - static final private boolean jj_3R_153() { - if (jj_scan_token(DQUOTE)) return true; - if (jj_3R_27()) return true; - if (jj_scan_token(DQUOTE)) return true; - return false; - } - - static final private boolean jj_3R_130() { + static final private boolean jj_3R_120() { + if (jj_3R_34()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_145()) { - jj_scanpos = xsp; - if (jj_3R_146()) { - jj_scanpos = xsp; - if (jj_3R_147()) { - jj_scanpos = xsp; - if (jj_3R_148()) return true; - } - } + while (true) { + xsp = jj_scanpos; + if (jj_3R_138()) { jj_scanpos = xsp; break; } } return false; } @@ -2930,58 +2980,48 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_116() { - if (jj_3R_34()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_134()) { jj_scanpos = xsp; break; } - } - return false; - } - static final private boolean jj_3R_64() { if (jj_scan_token(AND)) return true; if (jj_3R_63()) return true; return false; } - static final private boolean jj_3R_61() { - if (jj_3R_63()) return true; + static final private boolean jj_3R_154() { + if (jj_scan_token(LBRACE)) return true; Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_64()) { jj_scanpos = xsp; break; } + xsp = jj_scanpos; + if (jj_3R_157()) { + jj_scanpos = xsp; + if (jj_3R_158()) return true; } + if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3R_150() { - if (jj_scan_token(LBRACE)) return true; + static final private boolean jj_3R_61() { + if (jj_3R_63()) return true; Token xsp; - xsp = jj_scanpos; - if (jj_3R_153()) { - jj_scanpos = xsp; - if (jj_3R_154()) return true; + while (true) { + xsp = jj_scanpos; + if (jj_3R_64()) { jj_scanpos = xsp; break; } } - if (jj_scan_token(RBRACE)) return true; return false; } - static final private boolean jj_3R_103() { + static final private boolean jj_3R_105() { if (jj_scan_token(FUNC)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_117()) { + if (jj_3R_121()) { jj_scanpos = xsp; - if (jj_3R_118()) { + if (jj_3R_122()) { jj_scanpos = xsp; - if (jj_3R_119()) return true; + if (jj_3R_123()) return true; } } if (jj_scan_token(COMMA)) return true; - if (jj_3R_116()) return true; + if (jj_3R_120()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } @@ -2992,12 +3032,22 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_130() { + if (jj_3R_143()) return true; + return false; + } + static final private boolean jj_3R_62() { if (jj_scan_token(OR)) return true; if (jj_3R_61()) return true; return false; } + static final private boolean jj_3R_144() { + if (jj_3R_154()) return true; + return false; + } + static final private boolean jj_3R_55() { if (jj_3R_61()) return true; Token xsp; @@ -3008,74 +3058,70 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_126() { - if (jj_3R_139()) return true; - return false; - } - - static final private boolean jj_3R_140() { - if (jj_3R_150()) return true; - return false; - } - - static final private boolean jj_3R_114() { + static final private boolean jj_3R_118() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3R_102() { + static final private boolean jj_3R_104() { Token xsp; xsp = jj_scanpos; - if (jj_3R_114()) { + if (jj_3R_118()) { jj_scanpos = xsp; - if (jj_3R_115()) return true; + if (jj_3R_119()) return true; } if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_116()) return true; + if (jj_3R_120()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3R_56() { - if (jj_scan_token(IMPLIES)) return true; - if (jj_3R_55()) return true; - return false; - } - - static final private boolean jj_3R_144() { + static final private boolean jj_3R_148() { 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_129() { + static final private boolean jj_3R_133() { if (jj_scan_token(RMAX)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_143() { + static final private boolean jj_3R_147() { if (jj_scan_token(MIN)) return true; if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_128() { + static final private boolean jj_3R_132() { 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_142() { + static final private boolean jj_3R_146() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } + static final private boolean jj_3R_56() { + if (jj_scan_token(IMPLIES)) return true; + if (jj_3R_55()) return true; + return false; + } + + static final private boolean jj_3R_145() { + if (jj_3R_75()) return true; + if (jj_3R_34()) return true; + return false; + } + static final private boolean jj_3R_50() { if (jj_3R_55()) return true; Token xsp; @@ -3086,75 +3132,69 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_141() { - if (jj_3R_75()) return true; - if (jj_3R_34()) return true; - return false; - } - - static final private boolean jj_3R_127() { + static final private boolean jj_3R_131() { if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_140()) jj_scanpos = xsp; + if (jj_3R_144()) jj_scanpos = xsp; xsp = jj_scanpos; - if (jj_3R_141()) { + if (jj_3R_145()) { jj_scanpos = xsp; - if (jj_3R_142()) { + if (jj_3R_146()) { jj_scanpos = xsp; - if (jj_3R_143()) { + if (jj_3R_147()) { jj_scanpos = xsp; - if (jj_3R_144()) return true; + if (jj_3R_148()) return true; } } } return false; } - static final private boolean jj_3R_51() { - if (jj_scan_token(QMARK)) return true; - if (jj_3R_50()) return true; - if (jj_scan_token(COLON)) return true; - if (jj_3R_48()) return true; - return false; - } - - static final private boolean jj_3R_113() { + static final private boolean jj_3R_117() { if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_116()) return true; + if (jj_3R_120()) return true; if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3R_107() { + static final private boolean jj_3R_109() { Token xsp; xsp = jj_scanpos; - if (jj_3R_127()) { + if (jj_3R_131()) { jj_scanpos = xsp; - if (jj_3R_128()) { + if (jj_3R_132()) { jj_scanpos = xsp; - if (jj_3R_129()) return true; + if (jj_3R_133()) return true; } } if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_130()) return true; + if (jj_3R_134()) return true; xsp = jj_scanpos; - if (jj_3R_131()) jj_scanpos = xsp; + if (jj_3R_135()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3_10() { - if (jj_3R_29()) return true; - if (jj_scan_token(LPARENTH)) return true; + static final private boolean jj_3R_51() { + if (jj_scan_token(QMARK)) return true; + if (jj_3R_50()) return true; + if (jj_scan_token(COLON)) return true; + if (jj_3R_48()) return true; return false; } - static final private boolean jj_3R_101() { + static final private boolean jj_3R_103() { if (jj_3R_27()) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_113()) jj_scanpos = xsp; + if (jj_3R_117()) jj_scanpos = xsp; + return false; + } + + static final private boolean jj_3_10() { + if (jj_3R_29()) return true; + if (jj_scan_token(LPARENTH)) return true; return false; } @@ -3177,11 +3217,21 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_101() { + if (jj_3R_112()) return true; + return false; + } + static final private boolean jj_3R_57() { if (jj_3R_29()) return true; return false; } + static final private boolean jj_3R_100() { + if (jj_3R_111()) return true; + return false; + } + static final private boolean jj_3_1() { if (jj_scan_token(MODULE)) return true; if (jj_3R_27()) return true; @@ -3189,8 +3239,20 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_129() { + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; + return false; + } + static final private boolean jj_3R_99() { - if (jj_3R_108()) return true; + if (jj_3R_110()) return true; + return false; + } + + static final private boolean jj_3R_128() { + if (jj_3R_75()) return true; + if (jj_3R_34()) return true; return false; } @@ -3209,7 +3271,7 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_98() { - if (jj_3R_107()) return true; + if (jj_3R_109()) return true; return false; } @@ -3235,20 +3297,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_125() { - if (jj_scan_token(EQ)) return true; - if (jj_scan_token(QMARK)) return true; + static final private boolean jj_3R_85() { + if (jj_scan_token(LE)) return true; return false; } static final private boolean jj_3R_97() { - if (jj_3R_106()) return true; + if (jj_3R_108()) return true; return false; } - static final private boolean jj_3R_124() { - if (jj_3R_75()) return true; - if (jj_3R_34()) return true; + static final private boolean jj_3R_84() { + if (jj_scan_token(GE)) return true; return false; } @@ -3265,13 +3325,39 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_83() { + if (jj_scan_token(LT)) return true; + return false; + } + static final private boolean jj_3R_96() { - if (jj_3R_105()) return true; + if (jj_3R_107()) return true; + return false; + } + + static final private boolean jj_3R_75() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_82()) { + jj_scanpos = xsp; + if (jj_3R_83()) { + jj_scanpos = xsp; + if (jj_3R_84()) { + jj_scanpos = xsp; + if (jj_3R_85()) return true; + } + } + } + return false; + } + + static final private boolean jj_3R_82() { + if (jj_scan_token(GT)) return true; return false; } static final private boolean jj_3R_95() { - if (jj_3R_104()) return true; + if (jj_3R_106()) return true; return false; } @@ -3281,7 +3367,28 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_94() { - if (jj_3R_103()) return true; + if (jj_3R_105()) return true; + return false; + } + + static final private boolean jj_3R_127() { + if (jj_3R_143()) return true; + return false; + } + + static final private boolean jj_3R_108() { + if (jj_scan_token(S)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_128()) { + jj_scanpos = xsp; + if (jj_3R_129()) return true; + } + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_34()) return true; + xsp = jj_scanpos; + if (jj_3R_130()) jj_scanpos = xsp; + if (jj_scan_token(RBRACKET)) return true; return false; } @@ -3291,7 +3398,7 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_93() { - if (jj_3R_102()) return true; + if (jj_3R_104()) return true; return false; } @@ -3306,7 +3413,7 @@ public class PrismParser implements PrismParserConstants { } static final private boolean jj_3R_92() { - if (jj_3R_101()) return true; + if (jj_3R_103()) return true; return false; } @@ -3315,29 +3422,28 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_123() { - if (jj_3R_139()) return true; + static final private boolean jj_3R_77() { + if (jj_scan_token(NE)) return true; return false; } - static final private boolean jj_3R_106() { - if (jj_scan_token(S)) return true; + static final private boolean jj_3R_72() { Token xsp; xsp = jj_scanpos; - if (jj_3R_124()) { + if (jj_3R_76()) { jj_scanpos = xsp; - if (jj_3R_125()) return true; + if (jj_3R_77()) return true; } - if (jj_scan_token(LBRACKET)) return true; - if (jj_3R_34()) return true; - xsp = jj_scanpos; - if (jj_3R_126()) jj_scanpos = xsp; - if (jj_scan_token(RBRACKET)) return true; + return false; + } + + static final private boolean jj_3R_76() { + if (jj_scan_token(EQ)) return true; return false; } static final private boolean jj_3R_91() { - if (jj_3R_100()) return true; + if (jj_3R_102()) return true; return false; } @@ -3362,12 +3468,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_152() { + static final private boolean jj_3R_156() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_151() { + static final private boolean jj_3R_155() { if (jj_scan_token(MIN)) return true; return false; } @@ -3391,7 +3497,13 @@ public class PrismParser implements PrismParserConstants { jj_scanpos = xsp; if (jj_3R_98()) { jj_scanpos = xsp; - if (jj_3R_99()) return true; + if (jj_3R_99()) { + jj_scanpos = xsp; + if (jj_3R_100()) { + jj_scanpos = xsp; + if (jj_3R_101()) return true; + } + } } } } @@ -3418,26 +3530,48 @@ public class PrismParser implements PrismParserConstants { return false; } + static final private boolean jj_3R_153() { + if (jj_scan_token(LBRACE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_155()) { + jj_scanpos = xsp; + if (jj_3R_156()) return true; + } + if (jj_scan_token(RBRACE)) return true; + return false; + } + + static final private boolean jj_3R_137() { + if (jj_scan_token(INIT)) return true; + return false; + } + static final private boolean jj_3R_86() { if (jj_scan_token(MINUS)) return true; if (jj_3R_78()) return true; return false; } + static final private boolean jj_3R_143() { + if (jj_scan_token(LBRACE)) return true; + if (jj_3R_34()) return true; + if (jj_scan_token(RBRACE)) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_153()) { jj_scanpos = xsp; break; } + } + return false; + } + static final private boolean jj_3R_43() { if (jj_3R_49()) return true; return false; } - static final private boolean jj_3R_149() { - if (jj_scan_token(LBRACE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_151()) { - jj_scanpos = xsp; - if (jj_3R_152()) return true; - } - if (jj_scan_token(RBRACE)) return true; + static final private boolean jj_3R_33() { + if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } @@ -3456,18 +3590,6 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_139() { - if (jj_scan_token(LBRACE)) return true; - if (jj_3R_34()) return true; - if (jj_scan_token(RBRACE)) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_149()) { jj_scanpos = xsp; break; } - } - return false; - } - static final private boolean jj_3R_37() { Token xsp; xsp = jj_scanpos; @@ -3499,18 +3621,19 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_85() { - if (jj_scan_token(LE)) return true; + static final private boolean jj_3R_29() { + if (jj_3R_27()) return true; return false; } - static final private boolean jj_3R_88() { - if (jj_scan_token(TIMES)) return true; + static final private boolean jj_3R_139() { + if (jj_3R_75()) return true; + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_84() { - if (jj_scan_token(GE)) return true; + static final private boolean jj_3R_88() { + if (jj_scan_token(TIMES)) return true; return false; } @@ -3520,8 +3643,8 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_83() { - if (jj_scan_token(LT)) return true; + static final private boolean jj_3R_136() { + if (jj_3R_27()) return true; return false; } @@ -3536,30 +3659,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_75() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_82()) { - jj_scanpos = xsp; - if (jj_3R_83()) { - jj_scanpos = xsp; - if (jj_3R_84()) { - jj_scanpos = xsp; - if (jj_3R_85()) return true; - } - } - } - return false; - } - - static final private boolean jj_3R_82() { - if (jj_scan_token(GT)) return true; + static final private boolean jj_3R_142() { + 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_135() { - if (jj_3R_75()) return true; - if (jj_3R_34()) return true; + static final private boolean jj_3R_141() { + if (jj_scan_token(MIN)) return true; + if (jj_scan_token(EQ)) return true; + if (jj_scan_token(QMARK)) return true; return false; } @@ -3571,33 +3681,33 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_138() { - if (jj_scan_token(MAX)) return true; + static final private boolean jj_3R_140() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_137() { - if (jj_scan_token(MIN)) return true; + static final private boolean jj_3R_126() { + 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_3_5() { - if (jj_scan_token(DQUOTE)) 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_136() { + static final private boolean jj_3R_125() { + 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_77() { - if (jj_scan_token(NE)) return true; + static final private boolean jj_3_5() { + if (jj_scan_token(DQUOTE)) return true; return false; } @@ -3611,104 +3721,82 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_72() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_76()) { - jj_scanpos = xsp; - if (jj_3R_77()) return true; - } - return false; - } - - static final private boolean jj_3R_76() { - if (jj_scan_token(EQ)) return true; - return false; - } - - static final private boolean jj_3R_122() { - 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_121() { - 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_80() { - if (jj_scan_token(PLUS)) return true; - return false; - } - - static final private boolean jj_3R_154() { + static final private boolean jj_3R_158() { if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_120() { + static final private boolean jj_3R_124() { if (jj_scan_token(P)) return true; Token xsp; xsp = jj_scanpos; - if (jj_3R_135()) { + if (jj_3R_139()) { jj_scanpos = xsp; - if (jj_3R_136()) { + if (jj_3R_140()) { jj_scanpos = xsp; - if (jj_3R_137()) { + if (jj_3R_141()) { jj_scanpos = xsp; - if (jj_3R_138()) return true; + if (jj_3R_142()) return true; } } } return false; } - static final private boolean jj_3R_74() { - Token xsp; - xsp = jj_scanpos; - if (jj_3R_80()) { - jj_scanpos = xsp; - if (jj_3R_81()) return true; - } - if (jj_3R_73()) return true; + static final private boolean jj_3R_80() { + if (jj_scan_token(PLUS)) return true; return false; } - static final private boolean jj_3R_105() { + static final private boolean jj_3R_107() { Token xsp; xsp = jj_scanpos; - if (jj_3R_120()) { + if (jj_3R_124()) { jj_scanpos = xsp; - if (jj_3R_121()) { + if (jj_3R_125()) { jj_scanpos = xsp; - if (jj_3R_122()) return true; + if (jj_3R_126()) return true; } } if (jj_scan_token(LBRACKET)) return true; if (jj_3R_34()) return true; xsp = jj_scanpos; - if (jj_3R_123()) jj_scanpos = xsp; + if (jj_3R_127()) jj_scanpos = xsp; if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3R_134() { + static final private boolean jj_3R_74() { + Token xsp; + xsp = jj_scanpos; + if (jj_3R_80()) { + jj_scanpos = xsp; + if (jj_3R_81()) return true; + } + if (jj_3R_73()) return true; + return false; + } + + static final private boolean jj_3R_138() { if (jj_scan_token(COMMA)) return true; if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_133() { - if (jj_scan_token(INIT)) return true; + static final private boolean jj_3R_123() { + if (jj_3R_27()) return true; return false; } - static final private boolean jj_3R_119() { - if (jj_3R_27()) return true; + static final private boolean jj_3R_112() { + if (jj_scan_token(DQUOTE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_136()) { + jj_scanpos = xsp; + if (jj_3R_137()) return true; + } + if (jj_scan_token(DQUOTE)) return true; return false; } @@ -3722,30 +3810,28 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_33() { - if (jj_scan_token(REG_IDENTPRIME)) return true; - return false; - } - static final private boolean jj_3R_34() { if (jj_3R_35()) return true; return false; } - static final private boolean jj_3R_29() { - if (jj_3R_27()) return true; + static final private boolean jj_3R_106() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_34()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3R_132() { - if (jj_3R_27()) return true; + static final private boolean jj_3R_111() { + if (jj_scan_token(A)) return true; + if (jj_scan_token(LBRACKET)) return true; + if (jj_3R_34()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3R_104() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_34()) return true; - if (jj_scan_token(RPARENTH)) return true; + static final private boolean jj_3R_122() { + if (jj_scan_token(MAX)) return true; return false; } @@ -3765,13 +3851,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_118() { - if (jj_scan_token(MAX)) return true; + static final private boolean jj_3R_135() { + if (jj_3R_143()) 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_116() { + if (jj_scan_token(FALSE)) return true; return false; } @@ -3781,34 +3867,42 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_131() { - if (jj_3R_139()) return true; + static final private boolean jj_3R_115() { + if (jj_scan_token(TRUE)) return true; return false; } - static final private boolean jj_3R_112() { - if (jj_scan_token(FALSE)) return true; + static final private boolean jj_3R_60() { + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_60() { + static final private boolean jj_3R_58() { if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_111() { - if (jj_scan_token(TRUE)) return true; + static final private boolean jj_3R_69() { + if (jj_3R_72()) return true; + if (jj_3R_68()) return true; return false; } - static final private boolean jj_3R_58() { + static final private boolean jj_3R_110() { + if (jj_scan_token(E)) return true; + if (jj_scan_token(LBRACKET)) return true; if (jj_3R_34()) return true; + if (jj_scan_token(RBRACKET)) return true; return false; } - static final private boolean jj_3R_69() { - if (jj_3R_72()) return true; + static final private boolean jj_3R_67() { if (jj_3R_68()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_69()) { jj_scanpos = xsp; break; } + } return false; } @@ -3832,13 +3926,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,0xea85a000,0x0,0x0,0x0,0x2800000,0x2800000,0xea85a000,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x8050000,0x0,0xea85a000,0xea85a000,0xea85a000,0x0,0x0,0x0,0x0,0x0,0xe280a000,0x0,0x0,0x0,0x0,0x0,0x0,0xe280a000,0xe280a000,0x0,0x2800000,0x2800000,0x0,0x2000,0x2800000,0xe0000000,0x0,0x0,0x2800000,0x0,0x0,0x0,0x2800000,0x0,0x0,0xea85a000,0x110040,0x80000,0x0,0x0,0x0,}; + jj_la1_0 = new int[] {0x55290260,0x45090260,0x10200000,0x8b028428,0x0,0x8b028428,0x8b028428,0x0,0x8b028428,0x44000240,0x800110,0x800110,0x0,0x20,0x0,0x200000,0x200000,0x10,0x0,0x0,0x0,0x0,0xaa168408,0x0,0x0,0x0,0xa000000,0xa000000,0xaa168408,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x20140000,0x0,0xaa168408,0xaa168408,0xaa168408,0x0,0x0,0x0,0x0,0x0,0x8a028408,0x0,0x0,0x0,0x0,0x0,0x0,0x8a028408,0x8a028408,0x0,0xa000000,0xa000000,0x0,0x8000,0xa000000,0x80000000,0x0,0x0,0xa000000,0x0,0x0,0x0,0xa000000,0x0,0x0,0xaa168408,0x440080,0x200000,0x0,0x0,0x0,}; } private static void jj_la1_1() { - 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,0x1840,0x1000000,0x1840,0x0,0x1000000,0x4024f0,0x4024f0,0x4024f0,0x1000000,0x0,0x10000,0x8000,0x4000,0x4024f0,0x30000000,0xc0000000,0x0,0x0,0x0,0x0,0x4004f0,0x4004f0,0x400000,0x0,0x0,0x100000,0x400,0xd0000000,0x0,0x4000000,0x4000000,0x0,0xd0000000,0x4000000,0x4000000,0xd0000000,0x70,0x4000000,0x4024f0,0x80,0x0,0x30000000,0xc0000000,0x40000,}; + jj_la1_1 = new int[] {0xc3c,0x41c,0x820,0x10093db,0x200000,0x10093db,0x10093db,0x200000,0x10093db,0x404,0x0,0x0,0x18,0x18,0x40000000,0x0,0x0,0x4000000,0x0,0x4000000,0x0,0x0,0x10093c3,0x10000,0x1001000,0x400000,0x0,0x0,0x50093c3,0x0,0x4000000,0x400000,0x10000000,0x400000,0x400000,0x10000000,0x1000000,0x6100,0x4000000,0x6100,0x0,0x4000000,0x10093c3,0x10093c3,0x10093c3,0x4000000,0x0,0x40000,0x20000,0x10000,0x10093c3,0xc0000000,0x0,0x0,0x0,0x0,0x0,0x10013c3,0x10013c3,0x1000000,0x0,0x0,0x400000,0x1000,0x40000000,0x3,0x10000000,0x10000000,0x0,0x40000000,0x10000000,0x10000000,0x40000000,0x1c0,0x10000000,0x10093c3,0x200,0x0,0xc0000000,0x0,0x100000,}; } private static void jj_la1_2() { - 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,0x0,0x3,0x0,0x0,0x3,0x2e08,0x2e08,0x2e08,0x3,0x100,0x0,0x0,0x0,0x2e08,0x0,0x3,0xc,0xc,0x30,0x30,0x2e08,0x2e00,0x0,0x0,0x2000,0x0,0xc00,0x3,0x0,0x0,0x0,0x0,0x3,0x0,0x0,0x3,0x0,0x0,0x2e08,0x0,0x2000,0x0,0x3,0x0,}; + jj_la1_2 = new int[] {0x0,0x0,0x0,0xb820,0x0,0xb820,0xb820,0x0,0xb820,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x8000,0x0,0x8000,0x10,0xb820,0x0,0x0,0x0,0x8000,0x8000,0xb820,0x8000,0x0,0x0,0x80,0x0,0x0,0x80,0x8000,0x0,0xc,0x0,0x0,0xc,0xb820,0xb820,0xb820,0xc,0x400,0x0,0x0,0x0,0xb820,0x0,0xf,0x30,0x30,0xc0,0xc0,0xb820,0xb800,0x0,0x0,0x8000,0x0,0x3000,0xf,0x0,0x0,0x0,0x0,0xf,0x0,0x0,0xf,0x0,0x0,0xb820,0x0,0x8000,0x0,0xf,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[11]; static private boolean jj_rescan = false; @@ -4036,8 +4130,8 @@ public class PrismParser implements PrismParserConstants { static public ParseException generateParseException() { jj_expentries.removeAllElements(); - boolean[] la1tokens = new boolean[80]; - for (int i = 0; i < 80; i++) { + boolean[] la1tokens = new boolean[82]; + for (int i = 0; i < 82; i++) { la1tokens[i] = false; } if (jj_kind >= 0) { @@ -4059,7 +4153,7 @@ public class PrismParser implements PrismParserConstants { } } } - for (int i = 0; i < 80; i++) { + for (int i = 0; i < 82; i++) { if (la1tokens[i]) { jj_expentry = new int[1]; jj_expentry[0] = i; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index 5f66c996..7a9a18b7 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -352,12 +352,14 @@ SPECIAL_TOKEN : TOKEN : { // Keywords - < BOOL: "bool" > + < A: "A" > +| < BOOL: "bool" > | < CONST: "const" > | < CTMC: "ctmc" > | < C: "C" > | < DOUBLE: "double" > | < DTMC: "dtmc" > +| < E: "E" > | < ENDINIT: "endinit" > | < ENDMODULE: "endmodule" > | < ENDREWARDS: "endrewards" > @@ -1233,6 +1235,10 @@ Expression ExpressionBasic(boolean prop, boolean pathprop) : ret = ExpressionSS(prop, pathprop) | ret = ExpressionReward(prop, pathprop) + | + ret = ExpressionExists(prop, pathprop) + | + ret = ExpressionForAll(prop, pathprop) | ret = ExpressionLabel(prop, pathprop) ) @@ -1501,6 +1507,44 @@ Expression ExpressionRewardContents(boolean prop, boolean pathprop) : { ret.setPosition(begin, getToken(0)); return ret; } } +// (Property) expression: CTL existential operator E + +Expression ExpressionExists(boolean prop, boolean pathprop) : +{ + ExpressionExists ret = new ExpressionExists(); + Expression expr; + Token begin = null; +} +{ + // This production is only allowed in expressions if the "prop" parameter is true + { if (!prop) throw generateParseException(); } + ( begin = expr = Expression(prop, true) ) + { + ret.setExpression(expr); + ret.setPosition(begin, getToken(0)); + return ret; + } +} + +// (Property) expression: CTL universal operator A + +Expression ExpressionForAll(boolean prop, boolean pathprop) : +{ + ExpressionForAll ret = new ExpressionForAll(); + Expression expr; + Token begin = null; +} +{ + // This production is only allowed in expressions if the "prop" parameter is true + { if (!prop) throw generateParseException(); } + ( begin = expr = Expression(prop, true) ) + { + ret.setExpression(expr); + ret.setPosition(begin, getToken(0)); + return ret; + } +} + // (Property) expression: label (including "init") Expression ExpressionLabel(boolean prop, boolean pathprop) : diff --git a/prism/src/parser/PrismParserConstants.java b/prism/src/parser/PrismParserConstants.java index 65a03e88..e4e741e1 100644 --- a/prism/src/parser/PrismParserConstants.java +++ b/prism/src/parser/PrismParserConstants.java @@ -6,83 +6,85 @@ public interface PrismParserConstants { int EOF = 0; int WHITESPACE = 1; int COMMENT = 2; - int BOOL = 3; - int CONST = 4; - int CTMC = 5; - int C = 6; - int DOUBLE = 7; - int DTMC = 8; - int ENDINIT = 9; - int ENDMODULE = 10; - int ENDREWARDS = 11; - int ENDSYSTEM = 12; - int FALSE = 13; - int FORMULA = 14; - int FUNC = 15; - int F = 16; - int GLOBAL = 17; - int G = 18; - int INIT = 19; - int I = 20; - int INT = 21; - int LABEL = 22; - int MAX = 23; - int MDP = 24; - int MIN = 25; - int MODULE = 26; - int X = 27; - int NONDETERMINISTIC = 28; - int PMAX = 29; - int PMIN = 30; - int P = 31; - int PROBABILISTIC = 32; - int PROB = 33; - int RATE = 34; - int REWARDS = 35; - int RMAX = 36; - int RMIN = 37; - int R = 38; - int S = 39; - int STOCHASTIC = 40; - int SYSTEM = 41; - int TRUE = 42; - int U = 43; - 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 A = 3; + int BOOL = 4; + int CONST = 5; + int CTMC = 6; + int C = 7; + int DOUBLE = 8; + int DTMC = 9; + int E = 10; + int ENDINIT = 11; + int ENDMODULE = 12; + int ENDREWARDS = 13; + int ENDSYSTEM = 14; + int FALSE = 15; + int FORMULA = 16; + int FUNC = 17; + int F = 18; + int GLOBAL = 19; + int G = 20; + int INIT = 21; + int I = 22; + int INT = 23; + int LABEL = 24; + int MAX = 25; + int MDP = 26; + int MIN = 27; + int MODULE = 28; + int X = 29; + int NONDETERMINISTIC = 30; + int PMAX = 31; + int PMIN = 32; + int P = 33; + int PROBABILISTIC = 34; + int PROB = 35; + int RATE = 36; + int REWARDS = 37; + int RMAX = 38; + int RMIN = 39; + int R = 40; + int S = 41; + int STOCHASTIC = 42; + int SYSTEM = 43; + int TRUE = 44; + int U = 45; + int W = 46; + int NOT = 47; + int AND = 48; + int OR = 49; + int IMPLIES = 50; + int RARROW = 51; + int COLON = 52; + int SEMICOLON = 53; + int COMMA = 54; + int DOTS = 55; + int LPARENTH = 56; + int RPARENTH = 57; + int LBRACKET = 58; + int RBRACKET = 59; + int LBRACE = 60; + int RBRACE = 61; + int EQ = 62; + int NE = 63; + int LT = 64; + int GT = 65; + int LE = 66; + int GE = 67; + int PLUS = 68; + int MINUS = 69; + int TIMES = 70; + int DIVIDE = 71; + int PRIME = 72; + int RENAME = 73; + int QMARK = 74; + int DQUOTE = 75; + int REG_INT = 76; + int REG_DOUBLE = 77; + int REG_IDENTPRIME = 78; + int REG_IDENT = 79; + int PREPROC = 80; + int LEXICAL_ERROR = 81; int DEFAULT = 0; @@ -90,12 +92,14 @@ public interface PrismParserConstants { "", "", "", + "\"A\"", "\"bool\"", "\"const\"", "\"ctmc\"", "\"C\"", "\"double\"", "\"dtmc\"", + "\"E\"", "\"endinit\"", "\"endmodule\"", "\"endrewards\"", diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index 3e65f62a..f98890f7 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -14,145 +14,145 @@ private static final int jjStopStringLiteralDfa_0(int pos, long active0, long ac switch (pos) { case 0: - if ((active0 & 0x18f0e8150040L) != 0L) + if ((active0 & 0x63c3a0540488L) != 0L) return 23; - if ((active1 & 0x20L) != 0L) - return 1; - if ((active0 & 0x20000000000000L) != 0L) - return 11; - if ((active0 & 0x70f17eaffb8L) != 0L) + if ((active0 & 0x1c3c5fabfb70L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; return 23; } + if ((active1 & 0x80L) != 0L) + return 1; + if ((active0 & 0x80000000000000L) != 0L) + return 11; return -1; case 1: - if ((active0 & 0x73f77eaffb8L) != 0L) + if ((active0 & 0x1cfddfabfb70L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 1; return 23; } return -1; case 2: - if ((active0 & 0x3a00000L) != 0L) + if ((active0 & 0xe800000L) != 0L) return 23; - if ((active0 & 0x73f744affb8L) != 0L) + if ((active0 & 0x1cfdd12bfb70L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 2; return 23; } return -1; case 3: - if ((active0 & 0x43760088128L) != 0L) + if ((active0 & 0x10dd80220250L) != 0L) return 23; - if ((active0 & 0x30814427e90L) != 0L) + if ((active0 & 0xc205109f920L) != 0L) { if (jjmatchedPos != 3) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 3; } return 23; } return -1; case 4: - if ((active0 & 0x402010L) != 0L) + if ((active0 & 0x1008020L) != 0L) return 23; - if ((active0 & 0x30914025e80L) != 0L) + if ((active0 & 0xc2450097900L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 4; return 23; } return -1; case 5: - if ((active0 & 0x20004020080L) != 0L) + if ((active0 & 0x80010080100L) != 0L) return 23; - if ((active0 & 0x10910005e00L) != 0L) + if ((active0 & 0x42440017800L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 5; return 23; } return -1; case 6: - if ((active0 & 0x800004200L) != 0L) + if ((active0 & 0x2000010800L) != 0L) return 23; - if ((active0 & 0x10110001c00L) != 0L) + if ((active0 & 0x40440007000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 6; return 23; } return -1; case 7: - if ((active0 & 0x10110001c00L) != 0L) + if ((active0 & 0x40440007000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 7; return 23; } return -1; case 8: - if ((active0 & 0x1400L) != 0L) + if ((active0 & 0x5000L) != 0L) return 23; - if ((active0 & 0x10110000800L) != 0L) + if ((active0 & 0x40440002000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 8; return 23; } return -1; case 9: - if ((active0 & 0x10000000800L) != 0L) + if ((active0 & 0x40000002000L) != 0L) return 23; - if ((active0 & 0x110000000L) != 0L) + if ((active0 & 0x440000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 9; return 23; } return -1; case 10: - if ((active0 & 0x110000000L) != 0L) + if ((active0 & 0x440000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 10; return 23; } return -1; case 11: - if ((active0 & 0x110000000L) != 0L) + if ((active0 & 0x440000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 11; return 23; } return -1; case 12: - if ((active0 & 0x100000000L) != 0L) + if ((active0 & 0x400000000L) != 0L) return 23; - if ((active0 & 0x10000000L) != 0L) + if ((active0 & 0x40000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 12; return 23; } return -1; case 13: - if ((active0 & 0x10000000L) != 0L) + if ((active0 & 0x40000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 13; return 23; } return -1; case 14: - if ((active0 & 0x10000000L) != 0L) + if ((active0 & 0x40000000L) != 0L) { - jjmatchedKind = 77; + jjmatchedKind = 79; jjmatchedPos = 14; return 23; } @@ -184,106 +184,110 @@ static private final int jjMoveStringLiteralDfa0_0() switch(curChar) { case 33: - jjmatchedKind = 45; - return jjMoveStringLiteralDfa1_0(0x2000000000000000L, 0x0L); + jjmatchedKind = 47; + return jjMoveStringLiteralDfa1_0(0x8000000000000000L, 0x0L); case 34: - return jjStopAtPos(0, 73); + return jjStopAtPos(0, 75); case 38: - return jjStopAtPos(0, 46); + return jjStopAtPos(0, 48); case 39: - return jjStopAtPos(0, 70); + return jjStopAtPos(0, 72); case 40: - return jjStopAtPos(0, 54); + return jjStopAtPos(0, 56); case 41: - return jjStopAtPos(0, 55); + return jjStopAtPos(0, 57); case 42: - return jjStopAtPos(0, 68); + return jjStopAtPos(0, 70); case 43: - return jjStopAtPos(0, 66); + return jjStopAtPos(0, 68); case 44: - return jjStopAtPos(0, 52); + return jjStopAtPos(0, 54); case 45: - jjmatchedKind = 67; - return jjMoveStringLiteralDfa1_0(0x2000000000000L, 0x0L); + jjmatchedKind = 69; + return jjMoveStringLiteralDfa1_0(0x8000000000000L, 0x0L); case 46: - return jjMoveStringLiteralDfa1_0(0x20000000000000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x80000000000000L, 0x0L); case 47: - return jjStartNfaWithStates_0(0, 69, 1); + return jjStartNfaWithStates_0(0, 71, 1); case 58: - return jjStopAtPos(0, 50); + return jjStopAtPos(0, 52); case 59: - return jjStopAtPos(0, 51); + return jjStopAtPos(0, 53); case 60: - jjmatchedKind = 62; - return jjMoveStringLiteralDfa1_0(0x0L, 0x81L); + jjmatchedKind = 64; + return jjMoveStringLiteralDfa1_0(0x0L, 0x204L); case 61: - jjmatchedKind = 60; - return jjMoveStringLiteralDfa1_0(0x1000000000000L, 0x0L); + jjmatchedKind = 62; + return jjMoveStringLiteralDfa1_0(0x4000000000000L, 0x0L); case 62: - jjmatchedKind = 63; - return jjMoveStringLiteralDfa1_0(0x0L, 0x2L); + jjmatchedKind = 65; + return jjMoveStringLiteralDfa1_0(0x0L, 0x8L); case 63: - return jjStopAtPos(0, 72); + return jjStopAtPos(0, 74); + case 65: + return jjStartNfaWithStates_0(0, 3, 23); case 67: - return jjStartNfaWithStates_0(0, 6, 23); + return jjStartNfaWithStates_0(0, 7, 23); + case 69: + return jjStartNfaWithStates_0(0, 10, 23); case 70: - return jjStartNfaWithStates_0(0, 16, 23); - case 71: return jjStartNfaWithStates_0(0, 18, 23); - case 73: + case 71: return jjStartNfaWithStates_0(0, 20, 23); + case 73: + return jjStartNfaWithStates_0(0, 22, 23); case 80: - jjmatchedKind = 31; - return jjMoveStringLiteralDfa1_0(0x60000000L, 0x0L); + jjmatchedKind = 33; + return jjMoveStringLiteralDfa1_0(0x180000000L, 0x0L); case 82: - jjmatchedKind = 38; - return jjMoveStringLiteralDfa1_0(0x3000000000L, 0x0L); + jjmatchedKind = 40; + return jjMoveStringLiteralDfa1_0(0xc000000000L, 0x0L); case 83: - return jjStartNfaWithStates_0(0, 39, 23); + return jjStartNfaWithStates_0(0, 41, 23); case 85: - return jjStartNfaWithStates_0(0, 43, 23); + return jjStartNfaWithStates_0(0, 45, 23); case 87: - return jjStartNfaWithStates_0(0, 44, 23); + return jjStartNfaWithStates_0(0, 46, 23); case 88: - return jjStartNfaWithStates_0(0, 27, 23); + return jjStartNfaWithStates_0(0, 29, 23); case 91: - return jjStopAtPos(0, 56); + return jjStopAtPos(0, 58); case 93: - return jjStopAtPos(0, 57); + return jjStopAtPos(0, 59); case 98: - return jjMoveStringLiteralDfa1_0(0x8L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x10L, 0x0L); case 99: - return jjMoveStringLiteralDfa1_0(0x30L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x60L, 0x0L); case 100: - return jjMoveStringLiteralDfa1_0(0x180L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x300L, 0x0L); case 101: - return jjMoveStringLiteralDfa1_0(0x1e00L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x7800L, 0x0L); case 102: - return jjMoveStringLiteralDfa1_0(0xe000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x38000L, 0x0L); case 103: - return jjMoveStringLiteralDfa1_0(0x20000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x80000L, 0x0L); case 105: - return jjMoveStringLiteralDfa1_0(0x280000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0xa00000L, 0x0L); case 108: - return jjMoveStringLiteralDfa1_0(0x400000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x1000000L, 0x0L); case 109: - return jjMoveStringLiteralDfa1_0(0x7800000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x1e000000L, 0x0L); case 110: - return jjMoveStringLiteralDfa1_0(0x10000000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x40000000L, 0x0L); case 112: - return jjMoveStringLiteralDfa1_0(0x300000000L, 0x0L); - case 114: return jjMoveStringLiteralDfa1_0(0xc00000000L, 0x0L); + case 114: + return jjMoveStringLiteralDfa1_0(0x3000000000L, 0x0L); case 115: - return jjMoveStringLiteralDfa1_0(0x30000000000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0xc0000000000L, 0x0L); case 116: - return jjMoveStringLiteralDfa1_0(0x40000000000L, 0x0L); + return jjMoveStringLiteralDfa1_0(0x100000000000L, 0x0L); case 123: - return jjStopAtPos(0, 58); + return jjStopAtPos(0, 60); case 124: - return jjStopAtPos(0, 47); + return jjStopAtPos(0, 49); case 125: - return jjStopAtPos(0, 59); + return jjStopAtPos(0, 61); default : return jjMoveNfa_0(0, 0); } @@ -298,51 +302,51 @@ static private final int jjMoveStringLiteralDfa1_0(long active0, long active1) switch(curChar) { case 45: - if ((active1 & 0x80L) != 0L) - return jjStopAtPos(1, 71); + if ((active1 & 0x200L) != 0L) + return jjStopAtPos(1, 73); break; case 46: - if ((active0 & 0x20000000000000L) != 0L) - return jjStopAtPos(1, 53); + if ((active0 & 0x80000000000000L) != 0L) + return jjStopAtPos(1, 55); break; case 61: - 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); + if ((active0 & 0x8000000000000000L) != 0L) + return jjStopAtPos(1, 63); + else if ((active1 & 0x4L) != 0L) + return jjStopAtPos(1, 66); + else if ((active1 & 0x8L) != 0L) + return jjStopAtPos(1, 67); break; case 62: - if ((active0 & 0x1000000000000L) != 0L) - return jjStopAtPos(1, 48); - else if ((active0 & 0x2000000000000L) != 0L) - return jjStopAtPos(1, 49); + if ((active0 & 0x4000000000000L) != 0L) + return jjStopAtPos(1, 50); + else if ((active0 & 0x8000000000000L) != 0L) + return jjStopAtPos(1, 51); break; case 97: - return jjMoveStringLiteralDfa2_0(active0, 0x400c02000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x1003008000L, active1, 0L); case 100: - return jjMoveStringLiteralDfa2_0(active0, 0x1000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x4000000L, active1, 0L); case 101: - return jjMoveStringLiteralDfa2_0(active0, 0x800000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x2000000000L, active1, 0L); case 105: - return jjMoveStringLiteralDfa2_0(active0, 0x2000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x8000000L, active1, 0L); case 108: - return jjMoveStringLiteralDfa2_0(active0, 0x20000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x80000L, active1, 0L); case 109: - return jjMoveStringLiteralDfa2_0(active0, 0x3060000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0xc180000000L, active1, 0L); case 110: - return jjMoveStringLiteralDfa2_0(active0, 0x281e00L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0xa07800L, active1, 0L); case 111: - return jjMoveStringLiteralDfa2_0(active0, 0x14004098L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x50010130L, active1, 0L); case 114: - return jjMoveStringLiteralDfa2_0(active0, 0x40300000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x100c00000000L, active1, 0L); case 116: - return jjMoveStringLiteralDfa2_0(active0, 0x10000000120L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x40000000240L, active1, 0L); case 117: - return jjMoveStringLiteralDfa2_0(active0, 0x8000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x20000L, active1, 0L); case 121: - return jjMoveStringLiteralDfa2_0(active0, 0x20000000000L, active1, 0L); + return jjMoveStringLiteralDfa2_0(active0, 0x80000000000L, active1, 0L); default : break; } @@ -360,42 +364,42 @@ static private final int jjMoveStringLiteralDfa2_0(long old0, long active0, long switch(curChar) { case 97: - return jjMoveStringLiteralDfa3_0(active0, 0x1020000000L); + return jjMoveStringLiteralDfa3_0(active0, 0x4080000000L); case 98: - return jjMoveStringLiteralDfa3_0(active0, 0x400000L); + return jjMoveStringLiteralDfa3_0(active0, 0x1000000L); case 100: - return jjMoveStringLiteralDfa3_0(active0, 0x4001e00L); + return jjMoveStringLiteralDfa3_0(active0, 0x10007800L); case 105: - return jjMoveStringLiteralDfa3_0(active0, 0x2040080000L); + return jjMoveStringLiteralDfa3_0(active0, 0x8100200000L); case 108: - return jjMoveStringLiteralDfa3_0(active0, 0x2000L); + return jjMoveStringLiteralDfa3_0(active0, 0x8000L); case 109: - return jjMoveStringLiteralDfa3_0(active0, 0x120L); + return jjMoveStringLiteralDfa3_0(active0, 0x240L); case 110: - if ((active0 & 0x2000000L) != 0L) - return jjStartNfaWithStates_0(2, 25, 23); - return jjMoveStringLiteralDfa3_0(active0, 0x10008010L); + if ((active0 & 0x8000000L) != 0L) + return jjStartNfaWithStates_0(2, 27, 23); + return jjMoveStringLiteralDfa3_0(active0, 0x40020020L); case 111: - return jjMoveStringLiteralDfa3_0(active0, 0x10300020008L); + return jjMoveStringLiteralDfa3_0(active0, 0x40c00080010L); case 112: - if ((active0 & 0x1000000L) != 0L) - return jjStartNfaWithStates_0(2, 24, 23); + if ((active0 & 0x4000000L) != 0L) + return jjStartNfaWithStates_0(2, 26, 23); break; case 114: - return jjMoveStringLiteralDfa3_0(active0, 0x4000L); + return jjMoveStringLiteralDfa3_0(active0, 0x10000L); case 115: - return jjMoveStringLiteralDfa3_0(active0, 0x20000000000L); + return jjMoveStringLiteralDfa3_0(active0, 0x80000000000L); case 116: - if ((active0 & 0x200000L) != 0L) - return jjStartNfaWithStates_0(2, 21, 23); - return jjMoveStringLiteralDfa3_0(active0, 0x400000000L); + if ((active0 & 0x800000L) != 0L) + return jjStartNfaWithStates_0(2, 23, 23); + return jjMoveStringLiteralDfa3_0(active0, 0x1000000000L); case 117: - return jjMoveStringLiteralDfa3_0(active0, 0x40000000080L); + return jjMoveStringLiteralDfa3_0(active0, 0x100000000100L); case 119: - return jjMoveStringLiteralDfa3_0(active0, 0x800000000L); + return jjMoveStringLiteralDfa3_0(active0, 0x2000000000L); case 120: - if ((active0 & 0x800000L) != 0L) - return jjStartNfaWithStates_0(2, 23, 23); + if ((active0 & 0x2000000L) != 0L) + return jjStartNfaWithStates_0(2, 25, 23); break; default : break; @@ -414,59 +418,59 @@ static private final int jjMoveStringLiteralDfa3_0(long old0, long active0) switch(curChar) { case 97: - return jjMoveStringLiteralDfa4_0(active0, 0x800000000L); + return jjMoveStringLiteralDfa4_0(active0, 0x2000000000L); case 98: - if ((active0 & 0x200000000L) != 0L) + if ((active0 & 0x800000000L) != 0L) { - jjmatchedKind = 33; + jjmatchedKind = 35; jjmatchedPos = 3; } - return jjMoveStringLiteralDfa4_0(active0, 0x100020080L); + return jjMoveStringLiteralDfa4_0(active0, 0x400080100L); case 99: - if ((active0 & 0x20L) != 0L) - return jjStartNfaWithStates_0(3, 5, 23); - else if ((active0 & 0x100L) != 0L) - return jjStartNfaWithStates_0(3, 8, 23); - else if ((active0 & 0x8000L) != 0L) - return jjStartNfaWithStates_0(3, 15, 23); - return jjMoveStringLiteralDfa4_0(active0, 0x10000000000L); + if ((active0 & 0x40L) != 0L) + return jjStartNfaWithStates_0(3, 6, 23); + else if ((active0 & 0x200L) != 0L) + return jjStartNfaWithStates_0(3, 9, 23); + else if ((active0 & 0x20000L) != 0L) + return jjStartNfaWithStates_0(3, 17, 23); + return jjMoveStringLiteralDfa4_0(active0, 0x40000000000L); case 100: - return jjMoveStringLiteralDfa4_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa4_0(active0, 0x40000000L); case 101: - if ((active0 & 0x400000000L) != 0L) - return jjStartNfaWithStates_0(3, 34, 23); - else if ((active0 & 0x40000000000L) != 0L) - return jjStartNfaWithStates_0(3, 42, 23); - return jjMoveStringLiteralDfa4_0(active0, 0x400000L); + if ((active0 & 0x1000000000L) != 0L) + return jjStartNfaWithStates_0(3, 36, 23); + else if ((active0 & 0x100000000000L) != 0L) + return jjStartNfaWithStates_0(3, 44, 23); + return jjMoveStringLiteralDfa4_0(active0, 0x1000000L); case 105: - return jjMoveStringLiteralDfa4_0(active0, 0x200L); + return jjMoveStringLiteralDfa4_0(active0, 0x800L); case 108: - if ((active0 & 0x8L) != 0L) - return jjStartNfaWithStates_0(3, 3, 23); + if ((active0 & 0x10L) != 0L) + return jjStartNfaWithStates_0(3, 4, 23); break; case 109: - return jjMoveStringLiteralDfa4_0(active0, 0x4400L); + return jjMoveStringLiteralDfa4_0(active0, 0x11000L); case 110: - if ((active0 & 0x40000000L) != 0L) - return jjStartNfaWithStates_0(3, 30, 23); - else if ((active0 & 0x2000000000L) != 0L) - return jjStartNfaWithStates_0(3, 37, 23); + if ((active0 & 0x100000000L) != 0L) + return jjStartNfaWithStates_0(3, 32, 23); + else if ((active0 & 0x8000000000L) != 0L) + return jjStartNfaWithStates_0(3, 39, 23); break; case 114: - return jjMoveStringLiteralDfa4_0(active0, 0x800L); + return jjMoveStringLiteralDfa4_0(active0, 0x2000L); case 115: - return jjMoveStringLiteralDfa4_0(active0, 0x3010L); + return jjMoveStringLiteralDfa4_0(active0, 0xc020L); case 116: - if ((active0 & 0x80000L) != 0L) - return jjStartNfaWithStates_0(3, 19, 23); - return jjMoveStringLiteralDfa4_0(active0, 0x20000000000L); + if ((active0 & 0x200000L) != 0L) + return jjStartNfaWithStates_0(3, 21, 23); + return jjMoveStringLiteralDfa4_0(active0, 0x80000000000L); case 117: - return jjMoveStringLiteralDfa4_0(active0, 0x4000000L); + return jjMoveStringLiteralDfa4_0(active0, 0x10000000L); case 120: - if ((active0 & 0x20000000L) != 0L) - return jjStartNfaWithStates_0(3, 29, 23); - else if ((active0 & 0x1000000000L) != 0L) - return jjStartNfaWithStates_0(3, 36, 23); + if ((active0 & 0x80000000L) != 0L) + return jjStartNfaWithStates_0(3, 31, 23); + else if ((active0 & 0x4000000000L) != 0L) + return jjStartNfaWithStates_0(3, 38, 23); break; default : break; @@ -485,31 +489,31 @@ static private final int jjMoveStringLiteralDfa4_0(long old0, long active0) switch(curChar) { case 97: - return jjMoveStringLiteralDfa5_0(active0, 0x100020000L); + return jjMoveStringLiteralDfa5_0(active0, 0x400080000L); case 101: - if ((active0 & 0x2000L) != 0L) - return jjStartNfaWithStates_0(4, 13, 23); - return jjMoveStringLiteralDfa5_0(active0, 0x20010000800L); + if ((active0 & 0x8000L) != 0L) + return jjStartNfaWithStates_0(4, 15, 23); + return jjMoveStringLiteralDfa5_0(active0, 0x80040002000L); case 104: - return jjMoveStringLiteralDfa5_0(active0, 0x10000000000L); + return jjMoveStringLiteralDfa5_0(active0, 0x40000000000L); case 108: - if ((active0 & 0x400000L) != 0L) - return jjStartNfaWithStates_0(4, 22, 23); - return jjMoveStringLiteralDfa5_0(active0, 0x4000080L); + if ((active0 & 0x1000000L) != 0L) + return jjStartNfaWithStates_0(4, 24, 23); + return jjMoveStringLiteralDfa5_0(active0, 0x10000100L); case 110: - return jjMoveStringLiteralDfa5_0(active0, 0x200L); + return jjMoveStringLiteralDfa5_0(active0, 0x800L); case 111: - return jjMoveStringLiteralDfa5_0(active0, 0x400L); + return jjMoveStringLiteralDfa5_0(active0, 0x1000L); case 114: - return jjMoveStringLiteralDfa5_0(active0, 0x800000000L); + return jjMoveStringLiteralDfa5_0(active0, 0x2000000000L); case 116: - if ((active0 & 0x10L) != 0L) - return jjStartNfaWithStates_0(4, 4, 23); + if ((active0 & 0x20L) != 0L) + return jjStartNfaWithStates_0(4, 5, 23); break; case 117: - return jjMoveStringLiteralDfa5_0(active0, 0x4000L); + return jjMoveStringLiteralDfa5_0(active0, 0x10000L); case 121: - return jjMoveStringLiteralDfa5_0(active0, 0x1000L); + return jjMoveStringLiteralDfa5_0(active0, 0x4000L); default : break; } @@ -527,33 +531,33 @@ static private final int jjMoveStringLiteralDfa5_0(long old0, long active0) switch(curChar) { case 97: - return jjMoveStringLiteralDfa6_0(active0, 0x10000000000L); + return jjMoveStringLiteralDfa6_0(active0, 0x40000000000L); case 98: - return jjMoveStringLiteralDfa6_0(active0, 0x100000000L); + return jjMoveStringLiteralDfa6_0(active0, 0x400000000L); case 100: - return jjMoveStringLiteralDfa6_0(active0, 0x800000400L); + return jjMoveStringLiteralDfa6_0(active0, 0x2000001000L); case 101: - if ((active0 & 0x80L) != 0L) - return jjStartNfaWithStates_0(5, 7, 23); - else if ((active0 & 0x4000000L) != 0L) - return jjStartNfaWithStates_0(5, 26, 23); + if ((active0 & 0x100L) != 0L) + return jjStartNfaWithStates_0(5, 8, 23); + else if ((active0 & 0x10000000L) != 0L) + return jjStartNfaWithStates_0(5, 28, 23); break; case 105: - return jjMoveStringLiteralDfa6_0(active0, 0x200L); + return jjMoveStringLiteralDfa6_0(active0, 0x800L); case 108: - if ((active0 & 0x20000L) != 0L) - return jjStartNfaWithStates_0(5, 17, 23); - return jjMoveStringLiteralDfa6_0(active0, 0x4000L); + if ((active0 & 0x80000L) != 0L) + return jjStartNfaWithStates_0(5, 19, 23); + return jjMoveStringLiteralDfa6_0(active0, 0x10000L); case 109: - if ((active0 & 0x20000000000L) != 0L) - return jjStartNfaWithStates_0(5, 41, 23); + if ((active0 & 0x80000000000L) != 0L) + return jjStartNfaWithStates_0(5, 43, 23); break; case 115: - return jjMoveStringLiteralDfa6_0(active0, 0x1000L); + return jjMoveStringLiteralDfa6_0(active0, 0x4000L); case 116: - return jjMoveStringLiteralDfa6_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa6_0(active0, 0x40000000L); case 119: - return jjMoveStringLiteralDfa6_0(active0, 0x800L); + return jjMoveStringLiteralDfa6_0(active0, 0x2000L); default : break; } @@ -571,23 +575,23 @@ static private final int jjMoveStringLiteralDfa6_0(long old0, long active0) switch(curChar) { case 97: - if ((active0 & 0x4000L) != 0L) - return jjStartNfaWithStates_0(6, 14, 23); - return jjMoveStringLiteralDfa7_0(active0, 0x800L); + if ((active0 & 0x10000L) != 0L) + return jjStartNfaWithStates_0(6, 16, 23); + return jjMoveStringLiteralDfa7_0(active0, 0x2000L); case 101: - return jjMoveStringLiteralDfa7_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa7_0(active0, 0x40000000L); case 105: - return jjMoveStringLiteralDfa7_0(active0, 0x100000000L); + return jjMoveStringLiteralDfa7_0(active0, 0x400000000L); case 115: - if ((active0 & 0x800000000L) != 0L) - return jjStartNfaWithStates_0(6, 35, 23); - return jjMoveStringLiteralDfa7_0(active0, 0x10000000000L); + if ((active0 & 0x2000000000L) != 0L) + return jjStartNfaWithStates_0(6, 37, 23); + return jjMoveStringLiteralDfa7_0(active0, 0x40000000000L); case 116: - if ((active0 & 0x200L) != 0L) - return jjStartNfaWithStates_0(6, 9, 23); - return jjMoveStringLiteralDfa7_0(active0, 0x1000L); + if ((active0 & 0x800L) != 0L) + return jjStartNfaWithStates_0(6, 11, 23); + return jjMoveStringLiteralDfa7_0(active0, 0x4000L); case 117: - return jjMoveStringLiteralDfa7_0(active0, 0x400L); + return jjMoveStringLiteralDfa7_0(active0, 0x1000L); default : break; } @@ -605,13 +609,13 @@ static private final int jjMoveStringLiteralDfa7_0(long old0, long active0) switch(curChar) { case 101: - return jjMoveStringLiteralDfa8_0(active0, 0x1000L); + return jjMoveStringLiteralDfa8_0(active0, 0x4000L); case 108: - return jjMoveStringLiteralDfa8_0(active0, 0x100000400L); + return jjMoveStringLiteralDfa8_0(active0, 0x400001000L); case 114: - return jjMoveStringLiteralDfa8_0(active0, 0x10000800L); + return jjMoveStringLiteralDfa8_0(active0, 0x40002000L); case 116: - return jjMoveStringLiteralDfa8_0(active0, 0x10000000000L); + return jjMoveStringLiteralDfa8_0(active0, 0x40000000000L); default : break; } @@ -629,17 +633,17 @@ static private final int jjMoveStringLiteralDfa8_0(long old0, long active0) switch(curChar) { case 100: - return jjMoveStringLiteralDfa9_0(active0, 0x800L); + return jjMoveStringLiteralDfa9_0(active0, 0x2000L); case 101: - if ((active0 & 0x400L) != 0L) - return jjStartNfaWithStates_0(8, 10, 23); + if ((active0 & 0x1000L) != 0L) + return jjStartNfaWithStates_0(8, 12, 23); break; case 105: - return jjMoveStringLiteralDfa9_0(active0, 0x10100000000L); + return jjMoveStringLiteralDfa9_0(active0, 0x40400000000L); case 109: - if ((active0 & 0x1000L) != 0L) - return jjStartNfaWithStates_0(8, 12, 23); - return jjMoveStringLiteralDfa9_0(active0, 0x10000000L); + if ((active0 & 0x4000L) != 0L) + return jjStartNfaWithStates_0(8, 14, 23); + return jjMoveStringLiteralDfa9_0(active0, 0x40000000L); default : break; } @@ -657,15 +661,15 @@ static private final int jjMoveStringLiteralDfa9_0(long old0, long active0) switch(curChar) { case 99: - if ((active0 & 0x10000000000L) != 0L) - return jjStartNfaWithStates_0(9, 40, 23); + if ((active0 & 0x40000000000L) != 0L) + return jjStartNfaWithStates_0(9, 42, 23); break; case 105: - return jjMoveStringLiteralDfa10_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa10_0(active0, 0x40000000L); case 115: - if ((active0 & 0x800L) != 0L) - return jjStartNfaWithStates_0(9, 11, 23); - return jjMoveStringLiteralDfa10_0(active0, 0x100000000L); + if ((active0 & 0x2000L) != 0L) + return jjStartNfaWithStates_0(9, 13, 23); + return jjMoveStringLiteralDfa10_0(active0, 0x400000000L); default : break; } @@ -683,9 +687,9 @@ static private final int jjMoveStringLiteralDfa10_0(long old0, long active0) switch(curChar) { case 110: - return jjMoveStringLiteralDfa11_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa11_0(active0, 0x40000000L); case 116: - return jjMoveStringLiteralDfa11_0(active0, 0x100000000L); + return jjMoveStringLiteralDfa11_0(active0, 0x400000000L); default : break; } @@ -703,7 +707,7 @@ static private final int jjMoveStringLiteralDfa11_0(long old0, long active0) switch(curChar) { case 105: - return jjMoveStringLiteralDfa12_0(active0, 0x110000000L); + return jjMoveStringLiteralDfa12_0(active0, 0x440000000L); default : break; } @@ -721,11 +725,11 @@ static private final int jjMoveStringLiteralDfa12_0(long old0, long active0) switch(curChar) { case 99: - if ((active0 & 0x100000000L) != 0L) - return jjStartNfaWithStates_0(12, 32, 23); + if ((active0 & 0x400000000L) != 0L) + return jjStartNfaWithStates_0(12, 34, 23); break; case 115: - return jjMoveStringLiteralDfa13_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa13_0(active0, 0x40000000L); default : break; } @@ -743,7 +747,7 @@ static private final int jjMoveStringLiteralDfa13_0(long old0, long active0) switch(curChar) { case 116: - return jjMoveStringLiteralDfa14_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa14_0(active0, 0x40000000L); default : break; } @@ -761,7 +765,7 @@ static private final int jjMoveStringLiteralDfa14_0(long old0, long active0) switch(curChar) { case 105: - return jjMoveStringLiteralDfa15_0(active0, 0x10000000L); + return jjMoveStringLiteralDfa15_0(active0, 0x40000000L); default : break; } @@ -779,8 +783,8 @@ static private final int jjMoveStringLiteralDfa15_0(long old0, long active0) switch(curChar) { case 99: - if ((active0 & 0x10000000L) != 0L) - return jjStartNfaWithStates_0(15, 28, 23); + if ((active0 & 0x40000000L) != 0L) + return jjStartNfaWithStates_0(15, 30, 23); break; default : break; @@ -842,14 +846,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 23: if ((0x3ff000000000000L & l) != 0L) { - if (kind > 77) - kind = 77; + if (kind > 79) + kind = 79; jjCheckNAdd(22); } else if (curChar == 39) { - if (kind > 76) - kind = 76; + if (kind > 78) + kind = 78; } if ((0x3ff000000000000L & l) != 0L) jjCheckNAddTwoStates(20, 21); @@ -857,8 +861,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 0: if ((0x3ff000000000000L & l) != 0L) { - if (kind > 75) - kind = 75; + if (kind > 77) + kind = 77; jjCheckNAddStates(0, 3); } else if ((0x100002600L & l) != 0L) @@ -874,14 +878,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjstateSet[jjnewStateCnt++] = 1; if ((0x3fe000000000000L & l) != 0L) { - if (kind > 74) - kind = 74; + if (kind > 76) + kind = 76; jjCheckNAdd(8); } else if (curChar == 48) { - if (kind > 74) - kind = 74; + if (kind > 76) + kind = 76; } break; case 1: @@ -911,20 +915,20 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 7: if ((0x3fe000000000000L & l) == 0L) break; - if (kind > 74) - kind = 74; + if (kind > 76) + kind = 76; jjCheckNAdd(8); break; case 8: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 74) - kind = 74; + if (kind > 76) + kind = 76; jjCheckNAdd(8); break; case 9: - if (curChar == 48 && kind > 74) - kind = 74; + if (curChar == 48 && kind > 76) + kind = 76; break; case 10: if (curChar == 46) @@ -933,8 +937,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 11: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 75) - kind = 75; + if (kind > 77) + kind = 77; jjCheckNAddTwoStates(11, 12); break; case 13: @@ -944,8 +948,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 14: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 75) - kind = 75; + if (kind > 77) + kind = 77; jjCheckNAdd(14); break; case 15: @@ -957,14 +961,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjCheckNAddTwoStates(16, 17); break; case 17: - if (curChar == 35 && kind > 78) - kind = 78; + if (curChar == 35 && kind > 80) + kind = 80; break; case 18: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 75) - kind = 75; + if (kind > 77) + kind = 77; jjCheckNAddStates(0, 3); break; case 20: @@ -972,14 +976,14 @@ static private final int jjMoveNfa_0(int startState, int curPos) jjCheckNAddTwoStates(20, 21); break; case 21: - if (curChar == 39 && kind > 76) - kind = 76; + if (curChar == 39 && kind > 78) + kind = 78; break; case 22: if ((0x3ff000000000000L & l) == 0L) break; - if (kind > 77) - kind = 77; + if (kind > 79) + kind = 79; jjCheckNAdd(22); break; default : break; @@ -996,8 +1000,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 23: if ((0x7fffffe87fffffeL & l) != 0L) { - if (kind > 77) - kind = 77; + if (kind > 79) + kind = 79; jjCheckNAdd(22); } if ((0x7fffffe87fffffeL & l) != 0L) @@ -1006,8 +1010,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 0: if ((0x7fffffe87fffffeL & l) == 0L) break; - if (kind > 77) - kind = 77; + if (kind > 79) + kind = 79; jjCheckNAddStates(7, 9); break; case 2: @@ -1027,8 +1031,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) case 22: if ((0x7fffffe87fffffeL & l) == 0L) break; - if (kind > 77) - kind = 77; + if (kind > 79) + kind = 79; jjCheckNAdd(22); break; default : break; @@ -1072,8 +1076,8 @@ static final int[] jjnextStates = { 10, 11, 12, 18, 2, 3, 5, 20, 21, 22, 13, 14, 16, 17, }; public static final String[] jjstrLiteralImages = { -"", null, null, "\142\157\157\154", "\143\157\156\163\164", -"\143\164\155\143", "\103", "\144\157\165\142\154\145", "\144\164\155\143", +"", null, null, "\101", "\142\157\157\154", "\143\157\156\163\164", +"\143\164\155\143", "\103", "\144\157\165\142\154\145", "\144\164\155\143", "\105", "\145\156\144\151\156\151\164", "\145\156\144\155\157\144\165\154\145", "\145\156\144\162\145\167\141\162\144\163", "\145\156\144\163\171\163\164\145\155", "\146\141\154\163\145", "\146\157\162\155\165\154\141", "\146\165\156\143", "\106", "\147\154\157\142\141\154", "\107", @@ -1091,7 +1095,7 @@ public static final String[] lexStateNames = { "DEFAULT", }; static final long[] jjtoToken = { - 0xfffffffffffffff9L, 0xffffL, + 0xfffffffffffffff9L, 0x3ffffL, }; static final long[] jjtoSkip = { 0x6L, 0x0L, @@ -1184,9 +1188,9 @@ public static Token getNextToken() jjmatchedKind = 0x7fffffff; jjmatchedPos = 0; curPos = jjMoveStringLiteralDfa0_0(); - if (jjmatchedPos == 0 && jjmatchedKind > 79) + if (jjmatchedPos == 0 && jjmatchedKind > 81) { - jjmatchedKind = 79; + jjmatchedKind = 81; } if (jjmatchedKind != 0x7fffffff) { diff --git a/prism/src/parser/ast/ExpressionExists.java b/prism/src/parser/ast/ExpressionExists.java new file mode 100644 index 00000000..b4dca69a --- /dev/null +++ b/prism/src/parser/ast/ExpressionExists.java @@ -0,0 +1,115 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser.ast; + +import parser.*; +import parser.visitor.*; +import prism.PrismLangException; + +public class ExpressionExists extends Expression +{ + Expression expression = null; + + // Constructors + + public ExpressionExists() + { + } + + public ExpressionExists(Expression e) + { + expression = e; + } + + // Set methods + + public void setExpression(Expression e) + { + expression = e; + } + + // Get methods + + public Expression getExpression() + { + return expression; + } + + // Methods required for Expression: + + /** + * Is this expression constant? + */ + public boolean isConstant() + { + return false; + } + + /** + * Evaluate this expression, return result. + * Note: assumes that type checking has been done already. + */ + public Object evaluate(Values constantValues, Values varValues) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an E operator without a model"); + } + + // Methods required for ASTElement: + + /** + * Visitor method. + */ + public Object accept(ASTVisitor v) throws PrismLangException + { + return v.visit(this); + } + + /** + * Convert to string. + */ + public String toString() + { + String s = ""; + + s += "E [ " + expression + " ]"; + + return s; + } + + /** + * Perform a deep copy. + */ + public Expression deepCopy() + { + ExpressionExists expr = new ExpressionExists(expression.deepCopy()); + expr.setType(type); + expr.setPosition(this); + return expr; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/ast/ExpressionForAll.java b/prism/src/parser/ast/ExpressionForAll.java new file mode 100644 index 00000000..521914c2 --- /dev/null +++ b/prism/src/parser/ast/ExpressionForAll.java @@ -0,0 +1,115 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford, formerly University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser.ast; + +import parser.*; +import parser.visitor.*; +import prism.PrismLangException; + +public class ExpressionForAll extends Expression +{ + Expression expression = null; + + // Constructors + + public ExpressionForAll() + { + } + + public ExpressionForAll(Expression e) + { + expression = e; + } + + // Set methods + + public void setExpression(Expression e) + { + expression = e; + } + + // Get methods + + public Expression getExpression() + { + return expression; + } + + // Methods required for Expression: + + /** + * Is this expression constant? + */ + public boolean isConstant() + { + return false; + } + + /** + * Evaluate this expression, return result. + * Note: assumes that type checking has been done already. + */ + public Object evaluate(Values constantValues, Values varValues) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate an E operator without a model"); + } + + // Methods required for ASTElement: + + /** + * Visitor method. + */ + public Object accept(ASTVisitor v) throws PrismLangException + { + return v.visit(this); + } + + /** + * Convert to string. + */ + public String toString() + { + String s = ""; + + s += "A [ " + expression + " ]"; + + return s; + } + + /** + * Perform a deep copy. + */ + public Expression deepCopy() + { + ExpressionForAll expr = new ExpressionForAll(expression.deepCopy()); + expr.setType(type); + expr.setPosition(this); + return expr; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 9b86f8df..4e96ea6d 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -446,6 +446,26 @@ public class ASTTraverse implements ASTVisitor } public void visitPost(ExpressionSS e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionExists e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionExists e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) e.getExpression().accept(this); + visitPost(e); + return null; + } + public void visitPost(ExpressionExists e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionForAll e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionForAll e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) e.getExpression().accept(this); + visitPost(e); + return null; + } + public void visitPost(ExpressionForAll e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLabel e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionLabel e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 90ea5e70..2ff7c1df 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -448,6 +448,26 @@ public class ASTTraverseModify implements ASTVisitor } public void visitPost(ExpressionSS e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionExists e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionExists e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this))); + visitPost(e); + return e; + } + public void visitPost(ExpressionExists e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionForAll e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionForAll e) throws PrismLangException + { + visitPre(e); + if (e.getExpression() != null) e.setExpression((Expression)(e.getExpression().accept(this))); + visitPost(e); + return e; + } + public void visitPost(ExpressionForAll e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(ExpressionLabel e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionLabel e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index 99cf13df..9de55257 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -67,6 +67,8 @@ public interface ASTVisitor public Object visit(ExpressionProb e) throws PrismLangException; public Object visit(ExpressionReward e) throws PrismLangException; public Object visit(ExpressionSS e) throws PrismLangException; + public Object visit(ExpressionExists e) throws PrismLangException; + public Object visit(ExpressionForAll e) throws PrismLangException; public Object visit(ExpressionLabel e) throws PrismLangException; // ASTElement classes (misc.) public Object visit(Filter e) throws PrismLangException; diff --git a/prism/src/parser/visitor/Rename.java b/prism/src/parser/visitor/Rename.java index 50927de3..baac0d1b 100644 --- a/prism/src/parser/visitor/Rename.java +++ b/prism/src/parser/visitor/Rename.java @@ -133,5 +133,19 @@ public class Rename extends ASTTraverseModify // at the level of an individual module (and below) throw new PrismLangException("S operator should never be renamed"); } + + public void visitPost(ExpressionExists e) throws PrismLangException + { + // This renaming is only designed to be applied + // at the level of an individual module (and below) + throw new PrismLangException("E operator should never be renamed"); + } + + public void visitPost(ExpressionForAll e) throws PrismLangException + { + // This renaming is only designed to be applied + // at the level of an individual module (and below) + throw new PrismLangException("A operator should never be renamed"); + } } diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index c850638b..0193d92d 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -443,6 +443,16 @@ public class TypeCheck extends ASTTraverse e.setType(e.getProb() == null ? Expression.DOUBLE : Expression.BOOLEAN); } + public void visitPost(ExpressionExists e) throws PrismLangException + { + e.setType(Expression.BOOLEAN); + } + + public void visitPost(ExpressionForAll e) throws PrismLangException + { + e.setType(Expression.BOOLEAN); + } + public void visitPost(ExpressionLabel e) throws PrismLangException { e.setType(Expression.BOOLEAN);