/* Generated By:JavaCC: Do not edit this line. PrismParser.java */
package parser;

import java.io.*;
import java.util.List;
import java.util.ArrayList;

import parser.ast.*;
import parser.type.*;
import prism.ModelType;
import prism.PrismLangException;

public class PrismParser implements PrismParserConstants {
        // The modules file associated with properties file being parsed
        private static ModulesFile modulesFile;

        // List of keyword strings
        private static ArrayList<String> keywordList = new ArrayList<String>();
        {
                keywordList.clear();
                for (int i = PrismParserConstants.COMMENT+1; i < PrismParserConstants.NOT; i++) {
                        keywordList.add(PrismParserConstants.tokenImage[i].replaceAll("\u005c"", ""));
                }
        }

        //-----------------------------------------------------------------------------------
        // Main method for testing purposes
        //-----------------------------------------------------------------------------------

        public static void main(String[] args)
        {
                PrismParser p = null;
                InputStream str = null;
                String src = null;

                try {
                        if (args.length == 0) {
                                System.out.println("Usage: java parser.PrismParser <switch> [<file>]");
                                System.out.println("Where: <switch> = -modulesfile or -mf");
                                System.out.println("                  -propertiesfile or -pf");
                                System.out.println("                  -expression or -e");
                                System.exit(1);
                        }

                        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+"...\u005cn");

                        if (args[0].equals("-modulesfile") || args[0].equals("-mf")) {
                                ModulesFile mf = p.parseModulesFile(str);
                                System.out.print("Modules file:\u005cn=============\u005cn\u005cn" + mf);
                                System.out.print("\u005cnTree:\u005cn=====\u005cn" + mf.toTreeString());
                                mf.tidyUp();
                                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:\u005cn================\u005cn\u005cn" + pf);
                                System.out.print("\u005cnTree:\u005cn=====\u005cn" + pf.toTreeString());
                                pf.tidyUp();
                                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:\u005cn=====\u005cn" + expr.toTreeString());
                                expr.typeCheck();
                                expr.semanticCheck();
                                System.out.println("Type: " + expr.getType().getTypeString());
                                System.out.println("Eval: " + expr.evaluate());
                        } else {
                                System.out.println("Unknown switch"); System.exit(1);
                        }
                }
                catch (PrismLangException e) {
                        System.out.println("Error in "+src+": " + e.getMessage()+"."); System.exit(1);
                }
                catch (FileNotFoundException e) {
                        System.out.println(e); System.exit(1);
                }
        }

        //-----------------------------------------------------------------------------------
        // Methods called by Prism
        //-----------------------------------------------------------------------------------

        // Constructor

        public PrismParser()
        {
                // Call default constructor
                this(System.in);
        }

        // Parse modules file

        public ModulesFile parseModulesFile(InputStream str) throws PrismLangException { return parseModulesFile(str, null); }

        public ModulesFile parseModulesFile(InputStream str, ModelType typeOverride) throws PrismLangException
        {
                ModulesFile mf = null;

                // (Re)start parser
                ReInit(str);
                // Parse
                try {
                        mf = ModulesFile();
                }
                catch (ParseException e) {
                        throw generateSyntaxError(e);
                }
                // Override type of model if requested
                if (typeOverride != null) {
                        mf.setModelType(typeOverride);
                }

                return mf;
        }

        // Parse properties file (pass ModulesFile in to get at its constants)

        public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str) throws PrismLangException
        { return parsePropertiesFile(mf, str, false); }

        public PropertiesFile parsePropertiesFile(ModulesFile mf, InputStream str, boolean strict) throws PrismLangException
        {
                PropertiesFile pf = null;

                // (Re)start parser
                ReInit(str);
                modulesFile = mf;
                // Parse
                try {
                        pf = strict ? PropertiesFile() : PropertiesFileSemicolonless();
                }
                catch (ParseException e) {
                        throw generateSyntaxError(e);
                }

                return pf;
        }

        // Parse a single expression

        public Expression parseSingleExpression(InputStream str) throws PrismLangException
        {
                Expression expr = null;

                // (Re)start parser
                ReInit(str);
                // Parse
                try {
                        expr = SingleExpression();
                }
                catch (ParseException e) {
                        throw generateSyntaxError(e);
                }
                return expr;
        }

        // Parse a for loop

        public ForLoop parseForLoop(InputStream str) throws PrismLangException
        {
                ForLoop fl = null;

                // (Re)start parser
                ReInit(str);
                // Parse
                try {
                        fl = ForLoop();
                }
                catch (ParseException e) {
                        throw generateSyntaxError(e);
                }
                return fl;
        }

        //-----------------------------------------------------------------------------------
        // Some utility methods
        //-----------------------------------------------------------------------------------

        /**
	 * Get comment block directly preceding a token and remove "//" characters
	 */
        public static String getPrecedingCommentBlock(Token firstToken)
        {
                String comment = "", s;
                Token t = firstToken;

                // extract any comment from the previous lines of the file
                if (t.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\u005c\u005cn\u005c\u005cr]*"))) {
                        // trace back thru special tokens that are comments
                        t = t.specialToken;
                        while (t.specialToken != null && !(t.specialToken.kind == PrismParserConstants.WHITESPACE && t.specialToken.image.matches("[\u005c\u005cn\u005c\u005cr]*")))
                                t = t.specialToken;
                        // concatenate comment special tokens
                        while (t != null) {
                                s = t.image;
                                // strip any nasty carriage returns
                                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("[ \u005ct]"))
                                                comment = comment.substring(0,comment.length()-1);
                                        s = s.substring(2);
                                        s = s.replaceFirst("[ \u005ct]*", "");
                                }
                                comment += s;
                                t = t.next;
                        }
                }
                // remove final new line (if present)
                if (comment.length() > 0 && (comment.charAt(comment.length()-1) == '\u005cn'))
                        comment = comment.substring(0,comment.length()-1);

                return comment;
        }

        // Add "//"s into comment block

        public static String slashCommentBlock(String comment)
        {
                int i;
                String s, res = "";
                // break into lines
                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 += "\u005cn";
                }
                // deal with any trailing characters (with no new line ending them)
                if (comment.trim().length()>0) res += "// " + comment + "\u005cn";
                return res;
        }

        /**
	 * Test a string to see if it is a PRISM language keyword.
	 */
        public static boolean isKeyword(String s)
        {
                return keywordList.contains(s);
        }

        /**
	 * Get access to the list of all PRISM language keywords.
	 */
        public static List<String> getListOfKeywords()
        {
                return keywordList;
        }

        /**
	 * Set the tab size used by the lexer/parser.
	 */
        public void setTabSize(int size)
        {
                SimpleCharStream.setTabSize(size);
        }

        /**
	 * Get the tab size used by the lexer/parser.
	 */
        public int getTabSize()
        {
                return SimpleCharStream.getTabSize(0);
        }

        /**
	 * Generate a syntax error (PrismLangException) from a ParseException.
	 */
        protected PrismLangException generateSyntaxError(ParseException e)
        {
                if (e == null) return new PrismLangException("Syntax error");
                // No token: was prob created manually so use message if present
                if (e.currentToken == null) {
                        String msg = e.getMessage();
                        String exMsg = "Syntax error";
                        if (msg != null && msg.length() > 0)
                                exMsg += ": " + msg;
                        return new PrismLangException(exMsg);
                }
                // Use current/next token to find location of error
                // But don't use error message if too long (esp if generated by JavaCC)
                else {
                        ExpressionIdent tmp;
                        if (e.currentToken.next == null) {
                                tmp = new ExpressionIdent(e.currentToken.image);
                                tmp.setPosition(e.currentToken);
                        } else {
                                tmp = new ExpressionIdent(e.currentToken.next.image);
                                tmp.setPosition(e.currentToken.next);
                        }
                        String msg = e.getMessage();
                        String exMsg = "Syntax error";
                        if (msg != null && msg.length() > 0 && msg.length() < 20)
                                exMsg += ": " + msg;
                        return new PrismLangException(exMsg, tmp);
                }
        }

        //-----------------------------------------------------------------------------------
        // A few classes for temporary storage of bits of the AST
        //-----------------------------------------------------------------------------------

        static class ExpressionPair { public Expression expr1 = null; public Expression expr2 = null; }

//-----------------------------------------------------------------------------------
// Top-level productions
//-----------------------------------------------------------------------------------

// Modules file
  static final public ModulesFile ModulesFile() throws ParseException, PrismLangException {
        ModelType type = ModelType.MDP;
        int typeCount = 0;
        Token typeDupe = null;
        Declaration global;
        Module m = null;
        RenamedModule rm = null;
        RewardStruct rs = null;
        Expression init = null;
        int initCount = 0;
        Expression initDupe = null;
        SystemDefn sys = null;
        int sysCount = 0;
        SystemDefn sysDupe = null;
        ModulesFile mf = new ModulesFile();
        Token begin = null;
    label_1:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case CONST:
      case CTMC:
      case DTMC:
      case FORMULA:
      case GLOBAL:
      case INIT:
      case LABEL:
      case MDP:
      case MODULE:
      case NONDETERMINISTIC:
      case PROBABILISTIC:
      case PROB:
      case PTA:
      case RATE:
      case REWARDS:
      case STOCHASTIC:
      case SYSTEM:
        ;
        break;
      default:
        jj_la1[0] = jj_gen;
        break label_1;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case CTMC:
      case DTMC:
      case MDP:
      case NONDETERMINISTIC:
      case PROBABILISTIC:
      case PTA:
      case STOCHASTIC:
            begin = getToken(1);
        type = ModulesFileType();
                                   typeCount++; if (typeCount == 2) typeDupe = getToken(0);
        break;
      case FORMULA:
        FormulaDef(mf.getFormulaList());
        break;
      case LABEL:
        LabelDef(mf.getLabelList());
        break;
      case CONST:
      case PROB:
      case RATE:
        ConstantDef(mf.getConstantList());
        break;
      case GLOBAL:
        // Global variable
                global = GlobalDecl();
                                mf.addGlobal(global);
        break;
      default:
        jj_la1[1] = jj_gen;
        if (jj_2_1(2147483647)) {
          rm = RenamedModule();
                                                                     mf.addRenamedModule(rm);
        } else {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case MODULE:
            // Module
                    m = Module();
                       mf.addModule(m);
            break;
          case REWARDS:
            // Reward structure
                    rs = RewardStruct();
                              mf.addRewardStruct(rs);
            break;
          case INIT:
            // Initial states ("init...endinit" construct)
                    init = Init();
                        mf.setInitialStates(init); initCount++; if (initCount == 2) initDupe = init;
            break;
          case SYSTEM:
            // System definition ("system...endsystem" construct)
                    sys = SystemEndsystem();
                                  mf.setSystemDefn(sys); sysCount++; if (sysCount == 2) sysDupe = sys;
            break;
          default:
            jj_la1[2] = jj_gen;
            jj_consume_token(-1);
            throw new ParseException();
          }
        }
      }
    }
    jj_consume_token(0);
                // Check for multiple instances of some items
                if (typeDupe != null) {
                        ExpressionIdent tmp = new ExpressionIdent(typeDupe.image);
                        tmp.setPosition(typeDupe);
                        {if (true) throw new PrismLangException("There were multiple model type declarations", tmp);}
                }
                if (initDupe != null) {
                        {if (true) throw new PrismLangException("There were multiple init...endinit constructs", initDupe);}
                }
                if (sysDupe != null) {
                        {if (true) throw new PrismLangException("There were multiple system...endsystem constructs", sysDupe);}
                }

                // Set model type (note default is MDP)
                mf.setModelType(type);

                // Return completed ModulesFile object
                mf.setPosition(begin != null? begin: getToken(0), getToken(0));
                {if (true) return mf;}
    throw new Error("Missing return statement in function");
  }

// Properties file
  static final public PropertiesFile PropertiesFile() throws ParseException, PrismLangException {
        PropertiesFile pf = new PropertiesFile(modulesFile);
        Property prop;
        Token begin = null;
          begin = getToken(1);
    label_2:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case CONST:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case LABEL:
      case MAX:
      case MIN:
      case PMAX:
      case PMIN:
      case P:
      case PROB:
      case RATE:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        ;
        break;
      default:
        jj_la1[3] = jj_gen;
        break label_2;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case MAX:
      case MIN:
      case PMAX:
      case PMIN:
      case P:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        prop = Property();
                                      pf.addProperty(prop);
        label_3:
        while (true) {
          jj_consume_token(SEMICOLON);
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case SEMICOLON:
            ;
            break;
          default:
            jj_la1[4] = jj_gen;
            break label_3;
          }
        }
        break;
      case LABEL:
        LabelDef(pf.getLabelList());
        break;
      case CONST:
      case PROB:
      case RATE:
        ConstantDef(pf.getConstantList());
        break;
      default:
        jj_la1[5] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
    jj_consume_token(0);
          pf.setPosition(begin, getToken(0)); {if (true) return pf;}
    throw new Error("Missing return statement in function");
  }

// Properties file with optional semicolons - beware of potential ambiguities
  static final public PropertiesFile PropertiesFileSemicolonless() throws ParseException, PrismLangException {
        PropertiesFile pf = new PropertiesFile(modulesFile);
        Property prop;
        Token begin = null;
          begin = getToken(1);
    label_4:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case CONST:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case LABEL:
      case MAX:
      case MIN:
      case PMAX:
      case PMIN:
      case P:
      case PROB:
      case RATE:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        ;
        break;
      default:
        jj_la1[6] = jj_gen;
        break label_4;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case MAX:
      case MIN:
      case PMAX:
      case PMIN:
      case P:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        prop = Property();
        label_5:
        while (true) {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case SEMICOLON:
            ;
            break;
          default:
            jj_la1[7] = jj_gen;
            break label_5;
          }
          jj_consume_token(SEMICOLON);
        }
                                                     pf.addProperty(prop);
        break;
      case LABEL:
        LabelDef(pf.getLabelList());
        break;
      case CONST:
      case PROB:
      case RATE:
        ConstantDef(pf.getConstantList());
        break;
      default:
        jj_la1[8] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
    jj_consume_token(0);
          pf.setPosition(begin, getToken(0)); {if (true) return pf;}
    throw new Error("Missing return statement in function");
  }

// Property - expression, with optional name/comment
  static final public Property Property() throws ParseException {
        String name = null;
        Expression expr;
        Property prop;
        Token begin = null;
            begin = getToken(1);
    if (jj_2_2(2147483647)) {
      jj_consume_token(DQUOTE);
      name = Identifier();
      jj_consume_token(DQUOTE);
      jj_consume_token(COLON);
    } else {
      ;
    }
    expr = ExpressionITE(true, false);
          prop = new Property(expr, name, getPrecedingCommentBlock(begin));
          prop.setPosition(begin, getToken(0)); {if (true) return prop;}
    throw new Error("Missing return statement in function");
  }

// A single expression
  static final public Expression SingleExpression() throws ParseException {
        Expression ret;
    ret = Expression(false, false);
    jj_consume_token(0);
                                                   {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

//-----------------------------------------------------------------------------------
// Modules file stuff (a few bits of which are reused for property files)
//-----------------------------------------------------------------------------------

// Keyword denoting model type
  static final public ModelType ModulesFileType() throws ParseException {
        ModelType modelType = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case DTMC:
    case PROBABILISTIC:
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case DTMC:
        jj_consume_token(DTMC);
        break;
      case PROBABILISTIC:
        jj_consume_token(PROBABILISTIC);
        break;
      default:
        jj_la1[9] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
                                     modelType=ModelType.DTMC;
      break;
    case MDP:
    case NONDETERMINISTIC:
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case MDP:
        jj_consume_token(MDP);
        break;
      case NONDETERMINISTIC:
        jj_consume_token(NONDETERMINISTIC);
        break;
      default:
        jj_la1[10] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
                                       modelType=ModelType.MDP;
      break;
    case CTMC:
    case STOCHASTIC:
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case CTMC:
        jj_consume_token(CTMC);
        break;
      case STOCHASTIC:
        jj_consume_token(STOCHASTIC);
        break;
      default:
        jj_la1[11] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
                                  modelType=ModelType.CTMC;
      break;
    case PTA:
      jj_consume_token(PTA);
                  modelType=ModelType.PTA;
      break;
    default:
      jj_la1[12] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          {if (true) return modelType;}
    throw new Error("Missing return statement in function");
  }

// Formula definition
  static final public void FormulaDef(FormulaList formulaList) throws ParseException {
        ExpressionIdent name = null;
        Expression expr = null;
    jj_consume_token(FORMULA);
    name = IdentifierExpression();
    jj_consume_token(EQ);
    expr = Expression(false, false);
    jj_consume_token(SEMICOLON);
          formulaList.addFormula(name, expr);
  }

// Label definition
  static final public void LabelDef(LabelList labelList) throws ParseException, PrismLangException {
        ExpressionIdent name = null;
        Expression expr = null;
    if (jj_2_3(2147483647)) {
      jj_consume_token(LABEL);
      jj_consume_token(DQUOTE);
      name = IdentifierExpression();
      jj_consume_token(DQUOTE);
      jj_consume_token(EQ);
      expr = Expression(false, false);
      jj_consume_token(SEMICOLON);
          labelList.addLabel(name, expr);
    } else if (jj_2_4(2147483647)) {
      jj_consume_token(LABEL);
      name = IdentifierExpression();
                                                                         {if (true) throw new PrismLangException("Label names must be enclosed in double-quotes", name);}
    } else {
      jj_consume_token(-1);
      throw new ParseException();
    }
  }

// Constant definition
  static final public void ConstantDef(ConstantList constantList) throws ParseException {
        Type type = TypeInt.getInstance();
        ExpressionIdent name = null;
        Expression expr = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case CONST:
      jj_consume_token(CONST);
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case BOOL:
      case DOUBLE:
      case INT:
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case INT:
          jj_consume_token(INT);
                             type=TypeInt.getInstance();
          break;
        case DOUBLE:
          jj_consume_token(DOUBLE);
                                                                        type=TypeDouble.getInstance();
          break;
        case BOOL:
          jj_consume_token(BOOL);
                                                                                                                    type=TypeBool.getInstance();
          break;
        default:
          jj_la1[13] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
        break;
      default:
        jj_la1[14] = jj_gen;
        ;
      }
      break;
    case PROB:
    case RATE:
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case RATE:
        jj_consume_token(RATE);
        break;
      case PROB:
        jj_consume_token(PROB);
        break;
      default:
        jj_la1[15] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
                               type=TypeDouble.getInstance();
      break;
    default:
      jj_la1[16] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    // Name and (optional) initial value
            name = IdentifierExpression();
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case EQ:
      jj_consume_token(EQ);
      expr = Expression(false, false);
      break;
    default:
      jj_la1[17] = jj_gen;
      ;
    }
    jj_consume_token(SEMICOLON);
          constantList.addConstant(name, expr, type);
  }

// Global variable declaration
  static final public Declaration GlobalDecl() throws ParseException {
        Declaration decl = null;
    jj_consume_token(GLOBAL);
    decl = Declaration();
          {if (true) return decl;}
    throw new Error("Missing return statement in function");
  }

// Variable declaration
  static final public Declaration Declaration() throws ParseException {
        Declaration decl;
        String name = null;
        DeclarationType declType;
        Expression init = null;
        Token begin = null;
            begin = getToken(1);
    name = Identifier();
    jj_consume_token(COLON);
    declType = DeclarationVarType();
                  decl = new Declaration(name, declType);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case INIT:
      jj_consume_token(INIT);
      init = Expression(false, false);
          decl.setStart(init);
      break;
    default:
      jj_la1[18] = jj_gen;
      ;
    }
    jj_consume_token(SEMICOLON);
          decl.setPosition(begin, getToken(0)); {if (true) return decl;}
    throw new Error("Missing return statement in function");
  }

// Type part of a declaration
  static final public DeclarationType DeclarationVarType() throws ParseException {
        Expression low = null, high = null;
        DeclarationType declType, subtype;
        Token begin = null;
            begin = getToken(1);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LBRACKET:
      jj_consume_token(LBRACKET);
      low = Expression(false, false);
      jj_consume_token(DOTS);
      high = Expression(false, false);
      jj_consume_token(RBRACKET);
                  declType = new DeclarationInt(low, high);
      break;
    case BOOL:
      jj_consume_token(BOOL);
                     declType = new DeclarationBool();
      break;
    case CLOCK:
      jj_consume_token(CLOCK);
                      declType = new DeclarationClock();
      break;
    default:
      jj_la1[19] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          declType.setPosition(begin, getToken(0)); {if (true) return declType;}
    throw new Error("Missing return statement in function");
  }

// Module
  static final public Module Module() throws ParseException {
        ExpressionIdent name = null;
        Declaration var = null;
        Expression invar;
        Command comm = null;
        Module module = null;
        Token begin = null;
    begin = jj_consume_token(MODULE);
    name = IdentifierExpression();
                                                         module = new Module(name.getName());
    label_6:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case REG_IDENT:
        ;
        break;
      default:
        jj_la1[20] = jj_gen;
        break label_6;
      }
      var = Declaration();
                                module.addDeclaration(var);
    }
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case INVARIANT:
      jj_consume_token(INVARIANT);
      invar = Expression(false, false);
      jj_consume_token(ENDINVARIANT);
                                                                        module.setInvariant(invar);
      break;
    default:
      jj_la1[21] = jj_gen;
      ;
    }
    label_7:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACKET:
        ;
        break;
      default:
        jj_la1[22] = jj_gen;
        break label_7;
      }
      comm = Command();
                             module.addCommand(comm);
    }
    jj_consume_token(ENDMODULE);
          module.setPosition(begin, getToken(0)); module.setNameASTElement(name); {if (true) return module;}
    throw new Error("Missing return statement in function");
  }

// Command
  static final public Command Command() throws ParseException {
        String synch = null;
        Expression guard = null;
        Updates updates = null;
        Command comm = new Command();
        Token begin = null;
    // Synchronisation action-label
            begin = jj_consume_token(LBRACKET);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case REG_IDENT:
      synch = Identifier();
                                                    comm.setSynch(synch);
      break;
    default:
      jj_la1[23] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
    // Guard/updates
            guard = Expression(false, false);
                                           comm.setGuard(guard);
    jj_consume_token(RARROW);
    updates = Updates();
                                                                                                  comm.setUpdates(updates);
    jj_consume_token(SEMICOLON);
          comm.setPosition(begin, getToken(0)); {if (true) return comm;}
    throw new Error("Missing return statement in function");
  }

// Updates
  static final public Updates Updates() throws ParseException {
        Expression prob;
        Update update;
        Updates updates = new Updates();
        Token begin = null;
          begin = getToken(1);
    if (jj_2_5(2147483647)) {
      update = Update();
                  updates.addUpdate(null, update);
    } else {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case F:
      case G:
      case MAX:
      case MIN:
      case X:
      case PMAX:
      case PMIN:
      case P:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        prob = Expression(false, false);
        jj_consume_token(COLON);
        update = Update();
                                                                              updates.addUpdate(prob, update);
        label_8:
        while (true) {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case PLUS:
            ;
            break;
          default:
            jj_la1[24] = jj_gen;
            break label_8;
          }
          jj_consume_token(PLUS);
          prob = Expression(false, false);
          jj_consume_token(COLON);
          update = Update();
                                                                                     updates.addUpdate(prob, update);
        }
        break;
      default:
        jj_la1[25] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
          updates.setPosition(begin, getToken(0)); {if (true) return updates;}
    throw new Error("Missing return statement in function");
  }

  static final public Update Update() throws ParseException {
        Update update = new Update();
        Token begin = null;
          begin = getToken(1);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LPARENTH:
      UpdateElement(update);
      label_9:
      while (true) {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case AND:
          ;
          break;
        default:
          jj_la1[26] = jj_gen;
          break label_9;
        }
        jj_consume_token(AND);
        UpdateElement(update);
      }
      break;
    case TRUE:
      jj_consume_token(TRUE);
      break;
    default:
      jj_la1[27] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          update.setPosition(begin, getToken(0)); {if (true) return update;}
    throw new Error("Missing return statement in function");
  }

  static final public void UpdateElement(Update update) throws ParseException {
        ExpressionIdent var = null;
        Expression expr = null;
    jj_consume_token(LPARENTH);
    var = IdentifierPrime();
    jj_consume_token(EQ);
    expr = Expression(false, false);
    jj_consume_token(RPARENTH);
                                                                                             update.addElement(var, expr);
  }

// Module renaming
  static final public RenamedModule RenamedModule() throws ParseException {
        ExpressionIdent name = null, base = null;
        RenamedModule rm = null;
        Token begin = null;
    begin = jj_consume_token(MODULE);
    name = IdentifierExpression();
    jj_consume_token(EQ);
    base = IdentifierExpression();
                                                                                            rm = new RenamedModule(name.getName(), base.getName());
    jj_consume_token(LBRACKET);
    Rename(rm);
    label_10:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[28] = jj_gen;
        break label_10;
      }
      jj_consume_token(COMMA);
      Rename(rm);
    }
    jj_consume_token(RBRACKET);
    jj_consume_token(ENDMODULE);
          rm.setPosition(begin, getToken(0)); rm.setNameASTElement(name); rm.setBaseModuleASTElement(base); {if (true) return rm;}
    throw new Error("Missing return statement in function");
  }

  static final public void Rename(RenamedModule rm) throws ParseException {
        ExpressionIdent id1 = null, id2 = null;
    // NB: have to explicitly include keywords for functions because they can be renamed
            id1 = IdentifierExpressionMinMax();
    jj_consume_token(EQ);
    id2 = IdentifierExpressionMinMax();
                rm.addRename(id1.getName(), id2.getName(), id1, id2);
  }

// Reward structure
  static final public RewardStruct RewardStruct() throws ParseException {
        String name = null, s = null;
        Expression guard = null, value = null;
        RewardStruct rs = new RewardStruct();
        RewardStructItem rsi;
        Token begin = null, begin2 = null;
    begin = jj_consume_token(REWARDS);
    if (jj_2_6(2147483647)) {
      jj_consume_token(DQUOTE);
      name = Identifier();
      jj_consume_token(DQUOTE);
                                                                      rs.setName(name);
    } else {
      ;
    }
    label_11:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case F:
      case G:
      case MAX:
      case MIN:
      case X:
      case PMAX:
      case PMIN:
      case P:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case LBRACKET:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        ;
        break;
      default:
        jj_la1[29] = jj_gen;
        break label_11;
      }
            begin2 = getToken(1); s = null;
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACKET:
        jj_consume_token(LBRACKET);
                                                             s = "";
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case REG_IDENT:
          s = Identifier();
          break;
        default:
          jj_la1[30] = jj_gen;
          ;
        }
        jj_consume_token(RBRACKET);
        break;
      default:
        jj_la1[31] = jj_gen;
        ;
      }
      guard = Expression(false, false);
      jj_consume_token(COLON);
      value = Expression(false, false);
      jj_consume_token(SEMICOLON);
          rsi = new RewardStructItem(s, guard, value); rsi.setPosition(begin2, getToken(0)); rs.addItem(rsi);
    }
    jj_consume_token(ENDREWARDS);
          rs.setPosition(begin, getToken(0)); {if (true) return rs;}
    throw new Error("Missing return statement in function");
  }

// Initial states ("init...endinit" construct)
  static final public Expression Init() throws ParseException {
        Expression expr = null;
    jj_consume_token(INIT);
    expr = Expression(false, false);
    jj_consume_token(ENDINIT);
                                                           {if (true) return expr;}
    throw new Error("Missing return statement in function");
  }

// System definition ("system...endsystem" construct)
  static final public SystemDefn SystemEndsystem() throws ParseException {
        SystemDefn ret;
    jj_consume_token(SYSTEM);
    ret = SystemDefn();
    jj_consume_token(ENDSYSTEM);
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// System definition component
  static final public SystemDefn SystemDefn() throws ParseException {
        SystemDefn ret;
    ret = SystemFullParallel();
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// System definition component (full parallel)
  static final public SystemDefn SystemFullParallel() throws ParseException {
        SystemDefn sys1 = null, sys2 = null;
        SystemFullParallel par = null;
        Token begin;
          begin = getToken(1);
    sys1 = SystemInterleaved();
            par = new SystemFullParallel(); par.addOperand(sys1);
    label_12:
    while (true) {
      if (jj_2_7(2147483647)) {
        ;
      } else {
        break label_12;
      }
      jj_consume_token(OR);
      jj_consume_token(OR);
      sys2 = SystemParallel();
                                                                                                                               par.addOperand(sys2);
    }
                if (par==null) {
                        {if (true) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if (true) return par;}
                }
    throw new Error("Missing return statement in function");
  }

// System definition component (interleaved parallel)
  static final public SystemDefn SystemInterleaved() throws ParseException {
        SystemDefn sys1 = null, sys2 = null;
        SystemInterleaved par = null;
        Token begin;
          begin = getToken(1);
    sys1 = SystemParallel();
            par = new SystemInterleaved(); par.addOperand(sys1);
    label_13:
    while (true) {
      if (jj_2_8(2147483647)) {
        ;
      } else {
        break label_13;
      }
      jj_consume_token(OR);
      jj_consume_token(OR);
      jj_consume_token(OR);
      sys2 = SystemFullParallel();
                                                                                                                                             par.addOperand(sys2);
    }
                if (par==null) {
                        {if (true) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if (true) return par;}
                }
    throw new Error("Missing return statement in function");
  }

// System definition component (parallel over set of actions)
  static final public SystemDefn SystemParallel() throws ParseException {
        SystemDefn sys1 = null, sys2 = null;
        SystemParallel par = null;
        String s;
        Token begin;
          begin = getToken(1);
    sys1 = SystemHideRename();
    if (jj_2_9(2147483647)) {
                                       par = new SystemParallel(); par.setOperand1(sys1);
      jj_consume_token(OR);
      jj_consume_token(LBRACKET);
      s = Identifier();
                                          par.addAction(s);
      label_14:
      while (true) {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case COMMA:
          ;
          break;
        default:
          jj_la1[32] = jj_gen;
          break label_14;
        }
        jj_consume_token(COMMA);
        s = Identifier();
                                                                                           par.addAction(s);
      }
      jj_consume_token(RBRACKET);
      jj_consume_token(OR);
      sys2 = SystemHideRename();
                                           par.setOperand2(sys2);
    } else {
      ;
    }
                if (par==null) {
                        {if (true) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if (true) return par;}
                }
    throw new Error("Missing return statement in function");
  }

// System definition component (hiding and renaming)
  static final public SystemDefn SystemHideRename() throws ParseException {
        SystemDefn sys = null;
        SystemHide hide = null;
        SystemRename rename = null;
        String s1 = null, s2 = null;
        Token begin;
          begin = getToken(1);
    sys = SystemAtomic();
    label_15:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACE:
      case DIVIDE:
        ;
        break;
      default:
        jj_la1[33] = jj_gen;
        break label_15;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case DIVIDE:
                  hide = new SystemHide(sys);
        jj_consume_token(DIVIDE);
        jj_consume_token(LBRACE);
        s1 = Identifier();
                                                        hide.addAction(s1);
        label_16:
        while (true) {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case COMMA:
            ;
            break;
          default:
            jj_la1[34] = jj_gen;
            break label_16;
          }
          jj_consume_token(COMMA);
          s1 = Identifier();
                                                                                                            hide.addAction(s1);
        }
        jj_consume_token(RBRACE);
                  sys = hide;
        break;
      case LBRACE:
                  rename = new SystemRename(sys);
        jj_consume_token(LBRACE);
        s1 = Identifier();
        jj_consume_token(RENAME);
        s2 = Identifier();
                                                                        rename.addRename(s1, s2);
        label_17:
        while (true) {
          switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
          case COMMA:
            ;
            break;
          default:
            jj_la1[35] = jj_gen;
            break label_17;
          }
          jj_consume_token(COMMA);
          s1 = Identifier();
          jj_consume_token(RENAME);
          s2 = Identifier();
                                                                         rename.addRename(s1, s2);
        }
        jj_consume_token(RBRACE);
                  sys = rename;
        break;
      default:
        jj_la1[36] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
          sys.setPosition(begin, getToken(0)); {if (true) return sys;}
    throw new Error("Missing return statement in function");
  }

// System definition component (bottom level)
  static final public SystemDefn SystemAtomic() throws ParseException {
        String name = null;
        SystemDefn sys = null;
        Token begin;
          begin = getToken(1);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case REG_IDENT:
      name = Identifier();
                                 sys = new SystemModule(name);
      break;
    case LPARENTH:
      jj_consume_token(LPARENTH);
      sys = SystemDefn();
      jj_consume_token(RPARENTH);
                                                      sys = new SystemBrackets(sys);
      break;
    default:
      jj_la1[37] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          sys.setPosition(begin, getToken(0)); {if (true) return sys;}
    throw new Error("Missing return statement in function");
  }

//-----------------------------------------------------------------------------------
// Expressions.
// This includes PRISM properties (if the "prop" parameter is true)
// and (within this) path formulas (if the "pathprop" parameter is true).
// Which allows us to use the same productions for the grammars for
// all three cases (they are very similar).
//-----------------------------------------------------------------------------------

// Expression
  static final public Expression Expression(boolean prop, boolean pathprop) throws ParseException {
        Expression ret;
    ret = ExpressionTemporalBinary(prop, pathprop);
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: temporal operators, binary (U, W, R) and unary (X, F, G)

// Note: the potential occurrence of two successive (unseparated) expressions
// (e.g. "a" and "b" in "F<=a b") is a grammar flaw because the function and
// minus operators can cause ambiguities, for example:
// "F<=a(b)+c(d)" = "F<=a" "(b)+c(d)" = "F<=a(b)+c" "(d)" ?
// "F<=-a-b-c" = "F<=-a" "-b-c" = "F<=-a-b" "-c" ?
// In many cases, these could be distinguished by type checking but
// that does not really help since this is done post-parsing.
// To prevent (very common) cases such as "F<=t (b)", "F<=t (b)&(c)", etc.
// being mis-parsed ("t(b)" would always be taken over "t"), we catch this case
// separately (see TimeBound() production below for details).
// This means that more complex time-bounds, especially those that
// start/end with an identifier should be parenthesised, e.g. "F<=(t1+t2)".

// In fact, JavaCC also warns about lookahead for this function.
// This is because (like unary minus), R can appear on the left of a unary
// operator (reward R operator) or in the middle of a binary operator (release).
  static final public Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        ExpressionTemporal exprTemp;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionTemporalUnary(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case R:
    case U:
    case W:
                  if (!pathprop) {if (true) throw generateParseException();}
                  exprTemp = new ExpressionTemporal(); exprTemp.setOperand1(ret);
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case U:
        jj_consume_token(U);
                        exprTemp.setOperator(ExpressionTemporal.P_U);
        break;
      case W:
        jj_consume_token(W);
                        exprTemp.setOperator(ExpressionTemporal.P_W);
        break;
      case R:
        jj_consume_token(R);
                        exprTemp.setOperator(ExpressionTemporal.P_R);
        break;
      default:
        jj_la1[38] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACKET:
      case EQ:
      case LT:
      case GT:
      case LE:
      case GE:
        TimeBound(exprTemp);
        break;
      default:
        jj_la1[39] = jj_gen;
        ;
      }
      expr = ExpressionTemporalUnary(prop, pathprop);
                  exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp;
      break;
    default:
      jj_la1[40] = jj_gen;
      ;
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

  static final public Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        ExpressionTemporal exprTemp;
        Token begin = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case F:
    case G:
    case X:
                  if (!pathprop) {if (true) throw generateParseException();}
                  begin = getToken(1); exprTemp = new ExpressionTemporal();
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case X:
        jj_consume_token(X);
                        exprTemp.setOperator(ExpressionTemporal.P_X);
        break;
      case F:
        jj_consume_token(F);
                        exprTemp.setOperator(ExpressionTemporal.P_F);
        break;
      case G:
        jj_consume_token(G);
                        exprTemp.setOperator(ExpressionTemporal.P_G);
        break;
      default:
        jj_la1[41] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACKET:
      case EQ:
      case LT:
      case GT:
      case LE:
      case GE:
        TimeBound(exprTemp);
        break;
      default:
        jj_la1[42] = jj_gen;
        ;
      }
      expr = ExpressionTemporalUnary(prop, pathprop);
                  exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp;
      break;
    case A:
    case E:
    case FALSE:
    case FILTER:
    case FUNC:
    case MAX:
    case MIN:
    case PMAX:
    case PMIN:
    case P:
    case RMAX:
    case RMIN:
    case R:
    case S:
    case TRUE:
    case NOT:
    case LPARENTH:
    case MINUS:
    case DQUOTE:
    case REG_INT:
    case REG_DOUBLE:
    case REG_IDENT:
      ret = ExpressionITE(prop, pathprop);
      break;
    default:
      jj_la1[43] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Time bound for temporal operators
// (see ExpressionTemporal production for lookahead explanation)
  static final public void TimeBound(ExpressionTemporal exprTemp) throws ParseException {
        Expression lBound, uBound;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LE:
      jj_consume_token(LE);
      if (jj_2_10(2147483647)) {
        uBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case A:
        case E:
        case FALSE:
        case FILTER:
        case FUNC:
        case F:
        case G:
        case MAX:
        case MIN:
        case X:
        case PMAX:
        case PMIN:
        case P:
        case RMAX:
        case RMIN:
        case R:
        case S:
        case TRUE:
        case NOT:
        case LPARENTH:
        case MINUS:
        case DQUOTE:
        case REG_INT:
        case REG_DOUBLE:
        case REG_IDENT:
          uBound = Expression(false, false);
          break;
        default:
          jj_la1[44] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
                                                                                                                                        exprTemp.setUpperBound(uBound, false);
      break;
    case LT:
      jj_consume_token(LT);
      if (jj_2_11(2147483647)) {
        uBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case A:
        case E:
        case FALSE:
        case FILTER:
        case FUNC:
        case F:
        case G:
        case MAX:
        case MIN:
        case X:
        case PMAX:
        case PMIN:
        case P:
        case RMAX:
        case RMIN:
        case R:
        case S:
        case TRUE:
        case NOT:
        case LPARENTH:
        case MINUS:
        case DQUOTE:
        case REG_INT:
        case REG_DOUBLE:
        case REG_IDENT:
          uBound = Expression(false, false);
          break;
        default:
          jj_la1[45] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
                                                                                                                                        exprTemp.setUpperBound(uBound, true);
      break;
    case GE:
      jj_consume_token(GE);
      if (jj_2_12(2147483647)) {
        lBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case A:
        case E:
        case FALSE:
        case FILTER:
        case FUNC:
        case F:
        case G:
        case MAX:
        case MIN:
        case X:
        case PMAX:
        case PMIN:
        case P:
        case RMAX:
        case RMIN:
        case R:
        case S:
        case TRUE:
        case NOT:
        case LPARENTH:
        case MINUS:
        case DQUOTE:
        case REG_INT:
        case REG_DOUBLE:
        case REG_IDENT:
          lBound = Expression(false, false);
          break;
        default:
          jj_la1[46] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
                                                                                                                                        exprTemp.setLowerBound(lBound, false);
      break;
    case GT:
      jj_consume_token(GT);
      if (jj_2_13(2147483647)) {
        lBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
        case A:
        case E:
        case FALSE:
        case FILTER:
        case FUNC:
        case F:
        case G:
        case MAX:
        case MIN:
        case X:
        case PMAX:
        case PMIN:
        case P:
        case RMAX:
        case RMIN:
        case R:
        case S:
        case TRUE:
        case NOT:
        case LPARENTH:
        case MINUS:
        case DQUOTE:
        case REG_INT:
        case REG_DOUBLE:
        case REG_IDENT:
          lBound = Expression(false, false);
          break;
        default:
          jj_la1[47] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
                                                                                                                                        exprTemp.setLowerBound(lBound, true);
      break;
    case LBRACKET:
      jj_consume_token(LBRACKET);
      lBound = Expression(false, false);
      jj_consume_token(COMMA);
      uBound = Expression(false, false);
      jj_consume_token(RBRACKET);
                                                                                                                exprTemp.setLowerBound(lBound, false); exprTemp.setUpperBound(uBound, false);
      break;
    case EQ:
      jj_consume_token(EQ);
      lBound = Expression(false, false);
                                                     exprTemp.setEqualBounds(lBound);
      break;
    default:
      jj_la1[48] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
  }

// Expression: if-then-else, i.e. "cond ? then : else"
  static final public Expression ExpressionITE(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, left, right;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionImplies(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case QMARK:
      jj_consume_token(QMARK);
      left = ExpressionImplies(prop, pathprop);
      jj_consume_token(COLON);
      right = ExpressionITE(prop, pathprop);
                  ret = new ExpressionITE(ret, left, right); ret.setPosition(begin, getToken(0));
      break;
    default:
      jj_la1[49] = jj_gen;
      ;
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: implies
  static final public Expression ExpressionImplies(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionIff(prop, pathprop);
    label_18:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case IMPLIES:
        ;
        break;
      default:
        jj_la1[50] = jj_gen;
        break label_18;
      }
      jj_consume_token(IMPLIES);
      expr = ExpressionIff(prop, pathprop);
                                                           ret = new ExpressionBinaryOp(ExpressionBinaryOp.IMPLIES, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: if-and-only-iff
  static final public Expression ExpressionIff(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionOr(prop, pathprop);
    label_19:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case IFF:
        ;
        break;
      default:
        jj_la1[51] = jj_gen;
        break label_19;
      }
      jj_consume_token(IFF);
      expr = ExpressionOr(prop, pathprop);
                                                      ret = new ExpressionBinaryOp(ExpressionBinaryOp.IFF, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: or
  static final public Expression ExpressionOr(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionAnd(prop, pathprop);
    label_20:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case OR:
        ;
        break;
      default:
        jj_la1[52] = jj_gen;
        break label_20;
      }
      jj_consume_token(OR);
      expr = ExpressionAnd(prop, pathprop);
                                                      ret = new ExpressionBinaryOp(ExpressionBinaryOp.OR, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: and
  static final public Expression ExpressionAnd(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionNot(prop, pathprop);
    label_21:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case AND:
        ;
        break;
      default:
        jj_la1[53] = jj_gen;
        break label_21;
      }
      jj_consume_token(AND);
      expr = ExpressionNot(prop, pathprop);
                                                       ret = new ExpressionBinaryOp(ExpressionBinaryOp.AND, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: not
  static final public Expression ExpressionNot(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case NOT:
      begin = jj_consume_token(NOT);
      expr = ExpressionNot(prop, pathprop);
                                                                     ret = new ExpressionUnaryOp(ExpressionUnaryOp.NOT, expr); ret.setPosition(begin, getToken(0));
      break;
    case A:
    case E:
    case FALSE:
    case FILTER:
    case FUNC:
    case MAX:
    case MIN:
    case PMAX:
    case PMIN:
    case P:
    case RMAX:
    case RMIN:
    case R:
    case S:
    case TRUE:
    case LPARENTH:
    case MINUS:
    case DQUOTE:
    case REG_INT:
    case REG_DOUBLE:
    case REG_IDENT:
      ret = ExpressionEquality(prop, pathprop);
      break;
    default:
      jj_la1[54] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: equality operators: =, !=
  static final public Expression ExpressionEquality(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        int op;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionRelop(prop, pathprop);
    label_22:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case EQ:
      case NE:
        ;
        break;
      default:
        jj_la1[55] = jj_gen;
        break label_22;
      }
      op = EqNeq();
      expr = ExpressionRelop(prop, pathprop);
                                                                ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: relational operators: >, <, >=, <=
  static final public Expression ExpressionRelop(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        int op;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionPlusMinus(prop, pathprop);
    label_23:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LT:
      case GT:
      case LE:
      case GE:
        ;
        break;
      default:
        jj_la1[56] = jj_gen;
        break label_23;
      }
      op = LtGt();
      expr = ExpressionPlusMinus(prop, pathprop);
                                                                   ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: plus/minus

// JavaCC warns about lookahead for this function. This is because in a few places
// (bounded temporal operators and semicolon-less properties files)
// (see the relevant productions for details)
// we allow two or more successive expressions resulting in potential ambiguities
// e.g. "-a-b" = "(-a)-b" = "-a" "-b"
// Ignoring the warning results in the largest match being taken.
  static final public Expression ExpressionPlusMinus(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        int op;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionTimesDivide(prop, pathprop);
    label_24:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case PLUS:
      case MINUS:
        ;
        break;
      default:
        jj_la1[57] = jj_gen;
        break label_24;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case PLUS:
        jj_consume_token(PLUS);
                           op = ExpressionBinaryOp.PLUS;
        break;
      case MINUS:
        jj_consume_token(MINUS);
                                                                       op = ExpressionBinaryOp.MINUS;
        break;
      default:
        jj_la1[58] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      expr = ExpressionTimesDivide(prop, pathprop);
                                                               ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: times/divide
  static final public Expression ExpressionTimesDivide(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        int op;
        Token begin = null;
          begin = getToken(1);
    ret = ExpressionUnaryMinus(prop, pathprop);
    label_25:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case TIMES:
      case DIVIDE:
        ;
        break;
      default:
        jj_la1[59] = jj_gen;
        break label_25;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case TIMES:
        jj_consume_token(TIMES);
                            op = ExpressionBinaryOp.TIMES;
        break;
      case DIVIDE:
        jj_consume_token(DIVIDE);
                                                                          op = ExpressionBinaryOp.DIVIDE;
        break;
      default:
        jj_la1[60] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      expr = ExpressionUnaryMinus(prop, pathprop);
                                                              ret = new ExpressionBinaryOp(op, ret, expr); ret.setPosition(begin, getToken(0));
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: unary minus
  static final public Expression ExpressionUnaryMinus(boolean prop, boolean pathprop) throws ParseException {
        Expression ret, expr;
        Token begin = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case MINUS:
      begin = jj_consume_token(MINUS);
      expr = ExpressionUnaryMinus(prop, pathprop);
                  ret = new ExpressionUnaryOp(ExpressionUnaryOp.MINUS, expr); ret.setPosition(begin, getToken(0));
      break;
    case A:
    case E:
    case FALSE:
    case FILTER:
    case FUNC:
    case MAX:
    case MIN:
    case PMAX:
    case PMIN:
    case P:
    case RMAX:
    case RMIN:
    case R:
    case S:
    case TRUE:
    case LPARENTH:
    case DQUOTE:
    case REG_INT:
    case REG_DOUBLE:
    case REG_IDENT:
      ret = ExpressionBasic(prop, pathprop);
      break;
    default:
      jj_la1[61] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Basic expression (top of operator precedence ordering)
  static final public Expression ExpressionBasic(boolean prop, boolean pathprop) throws ParseException {
        Expression ret;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case FALSE:
    case TRUE:
    case REG_INT:
    case REG_DOUBLE:
      ret = ExpressionLiteral(prop, pathprop);
      break;
    case REG_IDENT:
      ret = ExpressionFuncOrIdent(prop, pathprop);
      break;
    case MAX:
    case MIN:
      ret = ExpressionFuncMinMax(prop, pathprop);
      break;
    case FUNC:
      ret = ExpressionFuncOldStyle(prop, pathprop);
      break;
    case LPARENTH:
      ret = ExpressionParenth(prop, pathprop);
      break;
    case PMAX:
    case PMIN:
    case P:
      // Remaining options are only applicable for properties
                      ret = ExpressionProb(prop, pathprop);
      break;
    case S:
      ret = ExpressionSS(prop, pathprop);
      break;
    case RMAX:
    case RMIN:
    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;
    case FILTER:
      ret = ExpressionFilter(prop, pathprop);
      break;
    default:
      jj_la1[62] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: function or identifier

// JavaCC warns about lookahead for this function. This is because in a few places
// (bounded temporal operators and semicolon-less properties files)
// (see the relevant productions for details)
// we allow two or more successive expressions resulting in potential ambiguities
// e.g. "a(b)" = "a" "(b)"
// Ignoring the warning results in the largest match being taken.
  static final public Expression ExpressionFuncOrIdent(boolean prop, boolean pathprop) throws ParseException {
        String s = null;
        Expression ret = null;
        Token begin = null;
    // If there is no "(...)", this is an identifier
            s = Identifier();
                           ret = new ExpressionIdent(s); begin = getToken(0);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LPARENTH:
      jj_consume_token(LPARENTH);
                       ret = new ExpressionFunc(s);
      ExpressionFuncArgs(prop, pathprop, (ExpressionFunc)ret);
      jj_consume_token(RPARENTH);
      break;
    default:
      jj_la1[63] = jj_gen;
      ;
    }
          ret.setPosition(begin, getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: min/max function (treated differently because min/max are keywords)
  static final public Expression ExpressionFuncMinMax(boolean prop, boolean pathprop) throws ParseException {
        String s = null;
        ExpressionFunc func = null;
        Token begin = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case MIN:
      begin = jj_consume_token(MIN);
                          s = "min";
      break;
    case MAX:
      begin = jj_consume_token(MAX);
                                                         s = "max";
      break;
    default:
      jj_la1[64] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          func = new ExpressionFunc(s);
    jj_consume_token(LPARENTH);
    ExpressionFuncArgs(prop, pathprop, func);
    jj_consume_token(RPARENTH);
          func.setPosition(begin, getToken(0)); {if (true) return func;}
    throw new Error("Missing return statement in function");
  }

// Expression: old-style function, i.e. "func(name, ...)"
  static final public Expression ExpressionFuncOldStyle(boolean prop, boolean pathprop) throws ParseException {
        String s = null;
        ExpressionFunc func = null;
        Token begin = null;
    begin = jj_consume_token(FUNC);
    jj_consume_token(LPARENTH);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case MIN:
      jj_consume_token(MIN);
                                            s = "min";
      break;
    case MAX:
      jj_consume_token(MAX);
                                                                   s = "max";
      break;
    case REG_IDENT:
      s = Identifier();
      break;
    default:
      jj_la1[65] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(COMMA);
                  func = new ExpressionFunc(s); func.setOldStyle(true);
    ExpressionFuncArgs(prop, pathprop, func);
    jj_consume_token(RPARENTH);
          func.setPosition(begin, getToken(0)); {if (true) return func;}
    throw new Error("Missing return statement in function");
  }

// Arguments for a function in an expression
  static final public void ExpressionFuncArgs(boolean prop, boolean pathprop, ExpressionFunc func) throws ParseException {
        Expression expr;
    expr = Expression(prop, pathprop);
                                            func.addOperand(expr);
    label_26:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case COMMA:
        ;
        break;
      default:
        jj_la1[66] = jj_gen;
        break label_26;
      }
      jj_consume_token(COMMA);
      expr = Expression(prop, pathprop);
                                                                                                                   func.addOperand(expr);
    }
  }

// Expression: literal
  static final public Expression ExpressionLiteral(boolean prop, boolean pathprop) throws ParseException {
        Expression ret = null;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case REG_INT:
      jj_consume_token(REG_INT);
                try {
                        int i = Integer.parseInt(getToken(0).image);
                        ret = new ExpressionLiteral(TypeInt.getInstance(), new Integer(i));
                } catch (NumberFormatException e) {
                        // Need to catch this because some matches for regexp REG_INT
                        // are not valid integers (e.g. too big).
                        ParseException ex = new ParseException("Invalid integer literal");
                        ex.currentToken = getToken(0);
                        {if (true) throw ex;}
                        // NB: can't call generateParseException() here; it crashes
                }
      break;
    case REG_DOUBLE:
      jj_consume_token(REG_DOUBLE);
                try {
                        double d = Double.parseDouble(getToken(0).image);
                        ret = new ExpressionLiteral(TypeDouble.getInstance(), new Double(d), getToken(0).image);
                } catch (NumberFormatException e) {
                        // Need to catch this because some matches for regexp REG_DOUBLE
                        // may not be valid doubles.
                        ParseException ex = new ParseException("Invalid double literal");
                        // NB: can't call generateParseException() here; it crashes
                }
      break;
    case TRUE:
      jj_consume_token(TRUE);
                 ret = new ExpressionLiteral(TypeBool.getInstance(), new Boolean(true));
      break;
    case FALSE:
      jj_consume_token(FALSE);
                  ret = new ExpressionLiteral(TypeBool.getInstance(), new Boolean(false));
      break;
    default:
      jj_la1[67] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          ret.setPosition(getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Expression: parentheses
  static final public Expression ExpressionParenth(boolean prop, boolean pathprop) throws ParseException {
        Expression expr, ret;
        Token begin = null;
    begin = jj_consume_token(LPARENTH);
    expr = Expression(prop, pathprop);
    jj_consume_token(RPARENTH);
          ret = new ExpressionUnaryOp(ExpressionUnaryOp.PARENTH, expr); ret.setPosition(begin, getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

//-----------------------------------------------------------------------------------
// Property stuff
//-----------------------------------------------------------------------------------

// (Property) expression: probabilistic operator P
  static final public Expression ExpressionProb(boolean prop, boolean pathprop) throws ParseException {
        int r;
        String relOp = null;
        Expression prob = null;
        Expression expr;
        Filter filter = null;
        ExpressionProb ret = new ExpressionProb();
        Token begin = null;
        boolean isBool;
          if (!prop) {if (true) throw generateParseException();}
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case P:
      begin = jj_consume_token(P);
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LT:
      case GT:
      case LE:
      case GE:
        r = LtGt();
        prob = Expression(false, false);
                                                                       relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true;
        break;
      case EQ:
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                                 relOp = "="; isBool = false;
        break;
      case MIN:
        jj_consume_token(MIN);
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                                       relOp = "min="; isBool = false;
        break;
      case MAX:
        jj_consume_token(MAX);
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                                       relOp = "max="; isBool = false;
        break;
      default:
        jj_la1[68] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      break;
    case PMIN:
      begin = jj_consume_token(PMIN);
      jj_consume_token(EQ);
      jj_consume_token(QMARK);
                                         relOp = "min="; isBool = false;
      break;
    case PMAX:
      begin = jj_consume_token(PMAX);
      jj_consume_token(EQ);
      jj_consume_token(QMARK);
                                         relOp = "max="; isBool = false;
      break;
    default:
      jj_la1[69] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = Expression(prop, true);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LBRACE:
      filter = Filter();
      break;
    default:
      jj_la1[70] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
                ret.setRelOp(relOp);
                ret.setProb(prob);
                ret.setExpression(expr);
                ret.setFilter(filter);
                ret.setPosition(begin, getToken(0));
                // Filter is actually dealt with by wrapping this expression in
                // an (invisible) ExpressionFilter expression
                if (filter != null) {
                        String filterOp = isBool ? "&" : filter.getFilterOpString();
                        ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
                        ef.setInvisible(true);
                        {if (true) return ef;}
                }
                else {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Filter for a P/S/R operator
  static final public Filter Filter() throws ParseException {
        Filter filter;
        Expression expr;
        Token begin = null;
    begin = jj_consume_token(LBRACE);
    expr = Expression(true, false);
                                                          filter = new Filter(expr);
    jj_consume_token(RBRACE);
    label_27:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACE:
        ;
        break;
      default:
        jj_la1[71] = jj_gen;
        break label_27;
      }
      jj_consume_token(LBRACE);
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case MIN:
        jj_consume_token(MIN);
                          filter.setMinRequested(true);
        break;
      case MAX:
        jj_consume_token(MAX);
                          filter.setMaxRequested(true);
        break;
      default:
        jj_la1[72] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      jj_consume_token(RBRACE);
    }
          filter.setPosition(begin, getToken(0)); {if (true) return filter;}
    throw new Error("Missing return statement in function");
  }

// (Property) expression: steady-state operator S
  static final public Expression ExpressionSS(boolean prop, boolean pathprop) throws ParseException {
        int r;
        String relOp = null;
        Expression prob = null;
        Expression expr;
        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);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LT:
    case GT:
    case LE:
    case GE:
      r = LtGt();
      prob = Expression(false, false);
                                                               relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true;
      break;
    case EQ:
      jj_consume_token(EQ);
      jj_consume_token(QMARK);
                                 relOp = "="; isBool = false;
      break;
    default:
      jj_la1[73] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = Expression(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LBRACE:
      filter = Filter();
      break;
    default:
      jj_la1[74] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
                ret.setRelOp(relOp);
                ret.setProb(prob);
                ret.setExpression(expr);
                ret.setFilter(filter);
                ret.setPosition(begin, getToken(0));
                // Filter is actually dealt with by wrapping this expression in
                // an (invisible) ExpressionFilter expression
                if (filter != null) {
                        String filterOp = isBool ? "&" : filter.getFilterOpString();
                        ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
                        ef.setInvisible(true);
                        {if (true) return ef;}
                }
                else {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// (Property) expression: expected reward operator R
  static final public Expression ExpressionReward(boolean prop, boolean pathprop) throws ParseException {
        int r;
        Object index = null;
        String relOp = null;
        Expression rew = null;
        Expression expr;
        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:
      begin = jj_consume_token(R);
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LBRACE:
        index = RewardIndex();
        break;
      default:
        jj_la1[75] = jj_gen;
        ;
      }
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case LT:
      case GT:
      case LE:
      case GE:
        r = LtGt();
        rew = Expression(false, false);
                                                       relOp = ExpressionBinaryOp.opSymbols[r]; isBool = true;
        break;
      case EQ:
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                             relOp = "="; isBool = false;
        break;
      case MIN:
        jj_consume_token(MIN);
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                                   relOp = "min="; isBool = false;
        break;
      case MAX:
        jj_consume_token(MAX);
        jj_consume_token(EQ);
        jj_consume_token(QMARK);
                                   relOp = "max="; isBool = false;
        break;
      default:
        jj_la1[76] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      break;
    case RMIN:
      begin = jj_consume_token(RMIN);
      jj_consume_token(EQ);
      jj_consume_token(QMARK);
                                         relOp = "min="; isBool = false;
      break;
    case RMAX:
      begin = jj_consume_token(RMAX);
      jj_consume_token(EQ);
      jj_consume_token(QMARK);
                                         relOp = "max="; isBool = false;
      break;
    default:
      jj_la1[77] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = ExpressionRewardContents(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case LBRACE:
      filter = Filter();
      break;
    default:
      jj_la1[78] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
                ret.setRewardStructIndex(index);
                ret.setRelOp(relOp);
                ret.setReward(rew);
                ret.setExpression(expr);
                ret.setFilter(filter);
                ret.setPosition(begin, getToken(0));
                // Filter is actually dealt with by wrapping this expression in
                // an (invisible) ExpressionFilter expression
                if (filter != null) {
                        String filterOp = isBool ? "&" : filter.getFilterOpString();
                        ExpressionFilter ef = new ExpressionFilter(filterOp, ret, filter.getExpression());
                        ef.setInvisible(true);
                        {if (true) return ef;}
                }
                else {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Reward struct index for R operator
  static final public Object RewardIndex() throws ParseException {
        Object index;
    jj_consume_token(LBRACE);
    if (jj_2_14(2147483647)) {
      jj_consume_token(DQUOTE);
      index = Identifier();
      jj_consume_token(DQUOTE);
    } else {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case A:
      case E:
      case FALSE:
      case FILTER:
      case FUNC:
      case F:
      case G:
      case MAX:
      case MIN:
      case X:
      case PMAX:
      case PMIN:
      case P:
      case RMAX:
      case RMIN:
      case R:
      case S:
      case TRUE:
      case NOT:
      case LPARENTH:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:
        index = Expression(false, false);
        break;
      default:
        jj_la1[79] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
    jj_consume_token(RBRACE);
          {if (true) return index;}
    throw new Error("Missing return statement in function");
  }

// Contents of an R operator
  static final public Expression ExpressionRewardContents(boolean prop, boolean pathprop) throws ParseException {
        Expression expr = null;
        ExpressionTemporal ret = null;
        Token begin;
    if (jj_2_15(2147483647)) {
      begin = jj_consume_token(C);
      jj_consume_token(LE);
      expr = Expression(false, false);
                                                                                 ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); ret.setUpperBound(expr);
    } else {
      switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
      case C:
        begin = jj_consume_token(C);
                        ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null);
        break;
      case I:
        begin = jj_consume_token(I);
        jj_consume_token(EQ);
        expr = Expression(false, false);
                                                             ret = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); ret.setUpperBound(expr);
        break;
      case F:
        begin = jj_consume_token(F);
        expr = Expression(prop, pathprop);
                                                          ret = new ExpressionTemporal(ExpressionTemporal.R_F, null, expr);
        break;
      case S:
        begin = jj_consume_token(S);
                        ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
        break;
      default:
        jj_la1[80] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
          ret.setPosition(begin, getToken(0)); {if (true) return ret;}
    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;
        ExpressionLabel ret = null;
        Token begin;
          if (!prop) {if (true) throw generateParseException();}
    begin = jj_consume_token(DQUOTE);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case REG_IDENT:
      s = Identifier();
      break;
    case INIT:
      jj_consume_token(INIT);
                                                       s = "init";
      break;
    default:
      jj_la1[81] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(DQUOTE);
          ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// (Property) expression: filter (using "filter" keyword)
  static final public Expression ExpressionFilter(boolean prop, boolean pathprop) throws ParseException {
        ExpressionFilter expr = null;
        String op = null;
        Expression filter = null;
        Expression expr2 = null;
        Token begin = null;
          if (!prop) {if (true) throw generateParseException();}
    // filter(
            begin = jj_consume_token(FILTER);
    jj_consume_token(LPARENTH);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case MIN:
      jj_consume_token(MIN);
                  op = "min";
      break;
    case MAX:
      jj_consume_token(MAX);
                                          op = "max";
      break;
    case PLUS:
      jj_consume_token(PLUS);
                   op = "+";
      break;
    case AND:
      jj_consume_token(AND);
                                         op = "&";
      break;
    case OR:
      jj_consume_token(OR);
                                                              op = "|";
      break;
    case REG_IDENT:
      op = Identifier();
      break;
    default:
      jj_la1[82] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(COMMA);
    expr2 = Expression(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case COMMA:
      jj_consume_token(COMMA);
      filter = Expression(prop, pathprop);
      break;
    default:
      jj_la1[83] = jj_gen;
      ;
    }
    jj_consume_token(RPARENTH);
          expr = new ExpressionFilter(op, expr2, filter); expr.setPosition(begin, getToken(0)); {if (true) return expr;}
    throw new Error("Missing return statement in function");
  }

//-----------------------------------------------------------------------------------
// Miscellaneous stuff
//-----------------------------------------------------------------------------------

// Identifier (returns String)
  static final public String Identifier() throws ParseException {
    jj_consume_token(REG_IDENT);
                      {if (true) return getToken(0).image;}
    throw new Error("Missing return statement in function");
  }

// Identifier (returns ExpressionIdent, storing position info)
  static final public ExpressionIdent IdentifierExpression() throws ParseException {
        String ident;
        ExpressionIdent ret;
    ident = Identifier();
          ret = new ExpressionIdent(ident); ret.setPosition(getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Identifier or min/max keyword (returns ExpressionIdent, storing position info)
  static final public ExpressionIdent IdentifierExpressionMinMax() throws ParseException {
        String ident;
        ExpressionIdent ret;
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case REG_IDENT:
      ident = Identifier();
      break;
    case MIN:
      jj_consume_token(MIN);
                                         ident="min";
      break;
    case MAX:
      jj_consume_token(MAX);
                                                                  ident="max";
      break;
    default:
      jj_la1[84] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
          ret = new ExpressionIdent(ident); ret.setPosition(getToken(0)); {if (true) return ret;}
    throw new Error("Missing return statement in function");
  }

// Primed identifier
  static final public ExpressionIdent IdentifierPrime() throws ParseException {
    jj_consume_token(REG_IDENTPRIME);
                // Remove prime, create new ident and return
                String s = getToken(0).image;
                s = s.substring(0, s.length()-1);
                ExpressionIdent expr = new ExpressionIdent(s);
                expr.setPosition(token);
                expr.setEndColumn(expr.getEndColumn() - 1);
                {if (true) return expr;}
    throw new Error("Missing return statement in function");
  }

// Equality operators: =, !=
  static final public int EqNeq() throws ParseException {
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case EQ:
      jj_consume_token(EQ);
              {if (true) return ExpressionBinaryOp.EQ;}
      break;
    case NE:
      jj_consume_token(NE);
              {if (true) return ExpressionBinaryOp.NE;}
      break;
    default:
      jj_la1[85] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    throw new Error("Missing return statement in function");
  }

// Relational operators: >, <, >=, <=
  static final public int LtGt() throws ParseException {
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case GT:
      jj_consume_token(GT);
              {if (true) return ExpressionBinaryOp.GT;}
      break;
    case LT:
      jj_consume_token(LT);
              {if (true) return ExpressionBinaryOp.LT;}
      break;
    case GE:
      jj_consume_token(GE);
               {if (true) return ExpressionBinaryOp.GE;}
      break;
    case LE:
      jj_consume_token(LE);
              {if (true) return ExpressionBinaryOp.LE;}
      break;
    default:
      jj_la1[86] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    throw new Error("Missing return statement in function");
  }

// For loop
  static final public ForLoop ForLoop() throws ParseException {
        String s;
        Expression from = null, to = null, step = null;
        ForLoop fl = new ForLoop();
        Token begin;
            begin = getToken(1);
    s = Identifier();
    jj_consume_token(EQ);
    from = Expression(false, false);
    jj_consume_token(COLON);
    to = Expression(false, false);
    switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
    case COLON:
      jj_consume_token(COLON);
      step = Expression(false, false);
      break;
    default:
      jj_la1[87] = jj_gen;
      ;
    }
    jj_consume_token(0);
                fl.setLHS(s);
                fl.setFrom(from);
                fl.setTo(to);
                if (step != null) fl.setStep(step);
                fl.setPosition(begin, getToken(0));
                {if (true) return fl;}
    throw new Error("Missing return statement in function");
  }

  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 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 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 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 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 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 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 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 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 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 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 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 private boolean jj_2_13(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_13(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(12, xla); }
  }

  static private boolean jj_2_14(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_14(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(13, xla); }
  }

  static private boolean jj_2_15(int xla) {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_15(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(14, xla); }
  }

  static private boolean jj_3R_51() {
    if (jj_3R_59()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_60()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_52() {
    if (jj_scan_token(QMARK)) return true;
    if (jj_3R_51()) return true;
    if (jj_scan_token(COLON)) return true;
    if (jj_3R_49()) return true;
    return false;
  }

  static private boolean jj_3_13() {
    if (jj_3R_30()) return true;
    if (jj_scan_token(LPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_119() {
    if (jj_scan_token(S)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_140()) {
    jj_scanpos = xsp;
    if (jj_3R_141()) return true;
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_35()) return true;
    xsp = jj_scanpos;
    if (jj_3R_142()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3_12() {
    if (jj_3R_30()) return true;
    if (jj_scan_token(LPARENTH)) return true;
    return false;
  }

  static private boolean jj_3_11() {
    if (jj_3R_30()) return true;
    if (jj_scan_token(LPARENTH)) return true;
    return false;
  }

  static private boolean jj_3_10() {
    if (jj_3R_30()) return true;
    if (jj_scan_token(LPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_49() {
    if (jj_3R_51()) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_52()) jj_scanpos = xsp;
    return false;
  }

  static private boolean jj_3R_139() {
    if (jj_3R_162()) return true;
    return false;
  }

  static private boolean jj_3R_176() {
    if (jj_scan_token(MAX)) return true;
    return false;
  }

  static private boolean jj_3R_67() {
    if (jj_3R_30()) return true;
    return false;
  }

  static private boolean jj_3R_175() {
    if (jj_scan_token(MIN)) return true;
    return false;
  }

  static private boolean jj_3R_65() {
    if (jj_3R_30()) return true;
    return false;
  }

  static private boolean jj_3R_63() {
    if (jj_3R_30()) return true;
    return false;
  }

  static private boolean jj_3R_61() {
    if (jj_3R_30()) return true;
    return false;
  }

  static private boolean jj_3R_58() {
    if (jj_scan_token(EQ)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_57() {
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_56() {
    if (jj_scan_token(GT)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_67()) {
    jj_scanpos = xsp;
    if (jj_3R_68()) return true;
    }
    return false;
  }

  static private boolean jj_3R_173() {
    if (jj_scan_token(LBRACE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_175()) {
    jj_scanpos = xsp;
    if (jj_3R_176()) return true;
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

  static private boolean jj_3R_55() {
    if (jj_scan_token(GE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_65()) {
    jj_scanpos = xsp;
    if (jj_3R_66()) return true;
    }
    return false;
  }

  static private boolean jj_3R_54() {
    if (jj_scan_token(LT)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_63()) {
    jj_scanpos = xsp;
    if (jj_3R_64()) return true;
    }
    return false;
  }

  static private boolean jj_3R_53() {
    if (jj_scan_token(LE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_61()) {
    jj_scanpos = xsp;
    if (jj_3R_62()) return true;
    }
    return false;
  }

  static private boolean jj_3R_162() {
    if (jj_scan_token(LBRACE)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RBRACE)) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_173()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_50() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_53()) {
    jj_scanpos = xsp;
    if (jj_3R_54()) {
    jj_scanpos = xsp;
    if (jj_3R_55()) {
    jj_scanpos = xsp;
    if (jj_3R_56()) {
    jj_scanpos = xsp;
    if (jj_3R_57()) {
    jj_scanpos = xsp;
    if (jj_3R_58()) return true;
    }
    }
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_40() {
    if (jj_3R_49()) return true;
    return false;
  }

  static private boolean jj_3R_48() {
    if (jj_3R_50()) return true;
    return false;
  }

  static private boolean jj_3R_47() {
    if (jj_scan_token(G)) return true;
    return false;
  }

  static private boolean jj_3R_46() {
    if (jj_scan_token(F)) return true;
    return false;
  }

  static private boolean jj_3R_45() {
    if (jj_scan_token(X)) return true;
    return false;
  }

  static private boolean jj_3R_39() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_45()) {
    jj_scanpos = xsp;
    if (jj_3R_46()) {
    jj_scanpos = xsp;
    if (jj_3R_47()) return true;
    }
    }
    xsp = jj_scanpos;
    if (jj_3R_48()) jj_scanpos = xsp;
    if (jj_3R_37()) return true;
    return false;
  }

  static private boolean jj_3R_158() {
    if (jj_3R_85()) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_161() {
    if (jj_scan_token(MAX)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_37() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_39()) {
    jj_scanpos = xsp;
    if (jj_3R_40()) return true;
    }
    return false;
  }

  static private boolean jj_3R_160() {
    if (jj_scan_token(MIN)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_159() {
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_44() {
    if (jj_3R_50()) return true;
    return false;
  }

  static private boolean jj_3R_138() {
    if (jj_scan_token(PMAX)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_43() {
    if (jj_scan_token(R)) return true;
    return false;
  }

  static private boolean jj_3R_137() {
    if (jj_scan_token(PMIN)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_42() {
    if (jj_scan_token(W)) return true;
    return false;
  }

  static private boolean jj_3R_41() {
    if (jj_scan_token(U)) return true;
    return false;
  }

  static private boolean jj_3R_136() {
    if (jj_scan_token(P)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_158()) {
    jj_scanpos = xsp;
    if (jj_3R_159()) {
    jj_scanpos = xsp;
    if (jj_3R_160()) {
    jj_scanpos = xsp;
    if (jj_3R_161()) return true;
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_38() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_41()) {
    jj_scanpos = xsp;
    if (jj_3R_42()) {
    jj_scanpos = xsp;
    if (jj_3R_43()) return true;
    }
    }
    xsp = jj_scanpos;
    if (jj_3R_44()) jj_scanpos = xsp;
    if (jj_3R_37()) return true;
    return false;
  }

  static private boolean jj_3R_118() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_136()) {
    jj_scanpos = xsp;
    if (jj_3R_137()) {
    jj_scanpos = xsp;
    if (jj_3R_138()) return true;
    }
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_35()) return true;
    xsp = jj_scanpos;
    if (jj_3R_139()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_36() {
    if (jj_3R_37()) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_38()) jj_scanpos = xsp;
    return false;
  }

  static private boolean jj_3R_157() {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_135() {
    if (jj_3R_28()) return true;
    return false;
  }

  static private boolean jj_3R_117() {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3_4() {
    if (jj_scan_token(LABEL)) return true;
    return false;
  }

  static private boolean jj_3_3() {
    if (jj_scan_token(LABEL)) return true;
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

  static private boolean jj_3R_134() {
    if (jj_scan_token(MAX)) return true;
    return false;
  }

  static private boolean jj_3R_128() {
    if (jj_scan_token(FALSE)) return true;
    return false;
  }

  static private boolean jj_3R_127() {
    if (jj_scan_token(TRUE)) return true;
    return false;
  }

  static private boolean jj_3R_35() {
    if (jj_3R_36()) return true;
    return false;
  }

  static private boolean jj_3R_126() {
    if (jj_scan_token(REG_DOUBLE)) return true;
    return false;
  }

  static private boolean jj_3R_133() {
    if (jj_scan_token(MIN)) return true;
    return false;
  }

  static private boolean jj_3R_125() {
    if (jj_scan_token(REG_INT)) return true;
    return false;
  }

  static private boolean jj_3R_113() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_125()) {
    jj_scanpos = xsp;
    if (jj_3R_126()) {
    jj_scanpos = xsp;
    if (jj_3R_127()) {
    jj_scanpos = xsp;
    if (jj_3R_128()) return true;
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_95() {
    if (jj_scan_token(LE)) return true;
    return false;
  }

  static private boolean jj_3R_94() {
    if (jj_scan_token(GE)) return true;
    return false;
  }

  static private boolean jj_3R_93() {
    if (jj_scan_token(LT)) return true;
    return false;
  }

  static private boolean jj_3R_131() {
    if (jj_scan_token(MAX)) return true;
    return false;
  }

  static private boolean jj_3R_85() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_92()) {
    jj_scanpos = xsp;
    if (jj_3R_93()) {
    jj_scanpos = xsp;
    if (jj_3R_94()) {
    jj_scanpos = xsp;
    if (jj_3R_95()) return true;
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_92() {
    if (jj_scan_token(GT)) return true;
    return false;
  }

  static private boolean jj_3_8() {
    if (jj_scan_token(OR)) return true;
    if (jj_scan_token(OR)) return true;
    if (jj_scan_token(OR)) return true;
    return false;
  }

  static private boolean jj_3R_132() {
    if (jj_3R_35()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_157()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_87() {
    if (jj_scan_token(NE)) return true;
    return false;
  }

  static private boolean jj_3R_82() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_86()) {
    jj_scanpos = xsp;
    if (jj_3R_87()) return true;
    }
    return false;
  }

  static private boolean jj_3R_86() {
    if (jj_scan_token(EQ)) return true;
    return false;
  }

  static private boolean jj_3R_116() {
    if (jj_scan_token(FUNC)) return true;
    if (jj_scan_token(LPARENTH)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_133()) {
    jj_scanpos = xsp;
    if (jj_3R_134()) {
    jj_scanpos = xsp;
    if (jj_3R_135()) return true;
    }
    }
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_132()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3_2() {
    if (jj_scan_token(DQUOTE)) return true;
    if (jj_3R_28()) return true;
    if (jj_scan_token(DQUOTE)) return true;
    if (jj_scan_token(COLON)) return true;
    return false;
  }

  static private boolean jj_3_7() {
    if (jj_scan_token(OR)) return true;
    if (jj_scan_token(OR)) return true;
    return false;
  }

  static private boolean jj_3R_34() {
    if (jj_scan_token(REG_IDENTPRIME)) return true;
    return false;
  }

  static private boolean jj_3R_130() {
    if (jj_scan_token(MIN)) return true;
    return false;
  }

  static private boolean jj_3R_115() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_130()) {
    jj_scanpos = xsp;
    if (jj_3R_131()) return true;
    }
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_132()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_154() {
    if (jj_scan_token(OR)) return true;
    return false;
  }

  static private boolean jj_3_9() {
    if (jj_scan_token(OR)) return true;
    if (jj_scan_token(LBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_129() {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_132()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_114() {
    if (jj_3R_28()) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_129()) jj_scanpos = xsp;
    return false;
  }

  static private boolean jj_3R_30() {
    if (jj_3R_28()) return true;
    return false;
  }

  static private boolean jj_3R_151() {
    if (jj_scan_token(MAX)) return true;
    return false;
  }

  static private boolean jj_3R_153() {
    if (jj_scan_token(AND)) return true;
    return false;
  }

  static private boolean jj_3R_28() {
    if (jj_scan_token(REG_IDENT)) return true;
    return false;
  }

  static private boolean jj_3R_112() {
    if (jj_3R_124()) return true;
    return false;
  }

  static private boolean jj_3R_111() {
    if (jj_3R_123()) return true;
    return false;
  }

  static private boolean jj_3R_110() {
    if (jj_3R_122()) return true;
    return false;
  }

  static private boolean jj_3R_149() {
    if (jj_scan_token(INIT)) return true;
    return false;
  }

  static private boolean jj_3R_109() {
    if (jj_3R_121()) return true;
    return false;
  }

  static private boolean jj_3R_99() {
    if (jj_scan_token(DIVIDE)) return true;
    return false;
  }

  static private boolean jj_3R_108() {
    if (jj_3R_120()) return true;
    return false;
  }

  static private boolean jj_3R_107() {
    if (jj_3R_119()) return true;
    return false;
  }

  static private boolean jj_3R_106() {
    if (jj_3R_118()) return true;
    return false;
  }

  static private boolean jj_3R_156() {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_105() {
    if (jj_3R_117()) return true;
    return false;
  }

  static private boolean jj_3R_104() {
    if (jj_3R_116()) return true;
    return false;
  }

  static private boolean jj_3R_155() {
    if (jj_3R_28()) return true;
    return false;
  }

  static private boolean jj_3R_152() {
    if (jj_scan_token(PLUS)) return true;
    return false;
  }

  static private boolean jj_3R_103() {
    if (jj_3R_115()) return true;
    return false;
  }

  static private boolean jj_3R_150() {
    if (jj_scan_token(MIN)) return true;
    return false;
  }

  static private boolean jj_3R_102() {
    if (jj_3R_114()) return true;
    return false;
  }

  static private boolean jj_3R_148() {
    if (jj_3R_28()) return true;
    return false;
  }

  static private boolean jj_3R_101() {
    if (jj_3R_113()) return true;
    return false;
  }

  static private boolean jj_3R_91() {
    if (jj_scan_token(MINUS)) return true;
    return false;
  }

  static private boolean jj_3R_124() {
    if (jj_scan_token(FILTER)) return true;
    if (jj_scan_token(LPARENTH)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_150()) {
    jj_scanpos = xsp;
    if (jj_3R_151()) {
    jj_scanpos = xsp;
    if (jj_3R_152()) {
    jj_scanpos = xsp;
    if (jj_3R_153()) {
    jj_scanpos = xsp;
    if (jj_3R_154()) {
    jj_scanpos = xsp;
    if (jj_3R_155()) return true;
    }
    }
    }
    }
    }
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_35()) return true;
    xsp = jj_scanpos;
    if (jj_3R_156()) jj_scanpos = xsp;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_100() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_101()) {
    jj_scanpos = xsp;
    if (jj_3R_102()) {
    jj_scanpos = xsp;
    if (jj_3R_103()) {
    jj_scanpos = xsp;
    if (jj_3R_104()) {
    jj_scanpos = xsp;
    if (jj_3R_105()) {
    jj_scanpos = xsp;
    if (jj_3R_106()) {
    jj_scanpos = xsp;
    if (jj_3R_107()) {
    jj_scanpos = xsp;
    if (jj_3R_108()) {
    jj_scanpos = xsp;
    if (jj_3R_109()) {
    jj_scanpos = xsp;
    if (jj_3R_110()) {
    jj_scanpos = xsp;
    if (jj_3R_111()) {
    jj_scanpos = xsp;
    if (jj_3R_112()) return true;
    }
    }
    }
    }
    }
    }
    }
    }
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_178() {
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_97() {
    if (jj_3R_100()) return true;
    return false;
  }

  static private boolean jj_3R_96() {
    if (jj_scan_token(MINUS)) return true;
    if (jj_3R_88()) return true;
    return false;
  }

  static private boolean jj_3R_123() {
    if (jj_scan_token(DQUOTE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_148()) {
    jj_scanpos = xsp;
    if (jj_3R_149()) return true;
    }
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

  static private boolean jj_3R_88() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_96()) {
    jj_scanpos = xsp;
    if (jj_3R_97()) return true;
    }
    return false;
  }

  static private boolean jj_3_1() {
    if (jj_scan_token(MODULE)) return true;
    if (jj_3R_28()) return true;
    if (jj_scan_token(EQ)) return true;
    return false;
  }

  static private boolean jj_3R_98() {
    if (jj_scan_token(TIMES)) return true;
    return false;
  }

  static private boolean jj_3R_89() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_98()) {
    jj_scanpos = xsp;
    if (jj_3R_99()) return true;
    }
    if (jj_3R_88()) return true;
    return false;
  }

  static private boolean jj_3R_122() {
    if (jj_scan_token(A)) return true;
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_83() {
    if (jj_3R_88()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_89()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_90() {
    if (jj_scan_token(PLUS)) return true;
    return false;
  }

  static private boolean jj_3R_84() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_90()) {
    jj_scanpos = xsp;
    if (jj_3R_91()) return true;
    }
    if (jj_3R_83()) return true;
    return false;
  }

  static private boolean jj_3_6() {
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

  static private boolean jj_3R_80() {
    if (jj_3R_83()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_84()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_147() {
    if (jj_3R_162()) return true;
    return false;
  }

  static private boolean jj_3R_121() {
    if (jj_scan_token(E)) return true;
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3_15() {
    if (jj_scan_token(C)) return true;
    if (jj_scan_token(LE)) return true;
    return false;
  }

  static private boolean jj_3_14() {
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

  static private boolean jj_3R_172() {
    if (jj_scan_token(S)) return true;
    return false;
  }

  static private boolean jj_3R_171() {
    if (jj_scan_token(F)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_170() {
    if (jj_scan_token(I)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_169() {
    if (jj_scan_token(C)) return true;
    return false;
  }

  static private boolean jj_3R_168() {
    if (jj_scan_token(C)) return true;
    if (jj_scan_token(LE)) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_81() {
    if (jj_3R_85()) return true;
    if (jj_3R_80()) return true;
    return false;
  }

  static private boolean jj_3R_177() {
    if (jj_scan_token(DQUOTE)) return true;
    if (jj_3R_28()) return true;
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

  static private boolean jj_3R_146() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_168()) {
    jj_scanpos = xsp;
    if (jj_3R_169()) {
    jj_scanpos = xsp;
    if (jj_3R_170()) {
    jj_scanpos = xsp;
    if (jj_3R_171()) {
    jj_scanpos = xsp;
    if (jj_3R_172()) return true;
    }
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_78() {
    if (jj_3R_80()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_81()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_174() {
    if (jj_scan_token(LBRACE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_177()) {
    jj_scanpos = xsp;
    if (jj_3R_178()) return true;
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

  static private boolean jj_3R_79() {
    if (jj_3R_82()) return true;
    if (jj_3R_78()) return true;
    return false;
  }

  static private boolean jj_3R_77() {
    if (jj_3R_78()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_79()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_33() {
    if (jj_scan_token(AND)) return true;
    if (jj_3R_32()) return true;
    return false;
  }

  static private boolean jj_3R_76() {
    if (jj_3R_77()) return true;
    return false;
  }

  static private boolean jj_3R_75() {
    if (jj_scan_token(NOT)) return true;
    if (jj_3R_73()) return true;
    return false;
  }

  static private boolean jj_3R_68() {
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_66() {
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_64() {
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_62() {
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_32() {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_34()) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_3R_35()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_73() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_75()) {
    jj_scanpos = xsp;
    if (jj_3R_76()) return true;
    }
    return false;
  }

  static private boolean jj_3R_163() {
    if (jj_3R_174()) return true;
    return false;
  }

  static private boolean jj_3R_142() {
    if (jj_3R_162()) return true;
    return false;
  }

  static private boolean jj_3R_167() {
    if (jj_scan_token(MAX)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_145() {
    if (jj_scan_token(RMAX)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_166() {
    if (jj_scan_token(MIN)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_74() {
    if (jj_scan_token(AND)) return true;
    if (jj_3R_73()) return true;
    return false;
  }

  static private boolean jj_3R_144() {
    if (jj_scan_token(RMIN)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_165() {
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_31() {
    if (jj_3R_32()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_33()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3_5() {
    if (jj_3R_29()) return true;
    return false;
  }

  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_29() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_31()) {
    jj_scanpos = xsp;
    if (jj_scan_token(49)) return true;
    }
    return false;
  }

  static private boolean jj_3R_164() {
    if (jj_3R_85()) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_3R_143() {
    if (jj_scan_token(R)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_163()) jj_scanpos = xsp;
    xsp = jj_scanpos;
    if (jj_3R_164()) {
    jj_scanpos = xsp;
    if (jj_3R_165()) {
    jj_scanpos = xsp;
    if (jj_3R_166()) {
    jj_scanpos = xsp;
    if (jj_3R_167()) return true;
    }
    }
    }
    return false;
  }

  static private boolean jj_3R_120() {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_143()) {
    jj_scanpos = xsp;
    if (jj_3R_144()) {
    jj_scanpos = xsp;
    if (jj_3R_145()) return true;
    }
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_146()) return true;
    xsp = jj_scanpos;
    if (jj_3R_147()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_72() {
    if (jj_scan_token(OR)) return true;
    if (jj_3R_71()) return true;
    return false;
  }

  static private boolean jj_3R_69() {
    if (jj_3R_71()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_72()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_70() {
    if (jj_scan_token(IFF)) return true;
    if (jj_3R_69()) return true;
    return false;
  }

  static private boolean jj_3R_59() {
    if (jj_3R_69()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_70()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_60() {
    if (jj_scan_token(IMPLIES)) return true;
    if (jj_3R_59()) return true;
    return false;
  }

  static private boolean jj_3R_141() {
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_140() {
    if (jj_3R_85()) return true;
    if (jj_3R_35()) return true;
    return false;
  }

  static private boolean jj_initialized_once = false;
  /** Generated Token Manager. */
  static public PrismParserTokenManager token_source;
  static SimpleCharStream jj_input_stream;
  /** 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 private int jj_gen;
  static final private int[] jj_la1 = new int[88];
  static private int[] jj_la1_0;
  static private int[] jj_la1_1;
  static private int[] jj_la1_2;
  static {
      jj_la1_init_0();
      jj_la1_init_1();
      jj_la1_init_2();
   }
   private static void jj_la1_init_0() {
      jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,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,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0x4200100,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
   }
   private static void jj_la1_init_1() {
      jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x0,0x38,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x3800,0x0,0x4012783a,0x4000,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
   }
   private static void jj_la1_init_2() {
      jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e0800,0x0,0x2e0800,0x2e0800,0x0,0x2e0800,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x10,0x0,0x1,0x200000,0x0,0x1,0x200000,0x400,0x2e0800,0x0,0x0,0x0,0x2e0801,0x200000,0x1,0x0,0x2004,0x0,0x0,0x2004,0x200000,0x0,0x3d1,0x0,0x0,0x3d1,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x2e0800,0x3d1,0x10000,0x0,0x0,0x0,0x0,0x2e0800,0x30,0x3c0,0xc00,0xc00,0x3000,0x3000,0x2e0800,0x2e0000,0x0,0x0,0x200000,0x0,0xc0000,0x3d0,0x0,0x4,0x4,0x0,0x3d0,0x4,0x4,0x3d0,0x0,0x4,0x2e0800,0x0,0x200000,0x200400,0x0,0x200000,0x30,0x3c0,0x0,};
   }
  static final private JJCalls[] jj_2_rtns = new JJCalls[15];
  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.  ");
      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();
    }
    jj_initialized_once = true;
    try { jj_input_stream = new SimpleCharStream(stream, encoding, 1, 1); } catch(java.io.UnsupportedEncodingException e) { throw new RuntimeException(e); }
    token_source = new PrismParserTokenManager(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < 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);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < 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. ");
      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();
    }
    jj_initialized_once = true;
    jj_input_stream = new SimpleCharStream(stream, 1, 1);
    token_source = new PrismParserTokenManager(jj_input_stream);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < 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);
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < 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. ");
      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();
    }
    jj_initialized_once = true;
    token_source = tm;
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  /** Reinitialise. */
  public void ReInit(PrismParserTokenManager tm) {
    token_source = tm;
    token = new Token();
    jj_ntk = -1;
    jj_gen = 0;
    for (int i = 0; i < 88; i++) jj_la1[i] = -1;
    for (int i = 0; i < jj_2_rtns.length; i++) jj_2_rtns[i] = new JJCalls();
  }

  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();
    jj_ntk = -1;
    if (token.kind == kind) {
      jj_gen++;
      if (++jj_gc > 100) {
        jj_gc = 0;
        for (int i = 0; i < jj_2_rtns.length; i++) {
          JJCalls c = jj_2_rtns[i];
          while (c != null) {
            if (c.gen < jj_gen) c.first = null;
            c = c.next;
          }
        }
      }
      return token;
    }
    token = oldToken;
    jj_kind = kind;
    throw generateParseException();
  }

  static private final class LookaheadSuccess extends java.lang.Error { }
  static final private LookaheadSuccess jj_ls = new LookaheadSuccess();
  static private boolean jj_scan_token(int kind) {
    if (jj_scanpos == jj_lastpos) {
      jj_la--;
      if (jj_scanpos.next == null) {
        jj_lastpos = jj_scanpos = jj_scanpos.next = token_source.getNextToken();
      } else {
        jj_lastpos = jj_scanpos = jj_scanpos.next;
      }
    } else {
      jj_scanpos = jj_scanpos.next;
    }
    if (jj_rescan) {
      int i = 0; Token tok = token;
      while (tok != null && tok != jj_scanpos) { i++; tok = tok.next; }
      if (tok != null) jj_add_error_token(kind, i);
    }
    if (jj_scanpos.kind != kind) return true;
    if (jj_la == 0 && jj_scanpos == jj_lastpos) throw jj_ls;
    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();
    jj_ntk = -1;
    jj_gen++;
    return token;
  }

/** Get the specific Token. */
  static final public Token getToken(int index) {
    Token t = token;
    for (int i = 0; i < index; i++) {
      if (t.next != null) t = t.next;
      else t = t.next = token_source.getNextToken();
    }
    return t;
  }

  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.List<int[]> jj_expentries = new java.util.ArrayList<int[]>();
  static private int[] jj_expentry;
  static private int jj_kind = -1;
  static private int[] jj_lasttokens = new int[100];
  static private int jj_endpos;

  static private void jj_add_error_token(int kind, int pos) {
    if (pos >= 100) return;
    if (pos == jj_endpos + 1) {
      jj_lasttokens[jj_endpos++] = kind;
    } else if (jj_endpos != 0) {
      jj_expentry = new int[jj_endpos];
      for (int i = 0; i < jj_endpos; i++) {
        jj_expentry[i] = jj_lasttokens[i];
      }
      jj_entries_loop: for (java.util.Iterator<?> it = jj_expentries.iterator(); it.hasNext();) {
        int[] oldentry = (int[])(it.next());
        if (oldentry.length == jj_expentry.length) {
          for (int i = 0; i < jj_expentry.length; i++) {
            if (oldentry[i] != jj_expentry[i]) {
              continue jj_entries_loop;
            }
          }
          jj_expentries.add(jj_expentry);
          break jj_entries_loop;
        }
      }
      if (pos != 0) jj_lasttokens[(jj_endpos = pos) - 1] = kind;
    }
  }

  /** Generate ParseException. */
  static public ParseException generateParseException() {
    jj_expentries.clear();
    boolean[] la1tokens = new boolean[88];
    if (jj_kind >= 0) {
      la1tokens[jj_kind] = true;
      jj_kind = -1;
    }
    for (int i = 0; i < 88; i++) {
      if (jj_la1[i] == jj_gen) {
        for (int j = 0; j < 32; j++) {
          if ((jj_la1_0[i] & (1<<j)) != 0) {
            la1tokens[j] = true;
          }
          if ((jj_la1_1[i] & (1<<j)) != 0) {
            la1tokens[32+j] = true;
          }
          if ((jj_la1_2[i] & (1<<j)) != 0) {
            la1tokens[64+j] = true;
          }
        }
      }
    }
    for (int i = 0; i < 88; i++) {
      if (la1tokens[i]) {
        jj_expentry = new int[1];
        jj_expentry[0] = i;
        jj_expentries.add(jj_expentry);
      }
    }
    jj_endpos = 0;
    jj_rescan_token();
    jj_add_error_token(0, 0);
    int[][] exptokseq = new int[jj_expentries.size()][];
    for (int i = 0; i < jj_expentries.size(); 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 private void jj_rescan_token() {
    jj_rescan = true;
    for (int i = 0; i < 15; i++) {
    try {
      JJCalls p = jj_2_rtns[i];
      do {
        if (p.gen > jj_gen) {
          jj_la = p.arg; jj_lastpos = jj_scanpos = p.first;
          switch (i) {
            case 0: jj_3_1(); break;
            case 1: jj_3_2(); break;
            case 2: jj_3_3(); break;
            case 3: jj_3_4(); break;
            case 4: jj_3_5(); break;
            case 5: jj_3_6(); break;
            case 6: jj_3_7(); break;
            case 7: jj_3_8(); break;
            case 8: jj_3_9(); break;
            case 9: jj_3_10(); break;
            case 10: jj_3_11(); break;
            case 11: jj_3_12(); break;
            case 12: jj_3_13(); break;
            case 13: jj_3_14(); break;
            case 14: jj_3_15(); break;
          }
        }
        p = p.next;
      } while (p != null);
      } catch(LookaheadSuccess ls) { }
    }
    jj_rescan = false;
  }

  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; }
      p = p.next;
    }
    p.gen = jj_gen + xla - jj_la; p.first = token; p.arg = xla;
  }

  static final class JJCalls {
    int gen;
    Token first;
    int arg;
    JJCalls next;
  }

}