From 726ff06c1b6208f2450ce581be7105d1e1003c58 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Mar 2010 22:18:52 +0000 Subject: [PATCH] Updates to filters. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1801 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismParser.java | 744 +++++++++--------- prism/src/parser/PrismParser.jj | 26 +- prism/src/parser/PrismParserConstants.java | 94 +++ prism/src/parser/PrismParserTokenManager.java | 176 +++-- prism/src/parser/ast/ExpressionFilter.java | 6 +- prism/src/parser/ast/Filter.java | 20 +- prism/src/parser/visitor/TypeCheck.java | 23 + prism/src/prism/StateModelChecker.java | 2 + 8 files changed, 635 insertions(+), 456 deletions(-) diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 9f08ed27..c98f0553 100644 --- a/prism/src/parser/PrismParser.java +++ b/prism/src/parser/PrismParser.java @@ -38,26 +38,26 @@ public class PrismParser implements PrismParserConstants { p = new PrismParser(); str = (args.length > 1) ? new FileInputStream(args[1]) : System.in; src = (args.length > 1) ? "file "+args[1] : "stdin"; - System.out.println("Reading from "+src+"...\n"); + System.out.println("Reading from "+src+"...\u005cn"); if (args[0].equals("-modulesfile") || args[0].equals("-mf")) { ModulesFile mf = p.parseModulesFile(str); - System.out.print("Modules file:\n=============\n\n" + mf); - System.out.print("\nTree:\n=====\n" + mf.toTreeString()); + System.out.print("Modules file:\u005cn=============\u005cn\u005cn" + mf); + System.out.print("\u005cnTree:\u005cn=====\u005cn" + mf.toTreeString()); mf.tidyUp(); - System.out.print("\nAnd after expansion:\n====================\n\n" +mf); + System.out.print("\u005cnAnd after expansion:\u005cn====================\u005cn\u005cn" +mf); } else if (args[0].equals("-propertiesfile") || args[0].equals("-pf")) { PropertiesFile pf = p.parsePropertiesFile(new ModulesFile(), str); - System.out.print("Properties file:\n================\n\n" + pf); - System.out.print("\nTree:\n=====\n" + pf.toTreeString()); + System.out.print("Properties file:\u005cn================\u005cn\u005cn" + pf); + System.out.print("\u005cnTree:\u005cn=====\u005cn" + pf.toTreeString()); pf.tidyUp(); - System.out.print("\nAnd after expansion:\n====================\n\n" + pf); + System.out.print("\u005cnAnd after expansion:\u005cn====================\u005cn\u005cn" + pf); } else if (args[0].equals("-expression") || args[0].equals("-e")) { Expression expr = p.parseSingleExpression(str); System.out.println("Expression: " + expr.toString()); - System.out.print("Tree:\n=====\n" + expr.toTreeString()); + System.out.print("Tree:\u005cn=====\u005cn" + expr.toTreeString()); expr.typeCheck(); expr.semanticCheck(); System.out.println("Type: " + expr.getType().getTypeString()); @@ -87,7 +87,7 @@ public class PrismParser implements PrismParserConstants { // Build a list of strings for keywords keywordList.clear(); for (int i = PrismParserConstants.COMMENT+1; i < PrismParserConstants.NOT; i++) { - keywordList.add(PrismParserConstants.tokenImage[i].replaceAll("\"", "")); + keywordList.add(PrismParserConstants.tokenImage[i].replaceAll("\u005c"", "")); } } @@ -198,20 +198,20 @@ public class PrismParser implements PrismParserConstants { while (t != null) { s = t.image; // strip any nasty carriage returns - s = s.replaceAll("\r", ""); + s = s.replaceAll("\u005cr", ""); // remove "//" and preceding/subsequent spaces/tabs from comments if (t.kind == PrismParserConstants.COMMENT) { - while (comment.length() > 0 && (""+comment.charAt(comment.length()-1)).matches("[ \t]")) + while (comment.length() > 0 && (""+comment.charAt(comment.length()-1)).matches("[ \u005ct]")) comment = comment.substring(0,comment.length()-1); s = s.substring(2); - s = s.replaceFirst("[ \t]*", ""); + s = s.replaceFirst("[ \u005ct]*", ""); } comment += s; t = t.next; } } // remove final new line (if present) - if (comment.length() > 0 && (comment.charAt(comment.length()-1) == '\n')) + if (comment.length() > 0 && (comment.charAt(comment.length()-1) == '\u005cn')) comment = comment.substring(0,comment.length()-1); return comment; @@ -224,15 +224,15 @@ public class PrismParser implements PrismParserConstants { int i; String s, res = ""; // break into lines - while ((i = comment.indexOf("\n")) != -1) { + while ((i = comment.indexOf("\u005cn")) != -1) { s = comment.substring(0, i); comment = comment.substring(i+1); // add "//" to non-empty lines if (s.trim().length()>0) res += "// " + s; - res += "\n"; + res += "\u005cn"; } // deal with any trailing characters (with no new line ending them) - if (comment.trim().length()>0) res += "// " + comment + "\n"; + if (comment.trim().length()>0) res += "// " + comment + "\u005cn"; return res; } @@ -2347,7 +2347,7 @@ public class PrismParser implements PrismParserConstants { // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - String filterOp = isBool ? "&" : filter.minRequested() ? "min" : "max"; + String filterOp = isBool ? "&" : filter.getFilterOpString(); ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); {if (true) return ef;} @@ -2405,6 +2405,7 @@ public class PrismParser implements PrismParserConstants { Filter filter = null; ExpressionSS ret = new ExpressionSS(); Token begin; + boolean isBool; if (!prop) {if (true) throw generateParseException();} // Various options for "S" keyword and attached symbols begin = jj_consume_token(S); @@ -2415,12 +2416,12 @@ public class PrismParser implements PrismParserConstants { case GE: r = LtGt(); prob = Expression(false, false); - relOp = ExpressionBinaryOp.opSymbols[r]; + relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; break; case EQ: jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "="; + relOp = "="; isBool = false; break; default: jj_la1[68] = jj_gen; @@ -2446,7 +2447,8 @@ public class PrismParser implements PrismParserConstants { // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression()); + String filterOp = isBool ? "&" : filter.getFilterOpString(); + ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); {if (true) return ef;} } @@ -2464,6 +2466,7 @@ public class PrismParser implements PrismParserConstants { Filter filter = null; ExpressionReward ret = new ExpressionReward(); Token begin; + boolean isBool; if (!prop) {if (true) throw generateParseException();} switch ((jj_ntk==-1)?jj_ntk():jj_ntk) { case R: @@ -2483,24 +2486,24 @@ public class PrismParser implements PrismParserConstants { case GE: r = LtGt(); rew = Expression(false, false); - relOp = ExpressionBinaryOp.opSymbols[r]; + relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; break; case EQ: jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "="; + relOp = "="; isBool = false; break; case MIN: jj_consume_token(MIN); jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "min="; + relOp = "min="; isBool = false; break; case MAX: jj_consume_token(MAX); jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "max="; + relOp = "max="; isBool = false; break; default: jj_la1[71] = jj_gen; @@ -2512,13 +2515,13 @@ public class PrismParser implements PrismParserConstants { begin = jj_consume_token(RMIN); jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "min="; + relOp = "min="; isBool = false; break; case RMAX: begin = jj_consume_token(RMAX); jj_consume_token(EQ); jj_consume_token(QMARK); - relOp = "max="; + relOp = "max="; isBool = false; break; default: jj_la1[72] = jj_gen; @@ -2545,7 +2548,8 @@ public class PrismParser implements PrismParserConstants { // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression()); + String filterOp = isBool ? "&" : filter.getFilterOpString(); + ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); {if (true) return ef;} } @@ -2885,152 +2889,146 @@ public class PrismParser implements PrismParserConstants { throw new Error("Missing return statement in function"); } - static final private boolean jj_2_1(int xla) { + static private boolean jj_2_1(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_1(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(0, xla); } } - static final private boolean jj_2_2(int xla) { + static private boolean jj_2_2(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_2(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(1, xla); } } - static final private boolean jj_2_3(int xla) { + static private boolean jj_2_3(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_3(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(2, xla); } } - static final private boolean jj_2_4(int xla) { + static private boolean jj_2_4(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_4(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(3, xla); } } - static final private boolean jj_2_5(int xla) { + static private boolean jj_2_5(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_5(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(4, xla); } } - static final private boolean jj_2_6(int xla) { + static private boolean jj_2_6(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_6(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(5, xla); } } - static final private boolean jj_2_7(int xla) { + static private boolean jj_2_7(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_7(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(6, xla); } } - static final private boolean jj_2_8(int xla) { + static private boolean jj_2_8(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_8(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(7, xla); } } - static final private boolean jj_2_9(int xla) { + static private boolean jj_2_9(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_9(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(8, xla); } } - static final private boolean jj_2_10(int xla) { + static private boolean jj_2_10(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_10(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(9, xla); } } - static final private boolean jj_2_11(int xla) { + static private boolean jj_2_11(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_11(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(10, xla); } } - static final private boolean jj_2_12(int xla) { + static private boolean jj_2_12(int xla) { jj_la = xla; jj_lastpos = jj_scanpos = token; try { return !jj_3_12(); } catch(LookaheadSuccess ls) { return true; } finally { jj_save(11, xla); } } - static final private boolean jj_3R_64() { - if (jj_3R_66()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_67()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3R_135() { + static private boolean jj_3R_135() { if (jj_3R_155()) return true; return false; } - static final private boolean jj_3R_160() { + static private boolean jj_3R_160() { 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_138() { + static private boolean jj_3R_64() { + if (jj_3R_66()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_67()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_138() { 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_159() { + static private boolean jj_3R_159() { 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_137() { + static private boolean jj_3R_137() { 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_158() { + static private boolean jj_3R_158() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_157() { + static private boolean jj_3R_157() { if (jj_3R_78()) return true; if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_65() { - if (jj_scan_token(OR)) return true; - if (jj_3R_64()) return true; - return false; - } - - static final private boolean jj_3R_136() { + static private boolean jj_3R_136() { if (jj_scan_token(R)) return true; Token xsp; xsp = jj_scanpos; @@ -3049,23 +3047,13 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_56() { + static private boolean jj_3R_65() { + if (jj_scan_token(OR)) return true; if (jj_3R_64()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_65()) { jj_scanpos = xsp; break; } - } 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_113() { + static private boolean jj_3R_113() { Token xsp; xsp = jj_scanpos; if (jj_3R_136()) { @@ -3083,18 +3071,34 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_60() { + static private boolean jj_3R_56() { + if (jj_3R_64()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_65()) { jj_scanpos = xsp; break; } + } + return false; + } + + static 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_57() { + static private boolean jj_3R_60() { + if (jj_3R_29()) return true; + return false; + } + + static private boolean jj_3R_57() { if (jj_scan_token(IMPLIES)) return true; if (jj_3R_56()) return true; return false; } - static final private boolean jj_3R_50() { + static private boolean jj_3R_50() { if (jj_3R_56()) return true; Token xsp; while (true) { @@ -3104,7 +3108,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_51() { + static 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; @@ -3112,25 +3116,31 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_11() { + static private boolean jj_3_11() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } - static final private boolean jj_3_9() { + static private boolean jj_3_9() { if (jj_3R_29()) return true; if (jj_scan_token(LPARENTH)) return true; return false; } - static final private boolean jj_3R_134() { + static private boolean jj_3R_134() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_48() { + static private boolean jj_3R_133() { + if (jj_3R_78()) return true; + if (jj_3R_34()) return true; + return false; + } + + static private boolean jj_3R_48() { if (jj_3R_50()) return true; Token xsp; xsp = jj_scanpos; @@ -3138,23 +3148,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_133() { - if (jj_3R_78()) return true; - if (jj_3R_34()) return true; - return false; - } - - static final private boolean jj_3R_62() { + static private boolean jj_3R_62() { if (jj_3R_29()) return true; return false; } - static final private boolean jj_3R_58() { + static private boolean jj_3R_58() { if (jj_3R_29()) return true; return false; } - static final private boolean jj_3R_55() { + static private boolean jj_3R_55() { if (jj_scan_token(LBRACKET)) return true; if (jj_3R_34()) return true; if (jj_scan_token(COMMA)) return true; @@ -3163,18 +3167,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_54() { - if (jj_scan_token(GE)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_62()) { - jj_scanpos = xsp; - if (jj_3R_63()) return true; - } - return false; - } - - static final private boolean jj_3R_112() { + static private boolean jj_3R_112() { if (jj_scan_token(S)) return true; Token xsp; xsp = jj_scanpos; @@ -3190,7 +3183,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_53() { + static private boolean jj_3R_54() { + if (jj_scan_token(GE)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_62()) { + jj_scanpos = xsp; + if (jj_3R_63()) return true; + } + return false; + } + + static private boolean jj_3R_53() { if (jj_scan_token(LT)) return true; Token xsp; xsp = jj_scanpos; @@ -3201,7 +3205,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_52() { + static private boolean jj_3R_52() { if (jj_scan_token(LE)) return true; Token xsp; xsp = jj_scanpos; @@ -3212,7 +3216,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_49() { + static private boolean jj_3R_49() { Token xsp; xsp = jj_scanpos; if (jj_3R_52()) { @@ -3228,47 +3232,47 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_132() { + static private boolean jj_3R_132() { if (jj_3R_155()) return true; return false; } - static final private boolean jj_3R_168() { + static private boolean jj_3R_168() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_39() { + static private boolean jj_3R_39() { if (jj_3R_48()) return true; return false; } - static final private boolean jj_3R_167() { + static private boolean jj_3R_167() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3R_47() { + static private boolean jj_3R_47() { if (jj_3R_49()) return true; return false; } - static final private boolean jj_3R_46() { + static private boolean jj_3R_46() { if (jj_scan_token(G)) return true; return false; } - static final private boolean jj_3R_45() { + static private boolean jj_3R_45() { if (jj_scan_token(F)) return true; return false; } - static final private boolean jj_3R_44() { + static private boolean jj_3R_44() { if (jj_scan_token(X)) return true; return false; } - static final private boolean jj_3R_38() { + static private boolean jj_3R_38() { Token xsp; xsp = jj_scanpos; if (jj_3R_44()) { @@ -3284,7 +3288,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_165() { + static private boolean jj_3R_165() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; @@ -3296,7 +3300,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_155() { + static private boolean jj_3R_155() { if (jj_scan_token(LBRACE)) return true; if (jj_3R_34()) return true; if (jj_scan_token(RBRACE)) return true; @@ -3308,7 +3312,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_36() { + static private boolean jj_3R_36() { Token xsp; xsp = jj_scanpos; if (jj_3R_38()) { @@ -3318,27 +3322,27 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_43() { + static private boolean jj_3R_43() { if (jj_3R_49()) return true; return false; } - static final private boolean jj_3R_42() { + static private boolean jj_3R_42() { if (jj_scan_token(R)) return true; return false; } - static final private boolean jj_3R_41() { + static private boolean jj_3R_41() { if (jj_scan_token(W)) return true; return false; } - static final private boolean jj_3R_40() { + static private boolean jj_3R_40() { if (jj_scan_token(U)) return true; return false; } - static final private boolean jj_3R_37() { + static private boolean jj_3R_37() { Token xsp; xsp = jj_scanpos; if (jj_3R_40()) { @@ -3354,33 +3358,33 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_151() { + static private boolean jj_3R_151() { if (jj_3R_78()) return true; if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_154() { + static private boolean jj_3R_154() { 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_153() { + static private boolean jj_3R_153() { 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_152() { + static private boolean jj_3R_152() { if (jj_scan_token(EQ)) return true; if (jj_scan_token(QMARK)) return true; return false; } - static final private boolean jj_3R_35() { + static private boolean jj_3R_35() { if (jj_3R_36()) return true; Token xsp; xsp = jj_scanpos; @@ -3388,21 +3392,21 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_131() { + static private boolean jj_3R_131() { 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_130() { + static private boolean jj_3R_130() { 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_129() { + static private boolean jj_3R_129() { if (jj_scan_token(P)) return true; Token xsp; xsp = jj_scanpos; @@ -3419,7 +3423,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_111() { + static private boolean jj_3R_111() { Token xsp; xsp = jj_scanpos; if (jj_3R_129()) { @@ -3437,78 +3441,78 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_150() { + static private boolean jj_3R_150() { if (jj_scan_token(COMMA)) return true; if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_128() { + static private boolean jj_3R_128() { if (jj_3R_27()) return true; return false; } - static final private boolean jj_3_3() { + static private boolean jj_3_3() { if (jj_scan_token(LABEL)) return true; return false; } - static final private boolean jj_3_2() { + static 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_34() { + static private boolean jj_3R_34() { if (jj_3R_35()) return true; return false; } - static final private boolean jj_3R_110() { + static private boolean jj_3R_110() { 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_127() { + static private boolean jj_3R_127() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_121() { + static private boolean jj_3R_121() { if (jj_scan_token(FALSE)) return true; return false; } - static final private boolean jj_3R_120() { + static private boolean jj_3R_120() { if (jj_scan_token(TRUE)) return true; return false; } - static final private boolean jj_3R_119() { + static private boolean jj_3R_119() { if (jj_scan_token(REG_DOUBLE)) return true; return false; } - static final private boolean jj_3_7() { + static 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_126() { + static private boolean jj_3R_126() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3R_118() { + static private boolean jj_3R_118() { if (jj_scan_token(REG_INT)) return true; return false; } - static final private boolean jj_3R_106() { + static private boolean jj_3R_106() { Token xsp; xsp = jj_scanpos; if (jj_3R_118()) { @@ -3524,42 +3528,32 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_124() { + static private boolean jj_3R_124() { if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_88() { + static private boolean jj_3R_88() { if (jj_scan_token(LE)) return true; return false; } - static final private boolean jj_3R_125() { - if (jj_3R_34()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_150()) { jj_scanpos = xsp; break; } - } - return false; - } - - static final private boolean jj_3R_87() { + static private boolean jj_3R_87() { if (jj_scan_token(GE)) return true; return false; } - static final private boolean jj_3R_86() { + static private boolean jj_3R_86() { if (jj_scan_token(LT)) return true; return false; } - static final private boolean jj_3R_85() { + static private boolean jj_3R_85() { if (jj_scan_token(GT)) return true; return false; } - static final private boolean jj_3R_78() { + static private boolean jj_3R_78() { Token xsp; xsp = jj_scanpos; if (jj_3R_85()) { @@ -3575,23 +3569,33 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_6() { + static private boolean jj_3R_125() { + if (jj_3R_34()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_150()) { jj_scanpos = xsp; break; } + } + return false; + } + + static 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_80() { + static private boolean jj_3R_80() { if (jj_scan_token(NE)) return true; return false; } - static final private boolean jj_3R_79() { + static private boolean jj_3R_79() { if (jj_scan_token(EQ)) return true; return false; } - static final private boolean jj_3R_75() { + static private boolean jj_3R_75() { Token xsp; xsp = jj_scanpos; if (jj_3R_79()) { @@ -3601,7 +3605,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_109() { + static private boolean jj_3R_109() { if (jj_scan_token(FUNC)) return true; if (jj_scan_token(LPARENTH)) return true; Token xsp; @@ -3619,18 +3623,18 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_8() { + static 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_123() { + static private boolean jj_3R_123() { if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3R_108() { + static private boolean jj_3R_108() { Token xsp; xsp = jj_scanpos; if (jj_3R_123()) { @@ -3643,24 +3647,24 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_33() { + static private boolean jj_3R_33() { if (jj_scan_token(REG_IDENTPRIME)) return true; return false; } - static final private boolean jj_3R_122() { - if (jj_scan_token(LPARENTH)) return true; - if (jj_3R_125()) return true; - if (jj_scan_token(RPARENTH)) return true; + static private boolean jj_3R_147() { + if (jj_scan_token(OR)) return true; return false; } - static final private boolean jj_3R_147() { - if (jj_scan_token(OR)) return true; + static private boolean jj_3R_122() { + if (jj_scan_token(LPARENTH)) return true; + if (jj_3R_125()) return true; + if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3R_107() { + static private boolean jj_3R_107() { if (jj_3R_27()) return true; Token xsp; xsp = jj_scanpos; @@ -3668,128 +3672,157 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_29() { + static private boolean jj_3R_29() { if (jj_3R_27()) return true; return false; } - static final private boolean jj_3R_105() { + static private boolean jj_3R_105() { if (jj_3R_117()) return true; return false; } - static final private boolean jj_3R_104() { - if (jj_3R_116()) return true; + static private boolean jj_3R_144() { + if (jj_scan_token(MAX)) return true; return false; } - static final private boolean jj_3R_103() { - if (jj_3R_115()) return true; + static private boolean jj_3R_146() { + if (jj_scan_token(AND)) return true; return false; } - static final private boolean jj_3R_144() { - if (jj_scan_token(MAX)) return true; + static private boolean jj_3R_104() { + if (jj_3R_116()) return true; return false; } - static final private boolean jj_3R_146() { - if (jj_scan_token(AND)) return true; + static private boolean jj_3R_103() { + if (jj_3R_115()) return true; + return false; + } + + static private boolean jj_3R_27() { + if (jj_scan_token(REG_IDENT)) return true; return false; } - static final private boolean jj_3R_102() { + static private boolean jj_3R_102() { if (jj_3R_114()) return true; return false; } - static final private boolean jj_3R_92() { + static private boolean jj_3R_92() { if (jj_scan_token(DIVIDE)) return true; return false; } - static final private boolean jj_3R_101() { + static private boolean jj_3R_101() { if (jj_3R_113()) return true; return false; } - static final private boolean jj_3R_27() { - if (jj_scan_token(REG_IDENT)) return true; + static private boolean jj_3R_142() { + if (jj_scan_token(INIT)) return true; return false; } - static final private boolean jj_3R_100() { + static private boolean jj_3R_100() { if (jj_3R_112()) return true; return false; } - static final private boolean jj_3R_99() { + static private boolean jj_3R_99() { if (jj_3R_111()) return true; return false; } - static final private boolean jj_3R_142() { - if (jj_scan_token(INIT)) return true; + static private boolean jj_3R_98() { + if (jj_3R_110()) return true; return false; } - static final private boolean jj_3R_98() { - if (jj_3R_110()) return true; + static private boolean jj_3R_97() { + if (jj_3R_109()) return true; return false; } - static final private boolean jj_3R_97() { - if (jj_3R_109()) return true; + static private boolean jj_3R_149() { + if (jj_scan_token(COMMA)) return true; + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_96() { + static private boolean jj_3R_96() { if (jj_3R_108()) return true; return false; } - static final private boolean jj_3R_95() { + static private boolean jj_3R_95() { if (jj_3R_107()) return true; return false; } - static final private boolean jj_3R_149() { - if (jj_scan_token(COMMA)) return true; - if (jj_3R_34()) return true; + static private boolean jj_3R_148() { + if (jj_3R_27()) return true; return false; } - static final private boolean jj_3R_94() { + static private boolean jj_3R_94() { if (jj_3R_106()) return true; return false; } - static final private boolean jj_3R_84() { - if (jj_scan_token(MINUS)) return true; + static private boolean jj_3R_145() { + if (jj_scan_token(PLUS)) return true; return false; } - static final private boolean jj_3R_148() { - if (jj_3R_27()) return true; + static private boolean jj_3R_143() { + if (jj_scan_token(MIN)) return true; return false; } - static final private boolean jj_3R_145() { - if (jj_scan_token(PLUS)) return true; + static private boolean jj_3R_84() { + if (jj_scan_token(MINUS)) return true; return false; } - static final private boolean jj_3R_143() { - if (jj_scan_token(MIN)) return true; + static private boolean jj_3R_141() { + if (jj_3R_27()) return true; return false; } - static final private boolean jj_3R_141() { - if (jj_3R_27()) return true; + static private boolean jj_3R_117() { + if (jj_scan_token(FILTER)) return true; + if (jj_scan_token(LPARENTH)) return true; + Token xsp; + xsp = jj_scanpos; + if (jj_3R_143()) { + jj_scanpos = xsp; + if (jj_3R_144()) { + jj_scanpos = xsp; + 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; + } + } + } + } + } + if (jj_scan_token(COMMA)) return true; + if (jj_3R_34()) return true; + xsp = jj_scanpos; + if (jj_3R_149()) jj_scanpos = xsp; + if (jj_scan_token(RPARENTH)) return true; return false; } - static final private boolean jj_3R_93() { + static private boolean jj_3R_93() { Token xsp; xsp = jj_scanpos; if (jj_3R_94()) { @@ -3829,59 +3862,30 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_1() { + static 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_117() { - if (jj_scan_token(FILTER)) return true; - if (jj_scan_token(LPARENTH)) return true; - Token xsp; - xsp = jj_scanpos; - if (jj_3R_143()) { - jj_scanpos = xsp; - if (jj_3R_144()) { - jj_scanpos = xsp; - 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; - } - } - } - } - } - if (jj_scan_token(COMMA)) return true; - if (jj_3R_34()) return true; - xsp = jj_scanpos; - if (jj_3R_149()) jj_scanpos = xsp; - if (jj_scan_token(RPARENTH)) return true; + static private boolean jj_3R_90() { + if (jj_3R_93()) return true; return false; } - static final private boolean jj_3R_90() { - if (jj_3R_93()) return true; + static private boolean jj_3R_170() { + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_89() { + static private boolean jj_3R_89() { if (jj_scan_token(MINUS)) return true; if (jj_3R_81()) return true; return false; } - static final private boolean jj_3R_170() { - if (jj_3R_34()) return true; - return false; - } - - static final private boolean jj_3R_81() { + static private boolean jj_3R_81() { Token xsp; xsp = jj_scanpos; if (jj_3R_89()) { @@ -3891,12 +3895,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_91() { - if (jj_scan_token(TIMES)) return true; - return false; - } - - static final private boolean jj_3R_116() { + static private boolean jj_3R_116() { if (jj_scan_token(DQUOTE)) return true; Token xsp; xsp = jj_scanpos; @@ -3908,7 +3907,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_82() { + static private boolean jj_3R_91() { + if (jj_scan_token(TIMES)) return true; + return false; + } + + static private boolean jj_3R_82() { Token xsp; xsp = jj_scanpos; if (jj_3R_91()) { @@ -3919,12 +3923,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_5() { + static private boolean jj_3_5() { if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3R_76() { + static private boolean jj_3R_76() { if (jj_3R_81()) return true; Token xsp; while (true) { @@ -3934,12 +3938,20 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_83() { + static private boolean jj_3R_115() { + 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 private boolean jj_3R_83() { if (jj_scan_token(PLUS)) return true; return false; } - static final private boolean jj_3R_77() { + static private boolean jj_3R_77() { Token xsp; xsp = jj_scanpos; if (jj_3R_83()) { @@ -3950,15 +3962,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_115() { - 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_73() { + static private boolean jj_3R_73() { if (jj_3R_76()) return true; Token xsp; while (true) { @@ -3968,17 +3972,17 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_61() { - if (jj_3R_34()) return true; + static private boolean jj_3R_140() { + if (jj_3R_155()) return true; return false; } - static final private boolean jj_3R_140() { - if (jj_3R_155()) return true; + static private boolean jj_3R_61() { + if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_114() { + static private boolean jj_3R_114() { if (jj_scan_token(E)) return true; if (jj_scan_token(LBRACKET)) return true; if (jj_3R_34()) return true; @@ -3986,66 +3990,60 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_12() { + static private boolean jj_3_12() { if (jj_scan_token(DQUOTE)) return true; return false; } - static final private boolean jj_3R_74() { - if (jj_3R_78()) return true; - if (jj_3R_73()) return true; + static private boolean jj_3R_164() { + if (jj_scan_token(S)) return true; return false; } - static final private boolean jj_3R_71() { + static private boolean jj_3R_74() { + if (jj_3R_78()) return true; if (jj_3R_73()) return true; - Token xsp; - while (true) { - xsp = jj_scanpos; - if (jj_3R_74()) { jj_scanpos = xsp; break; } - } return false; } - static final private boolean jj_3R_164() { - if (jj_scan_token(S)) return true; - return false; - } - - static final private boolean jj_3R_163() { + static private boolean jj_3R_163() { if (jj_scan_token(F)) return true; if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_162() { + static private boolean jj_3R_162() { 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_32() { - if (jj_scan_token(AND)) return true; - if (jj_3R_31()) return true; - return false; - } - - static final private boolean jj_3R_161() { + static private boolean jj_3R_161() { 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_169() { + static private boolean jj_3R_71() { + if (jj_3R_73()) return true; + Token xsp; + while (true) { + xsp = jj_scanpos; + if (jj_3R_74()) { jj_scanpos = xsp; break; } + } + return false; + } + + static private boolean jj_3R_169() { 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_139() { + static private boolean jj_3R_139() { Token xsp; xsp = jj_scanpos; if (jj_3R_161()) { @@ -4061,23 +4059,29 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_63() { + static private boolean jj_3R_32() { + if (jj_scan_token(AND)) return true; + if (jj_3R_31()) return true; + return false; + } + + static private boolean jj_3R_63() { if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_59() { + static private boolean jj_3R_59() { if (jj_3R_34()) return true; return false; } - static final private boolean jj_3R_72() { + static private boolean jj_3R_72() { if (jj_3R_75()) return true; if (jj_3R_71()) return true; return false; } - static final private boolean jj_3R_70() { + static private boolean jj_3R_70() { if (jj_3R_71()) return true; Token xsp; while (true) { @@ -4087,16 +4091,7 @@ 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_3R_166() { + static private boolean jj_3R_166() { if (jj_scan_token(LBRACE)) return true; Token xsp; xsp = jj_scanpos; @@ -4108,18 +4103,27 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_69() { + static 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 private boolean jj_3R_69() { if (jj_3R_70()) return true; return false; } - static final private boolean jj_3R_68() { + static private boolean jj_3R_68() { if (jj_scan_token(NOT)) return true; if (jj_3R_66()) return true; return false; } - static final private boolean jj_3R_30() { + static private boolean jj_3R_30() { if (jj_3R_31()) return true; Token xsp; while (true) { @@ -4129,12 +4133,12 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3_4() { + static private boolean jj_3_4() { if (jj_3R_28()) return true; return false; } - static final private boolean jj_3R_66() { + static private boolean jj_3R_66() { Token xsp; xsp = jj_scanpos; if (jj_3R_68()) { @@ -4144,7 +4148,7 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_28() { + static private boolean jj_3R_28() { Token xsp; xsp = jj_scanpos; if (jj_3R_30()) { @@ -4154,56 +4158,60 @@ public class PrismParser implements PrismParserConstants { return false; } - static final private boolean jj_3R_156() { + static private boolean jj_3R_156() { if (jj_3R_166()) return true; return false; } - static final private boolean jj_3R_67() { + static private boolean jj_3R_67() { if (jj_scan_token(AND)) return true; if (jj_3R_66()) return true; return false; } static private boolean jj_initialized_once = false; + /** Generated Token Manager. */ static public PrismParserTokenManager token_source; static SimpleCharStream jj_input_stream; - static public Token token, jj_nt; + /** Current token. */ + static public Token token; + /** Next token. */ + static public Token jj_nt; static private int jj_ntk; static private Token jj_scanpos, jj_lastpos; static private int jj_la; - static public boolean lookingAhead = false; - static private boolean jj_semLA; static private int jj_gen; static final private int[] jj_la1 = new int[83]; static private int[] jj_la1_0; static private int[] jj_la1_1; static private int[] jj_la1_2; static { - jj_la1_0(); - jj_la1_1(); - jj_la1_2(); + jj_la1_init_0(); + jj_la1_init_1(); + jj_la1_init_2(); } - private static void jj_la1_0() { + private static void jj_la1_init_0() { jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x30,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,}; } - private static void jj_la1_1() { + private static void jj_la1_init_1() { jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x20127ab8,0x4000000,0x20127ab8,0x20127ab8,0x4000000,0x20127ab8,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x80000000,0x0,0x0,0x80000000,0x0,0x0,0x2012783a,0x200000,0x20020000,0x8000000,0xa012783a,0x0,0x80000000,0x8000000,0x0,0x8000000,0x8000000,0x0,0x20000000,0xc2000,0x80000000,0xc2000,0x2,0x80000000,0x2012783a,0x2012783a,0x2012783a,0x2012783a,0x80000000,0x0,0x800000,0x400000,0x200000,0x20127838,0x0,0x0,0x0,0x0,0x0,0x0,0x20027838,0x20027838,0x20000000,0x0,0x0,0x8000000,0x20000,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x2012783a,0x4000,0x0,0x600000,0x8000000,0x0,0x0,0x0,0x2000000,}; } - private static void jj_la1_2() { + private static void jj_la1_init_2() { jj_la1_2 = new int[] {0x0,0x0,0x0,0x170400,0x0,0x170400,0x170400,0x0,0x170400,0x0,0x0,0x0,0x0,0x0,0x8,0x0,0x0,0x100000,0x0,0x0,0x100000,0x200,0x170400,0x0,0x0,0x0,0x170400,0x100000,0x0,0x0,0x1002,0x0,0x0,0x1002,0x100000,0x0,0x1a0,0x0,0x0,0x1a0,0x170400,0x170400,0x170400,0x170400,0x1a0,0x8000,0x0,0x0,0x0,0x170400,0x18,0x1e0,0x600,0x600,0x1800,0x1800,0x170400,0x170000,0x0,0x0,0x100000,0x0,0x60000,0x1e8,0x0,0x2,0x2,0x0,0x1e8,0x2,0x2,0x1e8,0x0,0x2,0x170400,0x0,0x100000,0x100200,0x0,0x100000,0x18,0x1e0,0x0,}; } static final private JJCalls[] jj_2_rtns = new JJCalls[12]; static private boolean jj_rescan = false; static private int jj_gc = 0; + /** Constructor with InputStream. */ public PrismParser(java.io.InputStream stream) { this(stream, null); } + /** Constructor with InputStream and supplied encoding */ public PrismParser(java.io.InputStream stream, String encoding) { if (jj_initialized_once) { - System.out.println("ERROR: Second call to constructor of static parser. You must"); - System.out.println(" either use ReInit() or set the JavaCC option STATIC to false"); + System.out.println("ERROR: Second call to constructor of static parser. "); + System.out.println(" You must either use ReInit() or set the JavaCC option STATIC to false"); System.out.println(" during parser generation."); throw new Error(); } @@ -4217,9 +4225,11 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } + /** Reinitialise. */ static public void ReInit(java.io.InputStream stream) { ReInit(stream, null); } + /** Reinitialise. */ static public void ReInit(java.io.InputStream stream, String encoding) { try { jj_input_stream.ReInit(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); } token_source.ReInit(jj_input_stream); @@ -4230,10 +4240,11 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } + /** Constructor. */ public PrismParser(java.io.Reader stream) { if (jj_initialized_once) { - System.out.println("ERROR: Second call to constructor of static parser. You must"); - System.out.println(" either use ReInit() or set the JavaCC option STATIC to false"); + System.out.println("ERROR: Second call to constructor of static parser. "); + System.out.println(" You must either use ReInit() or set the JavaCC option STATIC to false"); System.out.println(" during parser generation."); throw new Error(); } @@ -4247,6 +4258,7 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } + /** Reinitialise. */ static public void ReInit(java.io.Reader stream) { jj_input_stream.ReInit(stream, 1, 1); token_source.ReInit(jj_input_stream); @@ -4257,10 +4269,11 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } + /** Constructor with generated Token Manager. */ public PrismParser(PrismParserTokenManager tm) { if (jj_initialized_once) { - System.out.println("ERROR: Second call to constructor of static parser. You must"); - System.out.println(" either use ReInit() or set the JavaCC option STATIC to false"); + System.out.println("ERROR: Second call to constructor of static parser. "); + System.out.println(" You must either use ReInit() or set the JavaCC option STATIC to false"); System.out.println(" during parser generation."); throw new Error(); } @@ -4273,6 +4286,7 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } + /** Reinitialise. */ public void ReInit(PrismParserTokenManager tm) { token_source = tm; token = new Token(); @@ -4282,7 +4296,7 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls(); } - static final private Token jj_consume_token(int kind) throws ParseException { + static private Token jj_consume_token(int kind) throws ParseException { Token oldToken; if ((oldToken = token).next != null) token = token.next; else token = token.next = token_source.getNextToken(); @@ -4308,7 +4322,7 @@ public class PrismParser implements PrismParserConstants { static private final class LookaheadSuccess extends java.lang.Error { } static final private LookaheadSuccess jj_ls = new LookaheadSuccess(); - static final private boolean jj_scan_token(int kind) { + static private boolean jj_scan_token(int kind) { if (jj_scanpos == jj_lastpos) { jj_la--; if (jj_scanpos.next == null) { @@ -4329,6 +4343,8 @@ public class PrismParser implements PrismParserConstants { return false; } + +/** Get the next Token. */ static final public Token getNextToken() { if (token.next != null) token = token.next; else token = token.next = token_source.getNextToken(); @@ -4337,8 +4353,9 @@ public class PrismParser implements PrismParserConstants { return token; } +/** Get the specific Token. */ static final public Token getToken(int index) { - Token t = lookingAhead ? jj_scanpos : token; + Token t = token; for (int i = 0; i < index; i++) { if (t.next != null) t = t.next; else t = t.next = token_source.getNextToken(); @@ -4346,14 +4363,14 @@ public class PrismParser implements PrismParserConstants { return t; } - static final private int jj_ntk() { + static private int jj_ntk() { if ((jj_nt=token.next) == null) return (jj_ntk = (token.next=token_source.getNextToken()).kind); else return (jj_ntk = jj_nt.kind); } - static private java.util.Vector jj_expentries = new java.util.Vector(); + static private java.util.List jj_expentries = new java.util.ArrayList(); static private int[] jj_expentry; static private int jj_kind = -1; static private int[] jj_lasttokens = new int[100]; @@ -4368,31 +4385,26 @@ public class PrismParser implements PrismParserConstants { for (int i = 0; i < jj_endpos; i++) { jj_expentry[i] = jj_lasttokens[i]; } - boolean exists = false; - for (java.util.Enumeration e = jj_expentries.elements(); e.hasMoreElements();) { - int[] oldentry = (int[])(e.nextElement()); + jj_entries_loop: for (java.util.Iterator it = jj_expentries.iterator(); it.hasNext();) { + int[] oldentry = (int[])(it.next()); if (oldentry.length == jj_expentry.length) { - exists = true; for (int i = 0; i < jj_expentry.length; i++) { if (oldentry[i] != jj_expentry[i]) { - exists = false; - break; + continue jj_entries_loop; } } - if (exists) break; + jj_expentries.add(jj_expentry); + break jj_entries_loop; } } - if (!exists) jj_expentries.addElement(jj_expentry); if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind; } } + /** Generate ParseException. */ static public ParseException generateParseException() { - jj_expentries.removeAllElements(); + jj_expentries.clear(); boolean[] la1tokens = new boolean[87]; - for (int i = 0; i < 87; i++) { - la1tokens[i] = false; - } if (jj_kind >= 0) { la1tokens[jj_kind] = true; jj_kind = -1; @@ -4416,7 +4428,7 @@ public class PrismParser implements PrismParserConstants { if (la1tokens[i]) { jj_expentry = new int[1]; jj_expentry[0] = i; - jj_expentries.addElement(jj_expentry); + jj_expentries.add(jj_expentry); } } jj_endpos = 0; @@ -4424,18 +4436,20 @@ public class PrismParser implements PrismParserConstants { jj_add_error_token(0, 0); int[][] exptokseq = new int[jj_expentries.size()][]; for (int i = 0; i < jj_expentries.size(); i++) { - exptokseq[i] = (int[])jj_expentries.elementAt(i); + exptokseq[i] = jj_expentries.get(i); } return new ParseException(token, exptokseq, tokenImage); } + /** Enable tracing. */ static final public void enable_tracing() { } + /** Disable tracing. */ static final public void disable_tracing() { } - static final private void jj_rescan_token() { + static private void jj_rescan_token() { jj_rescan = true; for (int i = 0; i < 12; i++) { try { @@ -4465,7 +4479,7 @@ public class PrismParser implements PrismParserConstants { jj_rescan = false; } - static final private void jj_save(int index, int xla) { + static private void jj_save(int index, int xla) { JJCalls p = jj_2_rtns[index]; while (p.gen > jj_gen) { if (p.next == null) { p = p.next = new JJCalls(); break; } diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index dbe235ed..9ba93d14 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1425,7 +1425,7 @@ Expression ExpressionProb(boolean prop, boolean pathprop) : // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - String filterOp = isBool ? "&" : filter.minRequested() ? "min" : "max"; + String filterOp = isBool ? "&" : filter.getFilterOpString(); ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); return ef; @@ -1462,14 +1462,15 @@ Expression ExpressionSS(boolean prop, boolean pathprop) : Filter filter = null; ExpressionSS ret = new ExpressionSS(); Token begin; + boolean isBool; } { // This production is only allowed in expressions if the "prop" parameter is true { if (!prop) throw generateParseException(); } // Various options for "S" keyword and attached symbols begin = ( - ( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; } ) | - ( { relOp = "="; } ) + ( r = LtGt() prob = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) | + ( { relOp = "="; isBool = false; } ) ) // Expression, optional filter expr = Expression(prop, pathprop) (filter = Filter())? @@ -1482,7 +1483,8 @@ Expression ExpressionSS(boolean prop, boolean pathprop) : // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression()); + String filterOp = isBool ? "&" : filter.getFilterOpString(); + ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); return ef; } @@ -1502,19 +1504,20 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : Filter filter = null; ExpressionReward ret = new ExpressionReward(); Token begin; + boolean isBool; } { // This production is only allowed in expressions if the "prop" parameter is true { if (!prop) throw generateParseException(); } // Various options for "R" keyword and attached symbols (( begin = (index = RewardIndex())? - (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; } ) - |( { relOp = "="; } ) - |( { relOp = "min="; } ) - |( { relOp = "max="; } ))) + (( r = LtGt() rew = Expression(false, false) { relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true; } ) + |( { relOp = "="; isBool = false; } ) + |( { relOp = "min="; isBool = false; } ) + |( { relOp = "max="; isBool = false; } ))) // These two are dupes of above but allow space to be omitted - |( begin = { relOp = "min="; } ) - |( begin = { relOp = "max="; } )) + |( begin = { relOp = "min="; isBool = false; } ) + |( begin = { relOp = "max="; isBool = false; } )) // Path formula, optional filter expr = ExpressionRewardContents(prop, pathprop) (filter = Filter())? { @@ -1527,7 +1530,8 @@ Expression ExpressionReward(boolean prop, boolean pathprop) : // Filter is actually dealt with by wrapping this expression in // an (invisible) ExpressionFilter expression if (filter != null) { - ExpressionFilter ef = new ExpressionFilter(filter.minRequested() ? "min" : "max", ret, filter.getExpression()); + String filterOp = isBool ? "&" : filter.getFilterOpString(); + ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression()); ef.setInvisible(true); return ef; } diff --git a/prism/src/parser/PrismParserConstants.java b/prism/src/parser/PrismParserConstants.java index fec8d3f4..3b0a4f7d 100644 --- a/prism/src/parser/PrismParserConstants.java +++ b/prism/src/parser/PrismParserConstants.java @@ -1,98 +1,192 @@ /* Generated By:JavaCC: Do not edit this line. PrismParserConstants.java */ package parser; + +/** + * Token literal values and constants. + * Generated by org.javacc.parser.OtherFilesGen#start() + */ public interface PrismParserConstants { + /** End of File. */ int EOF = 0; + /** RegularExpression Id. */ int WHITESPACE = 1; + /** RegularExpression Id. */ int COMMENT = 2; + /** RegularExpression Id. */ int A = 3; + /** RegularExpression Id. */ int BOOL = 4; + /** RegularExpression Id. */ int CLOCK = 5; + /** RegularExpression Id. */ int CONST = 6; + /** RegularExpression Id. */ int CTMC = 7; + /** RegularExpression Id. */ int C = 8; + /** RegularExpression Id. */ int DOUBLE = 9; + /** RegularExpression Id. */ int DTMC = 10; + /** RegularExpression Id. */ int E = 11; + /** RegularExpression Id. */ int ENDINIT = 12; + /** RegularExpression Id. */ int ENDINVARIANT = 13; + /** RegularExpression Id. */ int ENDMODULE = 14; + /** RegularExpression Id. */ int ENDREWARDS = 15; + /** RegularExpression Id. */ int ENDSYSTEM = 16; + /** RegularExpression Id. */ int FALSE = 17; + /** RegularExpression Id. */ int FORMULA = 18; + /** RegularExpression Id. */ int FILTER = 19; + /** RegularExpression Id. */ int FUNC = 20; + /** RegularExpression Id. */ int F = 21; + /** RegularExpression Id. */ int GLOBAL = 22; + /** RegularExpression Id. */ int G = 23; + /** RegularExpression Id. */ int INIT = 24; + /** RegularExpression Id. */ int INVARIANT = 25; + /** RegularExpression Id. */ int I = 26; + /** RegularExpression Id. */ int INT = 27; + /** RegularExpression Id. */ int LABEL = 28; + /** RegularExpression Id. */ int MAX = 29; + /** RegularExpression Id. */ int MDP = 30; + /** RegularExpression Id. */ int MIN = 31; + /** RegularExpression Id. */ int MODULE = 32; + /** RegularExpression Id. */ int X = 33; + /** RegularExpression Id. */ int NONDETERMINISTIC = 34; + /** RegularExpression Id. */ int PMAX = 35; + /** RegularExpression Id. */ int PMIN = 36; + /** RegularExpression Id. */ int P = 37; + /** RegularExpression Id. */ int PROBABILISTIC = 38; + /** RegularExpression Id. */ int PROB = 39; + /** RegularExpression Id. */ int PTA = 40; + /** RegularExpression Id. */ int RATE = 41; + /** RegularExpression Id. */ int REWARDS = 42; + /** RegularExpression Id. */ int RMAX = 43; + /** RegularExpression Id. */ int RMIN = 44; + /** RegularExpression Id. */ int R = 45; + /** RegularExpression Id. */ int S = 46; + /** RegularExpression Id. */ int STOCHASTIC = 47; + /** RegularExpression Id. */ int SYSTEM = 48; + /** RegularExpression Id. */ int TRUE = 49; + /** RegularExpression Id. */ int U = 50; + /** RegularExpression Id. */ int W = 51; + /** RegularExpression Id. */ int NOT = 52; + /** RegularExpression Id. */ int AND = 53; + /** RegularExpression Id. */ int OR = 54; + /** RegularExpression Id. */ int IMPLIES = 55; + /** RegularExpression Id. */ int RARROW = 56; + /** RegularExpression Id. */ int COLON = 57; + /** RegularExpression Id. */ int SEMICOLON = 58; + /** RegularExpression Id. */ int COMMA = 59; + /** RegularExpression Id. */ int DOTS = 60; + /** RegularExpression Id. */ int LPARENTH = 61; + /** RegularExpression Id. */ int RPARENTH = 62; + /** RegularExpression Id. */ int LBRACKET = 63; + /** RegularExpression Id. */ int RBRACKET = 64; + /** RegularExpression Id. */ int LBRACE = 65; + /** RegularExpression Id. */ int RBRACE = 66; + /** RegularExpression Id. */ int EQ = 67; + /** RegularExpression Id. */ int NE = 68; + /** RegularExpression Id. */ int LT = 69; + /** RegularExpression Id. */ int GT = 70; + /** RegularExpression Id. */ int LE = 71; + /** RegularExpression Id. */ int GE = 72; + /** RegularExpression Id. */ int PLUS = 73; + /** RegularExpression Id. */ int MINUS = 74; + /** RegularExpression Id. */ int TIMES = 75; + /** RegularExpression Id. */ int DIVIDE = 76; + /** RegularExpression Id. */ int PRIME = 77; + /** RegularExpression Id. */ int RENAME = 78; + /** RegularExpression Id. */ int QMARK = 79; + /** RegularExpression Id. */ int DQUOTE = 80; + /** RegularExpression Id. */ int REG_INT = 81; + /** RegularExpression Id. */ int REG_DOUBLE = 82; + /** RegularExpression Id. */ int REG_IDENTPRIME = 83; + /** RegularExpression Id. */ int REG_IDENT = 84; + /** RegularExpression Id. */ int PREPROC = 85; + /** RegularExpression Id. */ int LEXICAL_ERROR = 86; + /** Lexical state. */ int DEFAULT = 0; + /** Literal token values. */ String[] tokenImage = { "", "", diff --git a/prism/src/parser/PrismParserTokenManager.java b/prism/src/parser/PrismParserTokenManager.java index 0273d508..5c8a059f 100644 --- a/prism/src/parser/PrismParserTokenManager.java +++ b/prism/src/parser/PrismParserTokenManager.java @@ -7,9 +7,13 @@ import parser.type.*; import prism.ModelType; import prism.PrismLangException; +/** Token Manager. */ public class PrismParserTokenManager implements PrismParserConstants { + + /** Debug output. */ public static java.io.PrintStream debugStream = System.out; + /** Set debug output. */ public static void setDebugStream(java.io.PrintStream ds) { debugStream = ds; } private static final int jjStopStringLiteralDfa_0(int pos, long active0, long active1) { @@ -169,21 +173,13 @@ private static final int jjStartNfa_0(int pos, long active0, long active1) { return jjMoveNfa_0(jjStopStringLiteralDfa_0(pos, active0, active1), pos + 1); } -static private final int jjStopAtPos(int pos, int kind) +static private int jjStopAtPos(int pos, int kind) { jjmatchedKind = kind; jjmatchedPos = pos; return pos + 1; } -static private final int jjStartNfaWithStates_0(int pos, int kind, int state) -{ - jjmatchedKind = kind; - jjmatchedPos = pos; - try { curChar = input_stream.readChar(); } - catch(java.io.IOException e) { return pos + 1; } - return jjMoveNfa_0(state, pos + 1); -} -static private final int jjMoveStringLiteralDfa0_0() +static private int jjMoveStringLiteralDfa0_0() { switch(curChar) { @@ -296,7 +292,7 @@ static private final int jjMoveStringLiteralDfa0_0() return jjMoveNfa_0(0, 0); } } -static private final int jjMoveStringLiteralDfa1_0(long active0, long active1) +static private int jjMoveStringLiteralDfa1_0(long active0, long active1) { try { curChar = input_stream.readChar(); } catch(java.io.IOException e) { @@ -356,10 +352,10 @@ static private final int jjMoveStringLiteralDfa1_0(long active0, long active1) } return jjStartNfa_0(0, active0, active1); } -static private final int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1, long active1) +static private int jjMoveStringLiteralDfa2_0(long old0, long active0, long old1, long active1) { if (((active0 &= old0) | (active1 &= old1)) == 0L) - return jjStartNfa_0(0, old0, old1); + return jjStartNfa_0(0, old0, old1); try { curChar = input_stream.readChar(); } catch(java.io.IOException e) { jjStopStringLiteralDfa_0(1, active0, 0L); @@ -414,7 +410,7 @@ static private final int jjMoveStringLiteralDfa2_0(long old0, long active0, long } return jjStartNfa_0(1, active0, 0L); } -static private final int jjMoveStringLiteralDfa3_0(long old0, long active0) +static private int jjMoveStringLiteralDfa3_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(1, old0, 0L); @@ -485,7 +481,7 @@ static private final int jjMoveStringLiteralDfa3_0(long old0, long active0) } return jjStartNfa_0(2, active0, 0L); } -static private final int jjMoveStringLiteralDfa4_0(long old0, long active0) +static private int jjMoveStringLiteralDfa4_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(2, old0, 0L); @@ -531,7 +527,7 @@ static private final int jjMoveStringLiteralDfa4_0(long old0, long active0) } return jjStartNfa_0(3, active0, 0L); } -static private final int jjMoveStringLiteralDfa5_0(long old0, long active0) +static private int jjMoveStringLiteralDfa5_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(3, old0, 0L); @@ -581,7 +577,7 @@ static private final int jjMoveStringLiteralDfa5_0(long old0, long active0) } return jjStartNfa_0(4, active0, 0L); } -static private final int jjMoveStringLiteralDfa6_0(long old0, long active0) +static private int jjMoveStringLiteralDfa6_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(4, old0, 0L); @@ -615,7 +611,7 @@ static private final int jjMoveStringLiteralDfa6_0(long old0, long active0) } return jjStartNfa_0(5, active0, 0L); } -static private final int jjMoveStringLiteralDfa7_0(long old0, long active0) +static private int jjMoveStringLiteralDfa7_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(5, old0, 0L); @@ -641,7 +637,7 @@ static private final int jjMoveStringLiteralDfa7_0(long old0, long active0) } return jjStartNfa_0(6, active0, 0L); } -static private final int jjMoveStringLiteralDfa8_0(long old0, long active0) +static private int jjMoveStringLiteralDfa8_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(6, old0, 0L); @@ -673,7 +669,7 @@ static private final int jjMoveStringLiteralDfa8_0(long old0, long active0) } return jjStartNfa_0(7, active0, 0L); } -static private final int jjMoveStringLiteralDfa9_0(long old0, long active0) +static private int jjMoveStringLiteralDfa9_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(7, old0, 0L); @@ -701,7 +697,7 @@ static private final int jjMoveStringLiteralDfa9_0(long old0, long active0) } return jjStartNfa_0(8, active0, 0L); } -static private final int jjMoveStringLiteralDfa10_0(long old0, long active0) +static private int jjMoveStringLiteralDfa10_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(8, old0, 0L); @@ -721,7 +717,7 @@ static private final int jjMoveStringLiteralDfa10_0(long old0, long active0) } return jjStartNfa_0(9, active0, 0L); } -static private final int jjMoveStringLiteralDfa11_0(long old0, long active0) +static private int jjMoveStringLiteralDfa11_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(9, old0, 0L); @@ -743,7 +739,7 @@ static private final int jjMoveStringLiteralDfa11_0(long old0, long active0) } return jjStartNfa_0(10, active0, 0L); } -static private final int jjMoveStringLiteralDfa12_0(long old0, long active0) +static private int jjMoveStringLiteralDfa12_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(10, old0, 0L); @@ -765,7 +761,7 @@ static private final int jjMoveStringLiteralDfa12_0(long old0, long active0) } return jjStartNfa_0(11, active0, 0L); } -static private final int jjMoveStringLiteralDfa13_0(long old0, long active0) +static private int jjMoveStringLiteralDfa13_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(11, old0, 0L); @@ -783,7 +779,7 @@ static private final int jjMoveStringLiteralDfa13_0(long old0, long active0) } return jjStartNfa_0(12, active0, 0L); } -static private final int jjMoveStringLiteralDfa14_0(long old0, long active0) +static private int jjMoveStringLiteralDfa14_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(12, old0, 0L); @@ -801,7 +797,7 @@ static private final int jjMoveStringLiteralDfa14_0(long old0, long active0) } return jjStartNfa_0(13, active0, 0L); } -static private final int jjMoveStringLiteralDfa15_0(long old0, long active0) +static private int jjMoveStringLiteralDfa15_0(long old0, long active0) { if (((active0 &= old0)) == 0L) return jjStartNfa_0(13, old0, 0L); @@ -821,47 +817,24 @@ static private final int jjMoveStringLiteralDfa15_0(long old0, long active0) } return jjStartNfa_0(14, active0, 0L); } -static private final void jjCheckNAdd(int state) -{ - if (jjrounds[state] != jjround) - { - jjstateSet[jjnewStateCnt++] = state; - jjrounds[state] = jjround; - } -} -static private final void jjAddStates(int start, int end) +static private int jjStartNfaWithStates_0(int pos, int kind, int state) { - do { - jjstateSet[jjnewStateCnt++] = jjnextStates[start]; - } while (start++ != end); -} -static private final void jjCheckNAddTwoStates(int state1, int state2) -{ - jjCheckNAdd(state1); - jjCheckNAdd(state2); -} -static private final void jjCheckNAddStates(int start, int end) -{ - do { - jjCheckNAdd(jjnextStates[start]); - } while (start++ != end); -} -static private final void jjCheckNAddStates(int start) -{ - jjCheckNAdd(jjnextStates[start]); - jjCheckNAdd(jjnextStates[start + 1]); + jjmatchedKind = kind; + jjmatchedPos = pos; + try { curChar = input_stream.readChar(); } + catch(java.io.IOException e) { return pos + 1; } + return jjMoveNfa_0(state, pos + 1); } static final long[] jjbitVec0 = { 0x0L, 0x0L, 0xffffffffffffffffL, 0xffffffffffffffffL }; -static private final int jjMoveNfa_0(int startState, int curPos) +static private int jjMoveNfa_0(int startState, int curPos) { - int[] nextStates; int startsAt = 0; jjnewStateCnt = 23; int i = 1; jjstateSet[0] = startState; - int j, kind = 0x7fffffff; + int kind = 0x7fffffff; for (;;) { if (++jjround == 0x7fffffff) @@ -869,7 +842,7 @@ static private final int jjMoveNfa_0(int startState, int curPos) if (curChar < 64) { long l = 1L << curChar; - MatchLoop: do + do { switch(jjstateSet[--i]) { @@ -1023,7 +996,7 @@ static private final int jjMoveNfa_0(int startState, int curPos) else if (curChar < 128) { long l = 1L << (curChar & 077); - MatchLoop: do + do { switch(jjstateSet[--i]) { @@ -1073,7 +1046,7 @@ static private final int jjMoveNfa_0(int startState, int curPos) { int i2 = (curChar & 0xff) >> 6; long l2 = 1L << (curChar & 077); - MatchLoop: do + do { switch(jjstateSet[--i]) { @@ -1105,6 +1078,8 @@ static private final int jjMoveNfa_0(int startState, int curPos) static final int[] jjnextStates = { 10, 11, 12, 18, 2, 3, 5, 20, 21, 22, 13, 14, 16, 17, }; + +/** Token literal values. */ public static final String[] jjstrLiteralImages = { "", null, null, "\101", "\142\157\157\154", "\143\154\157\143\153", "\143\157\156\163\164", "\143\164\155\143", "\103", "\144\157\165\142\154\145", "\144\164\155\143", @@ -1123,8 +1098,10 @@ public static final String[] jjstrLiteralImages = { "\135", "\173", "\175", "\75", "\41\75", "\74", "\76", "\74\75", "\76\75", "\53", "\55", "\52", "\57", "\47", "\74\55", "\77", "\42", null, null, null, null, null, null, }; + +/** Lexer state names. */ public static final String[] lexStateNames = { - "DEFAULT", + "DEFAULT", }; static final long[] jjtoToken = { 0xfffffffffffffff9L, 0x7fffffL, @@ -1139,15 +1116,20 @@ static protected SimpleCharStream input_stream; static private final int[] jjrounds = new int[23]; static private final int[] jjstateSet = new int[46]; static protected char curChar; +/** Constructor. */ public PrismParserTokenManager(SimpleCharStream stream){ if (input_stream != null) throw new TokenMgrError("ERROR: Second call to constructor of static lexer. You must use ReInit() to initialize the static variables.", TokenMgrError.STATIC_LEXER_ERROR); input_stream = stream; } + +/** Constructor. */ public PrismParserTokenManager(SimpleCharStream stream, int lexState){ this(stream); SwitchTo(lexState); } + +/** Reinitialise parser. */ static public void ReInit(SimpleCharStream stream) { jjmatchedPos = jjnewStateCnt = 0; @@ -1155,18 +1137,22 @@ static public void ReInit(SimpleCharStream stream) input_stream = stream; ReInitRounds(); } -static private final void ReInitRounds() +static private void ReInitRounds() { int i; jjround = 0x80000001; for (i = 23; i-- > 0;) jjrounds[i] = 0x80000000; } + +/** Reinitialise parser. */ static public void ReInit(SimpleCharStream stream, int lexState) { ReInit(stream); SwitchTo(lexState); } + +/** Switch to specified lex state. */ static public void SwitchTo(int lexState) { if (lexState >= 1 || lexState < 0) @@ -1177,14 +1163,27 @@ static public void SwitchTo(int lexState) static protected Token jjFillToken() { - Token t = Token.newToken(jjmatchedKind); - t.kind = jjmatchedKind; + final Token t; + final String curTokenImage; + final int beginLine; + final int endLine; + final int beginColumn; + final int endColumn; String im = jjstrLiteralImages[jjmatchedKind]; - t.image = (im == null) ? input_stream.GetImage() : im; - t.beginLine = input_stream.getBeginLine(); - t.beginColumn = input_stream.getBeginColumn(); - t.endLine = input_stream.getEndLine(); - t.endColumn = input_stream.getEndColumn(); + curTokenImage = (im == null) ? input_stream.GetImage() : im; + beginLine = input_stream.getBeginLine(); + beginColumn = input_stream.getBeginColumn(); + endLine = input_stream.getEndLine(); + endColumn = input_stream.getEndColumn(); + t = Token.newToken(jjmatchedKind); + t.kind = jjmatchedKind; + t.image = curTokenImage; + + t.beginLine = beginLine; + t.endLine = endLine; + t.beginColumn = beginColumn; + t.endColumn = endColumn; + return t; } @@ -1195,22 +1194,22 @@ static int jjround; static int jjmatchedPos; static int jjmatchedKind; +/** Get the next Token. */ public static Token getNextToken() { - int kind; Token specialToken = null; Token matchedToken; int curPos = 0; EOFLoop : for (;;) - { - try - { + { + try + { curChar = input_stream.BeginToken(); - } + } catch(java.io.IOException e) - { + { jjmatchedKind = 0; matchedToken = jjFillToken(); matchedToken.specialToken = specialToken; @@ -1273,4 +1272,31 @@ public static Token getNextToken() } } +static private void jjCheckNAdd(int state) +{ + if (jjrounds[state] != jjround) + { + jjstateSet[jjnewStateCnt++] = state; + jjrounds[state] = jjround; + } +} +static private void jjAddStates(int start, int end) +{ + do { + jjstateSet[jjnewStateCnt++] = jjnextStates[start]; + } while (start++ != end); +} +static private void jjCheckNAddTwoStates(int state1, int state2) +{ + jjCheckNAdd(state1); + jjCheckNAdd(state2); +} + +static private void jjCheckNAddStates(int start, int end) +{ + do { + jjCheckNAdd(jjnextStates[start]); + } while (start++ != end); +} + } diff --git a/prism/src/parser/ast/ExpressionFilter.java b/prism/src/parser/ast/ExpressionFilter.java index 70554fa3..7515fc29 100644 --- a/prism/src/parser/ast/ExpressionFilter.java +++ b/prism/src/parser/ast/ExpressionFilter.java @@ -34,7 +34,7 @@ public class ExpressionFilter extends Expression { // Enums for types of filter public enum FilterOperator { - MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, FORALL, EXISTS, PRINT; + MIN, MAX, ARGMIN, ARGMAX, COUNT, SUM, AVG, FIRST, RANGE, FORALL, EXISTS, PRINT; }; // Operator used in filter @@ -87,6 +87,8 @@ public class ExpressionFilter extends Expression opType = FilterOperator.AVG; else if (opName.equals("first")) opType = FilterOperator.FIRST; + else if (opName.equals("range")) + opType = FilterOperator.RANGE; else if (opName.equals("forall") || opName.equals("&")) opType = FilterOperator.FORALL; else if (opName.equals("exists") || opName.equals("|")) @@ -145,7 +147,7 @@ public class ExpressionFilter extends Expression */ public boolean isConstant() { - // Note: In some sense, ExpressionFilters are constant since they return the same + // Note: In some sense, ExpressionFilters are (often) constant since they return the same // value for every state. But the actual value is model dependent, so they are not // considered to be constants. return false; diff --git a/prism/src/parser/ast/Filter.java b/prism/src/parser/ast/Filter.java index fa21fa3d..0a645824 100644 --- a/prism/src/parser/ast/Filter.java +++ b/prism/src/parser/ast/Filter.java @@ -35,9 +35,9 @@ import prism.PrismLangException; public class Filter extends ASTElement { private Expression expr = null; - // Either "min" or "max" ("both" no longer supported) - // (and "min" is nominal default) - private boolean minReq = true; + // Either "min" or "max", or neither or both. + // In the latter case, this means "range" + private boolean minReq = false; private boolean maxReq = false; // Constructor @@ -83,6 +83,20 @@ public class Filter extends ASTElement return maxReq; } + /** + * Get (as a string) the operator for this filter + * (as need to construct an ExpressionFilter object) + * @return + */ + public String getFilterOpString() + { + if (minReq) { + return maxReq ? "range" : "min"; + } else { + return maxReq ? "max" : "range"; + } + } + // Methods required for ASTElement: /** diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 3b387da9..11dbba21 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/prism/src/parser/visitor/TypeCheck.java @@ -473,6 +473,13 @@ public class TypeCheck extends ASTTraverse throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter() .getExpression()); } + // Need to to do this type check here because some info has been lost when converted to ExpressionFilter + if (e.getProb() != null && e.getFilter() != null) { + if (e.getFilter().minRequested() || e.getFilter().maxRequested()) { + throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties"); + } + } + // Set type e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance()); } @@ -491,6 +498,13 @@ public class TypeCheck extends ASTTraverse throw new PrismLangException("Type error: R operator filter is not a Boolean", e.getFilter() .getExpression()); } + // Need to to do this type check here because some info has been lost when converted to ExpressionFilter + if (e.getReward() != null && e.getFilter() != null) { + if (e.getFilter().minRequested() || e.getFilter().maxRequested()) { + throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties"); + } + } + // Set type e.setType(e.getReward() == null ? TypeDouble.getInstance() : TypeBool.getInstance()); } @@ -503,6 +517,13 @@ public class TypeCheck extends ASTTraverse throw new PrismLangException("Type error: P operator filter is not a Boolean", e.getFilter() .getExpression()); } + // Need to to do this type check here because some info has been lost when converted to ExpressionFilter + if (e.getProb() != null && e.getFilter() != null) { + if (e.getFilter().minRequested() || e.getFilter().maxRequested()) { + throw new PrismLangException("Type error: Cannot use min/max filters in Boolean-valued properties"); + } + } + // Set type e.setType(e.getProb() == null ? TypeDouble.getInstance() : TypeBool.getInstance()); } @@ -539,6 +560,7 @@ public class TypeCheck extends ASTTraverse case ARGMAX: case SUM: case AVG: + case RANGE: if (t instanceof TypeBool) { throw new PrismLangException( "Type error: Boolean argument not allowed as operand for filter of type \"" @@ -567,6 +589,7 @@ public class TypeCheck extends ASTTraverse case MAX: case SUM: case FIRST: + case RANGE: case PRINT: e.setType(t); break; diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 8507db88..8a8d3024 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -1131,6 +1131,8 @@ public class StateModelChecker implements ModelChecker res = new StateValuesMTBDD(JDD.Constant(d), model); break; case FIRST: + case RANGE: + // TODO: Treat ranges properly if (empty) throw new PrismException("Can't select the first value from an empty filter"); d = vals.sumOverBDD(ddFilter) / JDD.GetNumMinterms(ddFilter, allDDRowVars.n());