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

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

import jltl2ba.SimpleLTL;
import parser.BooleanUtils;
import parser.ast.*;
import parser.type.*;
import prism.ModelInfo;
import parser.visitor.*;
import prism.ModelType;
import prism.PrismLangException;

@SuppressWarnings({"unused", "static-access", "serial"})
public class PrismParser implements PrismParserConstants {
        // The model associated with the properties file being parsed
        private static ModelInfo modelInfo;

        // List of keyword strings
        private static ArrayList<String> keywordList = new ArrayList<String>();
        static {
                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.out.println("                  -ltl or -l");
                                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 if (args[0].equals("-ltl") || args[0].equals("-l")) {
                                Expression expr = p.parseSingleLTLFormula(str);
                                expr = (Expression) expr.accept(new ASTTraverseModify() {
                                        public Object visit(ExpressionIdent e) throws PrismLangException
                                        {
                                                return new parser.ast.ExpressionVar(e.getName(), TypeBool.getInstance());
                                        }
                                });
                                System.out.println("LTL formula: " + expr.toString());
                                System.out.print("Tree:\u005cn=====\u005cn" + expr.toTreeString());
                                expr.typeCheck();
                                //expr.semanticCheck();
                                System.out.println("Type: " + expr.getType().getTypeString());
                                boolean pnf = Expression.isPositiveNormalFormLTL(expr);
                                System.out.println("Positive normal form: " + pnf);
                                System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(expr));
                                if (!pnf) {
                                        Expression exprPnf = BooleanUtils.convertLTLToPositiveNormalForm(expr.deepCopy());
                                        System.out.println("Positive normal form conversion: " + exprPnf);
                                        System.out.println("Syntactically co-safe: " + Expression.isCoSafeLTLSyntactic(exprPnf));
                                }
                                Expression expr2 = (Expression) expr.deepCopy().accept(new ASTTraverseModify() {
                                        public Object visit(ExpressionVar e) throws PrismLangException
                                        {
                                                        return new parser.ast.ExpressionLabel(e.getName());
                                        }
                                });
                                SimpleLTL sltl = expr2.convertForJltl2ba();
                                System.out.println("LBT: " + sltl.toStringLBT());
                                System.out.println("Spot: " + sltl.toStringSpot());
                                System.out.println("Spin: " + sltl.toStringSpin());
                        } 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(ModelInfo modelInfo, InputStream str) throws PrismLangException
        { return parsePropertiesFile(modelInfo, str, false); }

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

                // (Re)start parser
                ReInit(str);
                this.modelInfo = modelInfo;
                // 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 single LTL formula

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

                // (Re)start parser
                ReInit(str);
                // Parse
                try {
                        expr = SingleLTLFormula();
                }
                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();
        }

        /**
	 * 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;
        parser.ast.Module m = null;
        RenamedModule rm = null;
        RewardStruct rs = null;
        Expression init = null;
        int initCount = 0;
        Expression initDupe = null;
        ModulesFile mf = new ModulesFile();
        Token begin = null;
    label_1:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk_f():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_f():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_f():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:{
            SystemEndsystem(mf);
            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);}
                }

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

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

// Properties file
  static final public 
PropertiesFile PropertiesFile() throws ParseException, PrismLangException {PropertiesFile pf = new PropertiesFile(modelInfo);
        Property prop;
        Token begin = null;
begin = getToken(1);
    label_2:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
      case DLT:
      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_f():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 DLBRACKET:
      case DLT:
      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_f():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 ("" != null) 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(modelInfo);
        Property prop;
        Token begin = null;
begin = getToken(1);
    label_4:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
      case DLT:
      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_f():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 DLBRACKET:
      case DLT:
      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_f():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 ("" != null) 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 ("" != null) 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 ("" != null) return ret;}
    throw new Error("Missing return statement in function");
  }

// A single LTL formula
  static final public 
Expression SingleLTLFormula() throws ParseException {Expression ret;
    ret = Expression(true, true);
    jj_consume_token(0);
{if ("" != null) 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_f():jj_ntk) {
    case DTMC:
    case PROBABILISTIC:{
      switch ((jj_ntk==-1)?jj_ntk_f():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_f():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_f():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 ("" != null) 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_f():jj_ntk) {
    case CONST:{
      jj_consume_token(CONST);
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case BOOL:
      case DOUBLE:
      case INT:{
        switch ((jj_ntk==-1)?jj_ntk_f():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_f():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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 INT:{
      jj_consume_token(INT);
declType = new DeclarationIntUnbounded();
      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 ("" != null) return declType;}
    throw new Error("Missing return statement in function");
  }

// Module
  static final public 
parser.ast.Module Module() throws ParseException {ExpressionIdent name = null;
        Declaration var = null;
        Expression invar;
        Command comm = null;
        parser.ast.Module module = null;
        Token begin = null;
    begin = jj_consume_token(MODULE);
    name = IdentifierExpression();
module = new parser.ast.Module(name.getName());
    label_6:
    while (true) {
      switch ((jj_ntk==-1)?jj_ntk_f():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_f():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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 DLBRACKET:
      case DLT:
      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_f():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 ("" != null) 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_f():jj_ntk) {
    case LPARENTH:{
      UpdateElement(update);
      label_9:
      while (true) {
        switch ((jj_ntk==-1)?jj_ntk_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 DLBRACKET:
      case DLT:
      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_f():jj_ntk) {
      case LBRACKET:{
        jj_consume_token(LBRACKET);
s = "";
        switch ((jj_ntk==-1)?jj_ntk_f():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 ("" != null) 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 ("" != null) return expr;}
    throw new Error("Missing return statement in function");
  }

// System definition ("system...endsystem" construct)
  static final public 
void SystemEndsystem(ModulesFile mf) throws ParseException {String name = null;
        SystemDefn sysdef;
    jj_consume_token(SYSTEM);
    if (jj_2_7(2147483647)) {
      jj_consume_token(DQUOTE);
      name = Identifier();
      jj_consume_token(DQUOTE);
    } else {
      ;
    }
    sysdef = SystemDefn();
    jj_consume_token(ENDSYSTEM);
mf.addSystemDefn(sysdef, name);
  }

// System definition component
  static final public 
SystemDefn SystemDefn() throws ParseException {SystemDefn ret;
    ret = SystemFullParallel();
{if ("" != null) 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_8(2147483647)) {
        ;
      } else {
        break label_12;
      }
      jj_consume_token(OR);
      jj_consume_token(OR);
      sys2 = SystemParallel();
par.addOperand(sys2);
    }
if (par==null || par.getNumOperands() == 1) {
                        {if ("" != null) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if ("" != null) 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_9(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 || par.getNumOperands() == 1) {
                        {if ("" != null) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if ("" != null) 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_10(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_f():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 ("" != null) return sys1;}
                }
                else {
                        par.setPosition(begin, getToken(0));
                        {if ("" != null) 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_f():jj_ntk) {
      case LBRACE:
      case DIVIDE:{
        ;
        break;
        }
      default:
        jj_la1[33] = jj_gen;
        break label_15;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():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_f():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_f():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 ("" != null) 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_f():jj_ntk) {
    case REG_IDENT:{
      name = Identifier();
sys = new SystemModule(name);
      break;
      }
    case DQUOTE:{
      jj_consume_token(DQUOTE);
      name = Identifier();
      jj_consume_token(DQUOTE);
sys = new SystemReference(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 ("" != null) 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 ("" != null) 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_f():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_f():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_f():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 ("" != null) 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_f():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_f():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_f():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 DLBRACKET:
    case DLT:
    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 ("" != null) 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_f():jj_ntk) {
    case LE:{
      jj_consume_token(LE);
      if (jj_2_11(2147483647)) {
        uBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
        case DLT:
        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_12(2147483647)) {
        uBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
        case DLT:
        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_13(2147483647)) {
        lBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
        case DLT:
        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_14(2147483647)) {
        lBound = IdentifierExpression();
      } else {
        switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
        case DLT:
        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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 DLBRACKET:
    case DLT:
    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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():jj_ntk) {
      case PLUS:
      case MINUS:{
        ;
        break;
        }
      default:
        jj_la1[57] = jj_gen;
        break label_24;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():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 ("" != null) 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_f():jj_ntk) {
      case TIMES:
      case DIVIDE:{
        ;
        break;
        }
      default:
        jj_la1[59] = jj_gen;
        break label_25;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():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 ("" != null) 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_f():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 DLBRACKET:
    case DLT:
    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 ("" != null) 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_f():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 DLBRACKET:
    case DLT:{
      ret = ExpressionStrategy(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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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 ("" != null) 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_f():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_f():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 ("" != null) 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 ("" != null) 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 {ExpressionIdent modifier = null;
        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_f():jj_ntk) {
    case P:{
      begin = jj_consume_token(P);
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case LPARENTH:{
        jj_consume_token(LPARENTH);
        modifier = IdentifierExpression();
        jj_consume_token(RPARENTH);
        break;
        }
      default:
        jj_la1[68] = jj_gen;
        ;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():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[69] = 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[70] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = Expression(prop, true);
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case LBRACE:{
      filter = Filter();
      break;
      }
    default:
      jj_la1[71] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
ret.setModifier(modifier == null ? null : modifier.getName());
                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 ("" != null) return ef;}
                }
                else {if ("" != null) 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_f():jj_ntk) {
      case LBRACE:{
        ;
        break;
        }
      default:
        jj_la1[72] = jj_gen;
        break label_27;
      }
      jj_consume_token(LBRACE);
      switch ((jj_ntk==-1)?jj_ntk_f():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[73] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
      jj_consume_token(RBRACE);
    }
filter.setPosition(begin, getToken(0)); {if ("" != null) 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 {ExpressionIdent modifier = null;
        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_f():jj_ntk) {
    case LPARENTH:
    case LT:
    case GT:
    case LE:
    case GE:{
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case LPARENTH:{
        jj_consume_token(LPARENTH);
        modifier = IdentifierExpression();
        jj_consume_token(RPARENTH);
        break;
        }
      default:
        jj_la1[74] = jj_gen;
        ;
      }
      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[75] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = Expression(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case LBRACE:{
      filter = Filter();
      break;
      }
    default:
      jj_la1[76] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
ret.setModifier(modifier == null ? null : modifier.getName());
                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 ("" != null) return ef;}
                }
                else {if ("" != null) 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 {ExpressionIdent modifier = null;
        int r;
        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_f():jj_ntk) {
    case R:{
      begin = jj_consume_token(R);
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case LPARENTH:{
        jj_consume_token(LPARENTH);
        modifier = IdentifierExpression();
        jj_consume_token(RPARENTH);
        break;
        }
      default:
        jj_la1[77] = jj_gen;
        ;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case LBRACE:{
        RewardIndex(ret);
        break;
        }
      default:
        jj_la1[78] = jj_gen;
        ;
      }
      switch ((jj_ntk==-1)?jj_ntk_f():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[79] = 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[80] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(LBRACKET);
    expr = ExpressionRewardContents(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case LBRACE:{
      filter = Filter();
      break;
      }
    default:
      jj_la1[81] = jj_gen;
      ;
    }
    jj_consume_token(RBRACKET);
ret.setModifier(modifier == null ? null : modifier.getName());
                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 ("" != null) return ef;}
                }
                else {if ("" != null) return ret;}
    throw new Error("Missing return statement in function");
  }

// Reward struct index for R operator
  static final public 
void RewardIndex(ExpressionReward exprRew) throws ParseException {Object index = null;
        Object indexDiv = null;
    jj_consume_token(LBRACE);
    if (jj_2_15(2147483647)) {
      jj_consume_token(DQUOTE);
      index = Identifier();
      jj_consume_token(DQUOTE);
    } else {
      switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
      case DLT:
      case MINUS:
      case DQUOTE:
      case REG_INT:
      case REG_DOUBLE:
      case REG_IDENT:{
        index = Expression(false, false);
        break;
        }
      default:
        jj_la1[82] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
    }
    jj_consume_token(RBRACE);
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case DIVIDE:{
      jj_consume_token(DIVIDE);
      jj_consume_token(LBRACE);
      if (jj_2_16(2147483647)) {
        jj_consume_token(DQUOTE);
        indexDiv = Identifier();
        jj_consume_token(DQUOTE);
      } else {
        switch ((jj_ntk==-1)?jj_ntk_f():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 DLBRACKET:
        case DLT:
        case MINUS:
        case DQUOTE:
        case REG_INT:
        case REG_DOUBLE:
        case REG_IDENT:{
          indexDiv = Expression(false, false);
          break;
          }
        default:
          jj_la1[83] = jj_gen;
          jj_consume_token(-1);
          throw new ParseException();
        }
      }
      jj_consume_token(RBRACE);
      break;
      }
    default:
      jj_la1[84] = jj_gen;
      ;
    }
exprRew.setRewardStructIndex(index);
                if (indexDiv != null) {
                        exprRew.setRewardStructIndexDiv(indexDiv);
                }
  }

// Contents of an R operator

// JavaCC warns about lookahead for this function. This is because there is a possible conflict between
// R [ S ], where "S" is the long-run reward operator, and R [ S [ ] ], where "S [ ]" is an LTL formula
// comprising a single atomic proposition. We use lookahead to resolve the ambiguity.
  static final public 
Expression ExpressionRewardContents(boolean prop, boolean pathprop) throws ParseException {Expression expr = null;
        ExpressionTemporal exprTemp = null;
        Expression ret = null;
        Token begin;
begin = getToken(1);
    if (jj_2_17(2147483647)) {
      expr = ExpressionSS(prop, true);
ret = expr;
    } else {
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case S:{
        jj_consume_token(S);
ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
        break;
        }
      default:
        jj_la1[85] = jj_gen;
        if (jj_2_18(2147483647)) {
          begin = jj_consume_token(C);
          jj_consume_token(LE);
          expr = Expression(false, false);
exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp;
        } else {
          switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
          case C:{
            jj_consume_token(C);
ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null);
            break;
            }
          case I:{
            jj_consume_token(I);
            jj_consume_token(EQ);
            expr = Expression(false, false);
exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp;
            break;
            }
          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 DLBRACKET:
          case DLT:
          case MINUS:
          case DQUOTE:
          case REG_INT:
          case REG_DOUBLE:
          case REG_IDENT:{
            expr = Expression(prop, true);
ret = expr;
            break;
            }
          default:
            jj_la1[86] = jj_gen;
            jj_consume_token(-1);
            throw new ParseException();
          }
        }
      }
    }
ret.setPosition(begin, getToken(0)); {if ("" != null) 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 ("" != null) 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 ("" != null) return ret;}
    throw new Error("Missing return statement in function");
  }

// (Property) expression: ATL strategy operators <<>> and [[]]
  static final public 
Expression ExpressionStrategy(boolean prop, boolean pathprop) throws ParseException {ExpressionStrategy ret;
        Expression expr;
        Token begin = null;
if (!prop) {if (true) throw generateParseException();}
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case DLT:{
      begin = jj_consume_token(DLT);
ret = new ExpressionStrategy(true);
      ExpressionStrategyCoalition(ret);
      jj_consume_token(DGT);
      break;
      }
    case DLBRACKET:{
      begin = jj_consume_token(DLBRACKET);
ret = new ExpressionStrategy(false);
      ExpressionStrategyCoalition(ret);
      jj_consume_token(DRBRACKET);
      break;
      }
    default:
      jj_la1[87] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case PMAX:
    case PMIN:
    case P:
    case RMAX:
    case RMIN:
    case R:{
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case PMAX:
      case PMIN:
      case P:{
        expr = ExpressionProb(prop, pathprop);
        break;
        }
      case RMAX:
      case RMIN:
      case R:{
        expr = ExpressionReward(prop, pathprop);
        break;
        }
      default:
        jj_la1[88] = jj_gen;
        jj_consume_token(-1);
        throw new ParseException();
      }
ret.setSingleOperand(expr);
      break;
      }
    case LPARENTH:{
      expr = ExpressionParenth(prop, pathprop);
ret.addOperand(expr);
      break;
      }
    default:
      jj_la1[89] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
ret.setPosition(begin, getToken(0));
                {if ("" != null) return ret;}
    throw new Error("Missing return statement in function");
  }

// Coalition (player list) for a strategy (<<>> or [[]]) operator
  static final public 
void ExpressionStrategyCoalition(ExpressionStrategy exprStrat) throws ParseException {List<String> coalition = new ArrayList<String>();
        String s;
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case TIMES:{
      jj_consume_token(TIMES);
exprStrat.setCoalitionAllPlayers();
      break;
      }
    default:
      jj_la1[92] = jj_gen;
      switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
      case REG_INT:
      case REG_IDENT:{
        s = ExpressionStrategyCoalitionPlayer();
coalition.add(s);
        label_28:
        while (true) {
          switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
          case COMMA:{
            ;
            break;
            }
          default:
            jj_la1[90] = jj_gen;
            break label_28;
          }
          jj_consume_token(COMMA);
          s = ExpressionStrategyCoalitionPlayer();
coalition.add(s);
        }
        break;
        }
      default:
        jj_la1[91] = jj_gen;
        ;
      }
exprStrat.setCoalition(coalition);
    }
  }

// Single player in a coalition for a strategy (<<>> or [[]]) operator
  static final public 
String ExpressionStrategyCoalitionPlayer() throws ParseException {String s;
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case REG_INT:{
      jj_consume_token(REG_INT);
      break;
      }
    case REG_IDENT:{
      jj_consume_token(REG_IDENT);
      break;
      }
    default:
      jj_la1[93] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
s = getToken(0).image;
{if ("" != null) return s;}
    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_f():jj_ntk) {
    case REG_IDENT:{
      s = Identifier();
      break;
      }
    case INIT:{
      jj_consume_token(INIT);
s = "init";
      break;
      }
    default:
      jj_la1[94] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(DQUOTE);
ret = new ExpressionLabel(s); ret.setPosition(begin, getToken(0)); {if ("" != null) 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_f():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[95] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
    jj_consume_token(COMMA);
    expr2 = Expression(prop, pathprop);
    switch ((jj_ntk==-1)?jj_ntk_f():jj_ntk) {
    case COMMA:{
      jj_consume_token(COMMA);
      filter = Expression(prop, pathprop);
      break;
      }
    default:
      jj_la1[96] = jj_gen;
      ;
    }
    jj_consume_token(RPARENTH);
expr = new ExpressionFilter(op, expr2, filter); expr.setPosition(begin, getToken(0)); {if ("" != null) 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 ("" != null) 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 ("" != null) 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_f():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[97] = jj_gen;
      jj_consume_token(-1);
      throw new ParseException();
    }
ret = new ExpressionIdent(ident); ret.setPosition(getToken(0)); {if ("" != null) 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 ("" != null) 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_f():jj_ntk) {
    case EQ:{
      jj_consume_token(EQ);
{if ("" != null) return ExpressionBinaryOp.EQ;}
      break;
      }
    case NE:{
      jj_consume_token(NE);
{if ("" != null) return ExpressionBinaryOp.NE;}
      break;
      }
    default:
      jj_la1[98] = 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_f():jj_ntk) {
    case GT:{
      jj_consume_token(GT);
{if ("" != null) return ExpressionBinaryOp.GT;}
      break;
      }
    case LT:{
      jj_consume_token(LT);
{if ("" != null) return ExpressionBinaryOp.LT;}
      break;
      }
    case GE:{
      jj_consume_token(GE);
{if ("" != null) return ExpressionBinaryOp.GE;}
      break;
      }
    case LE:{
      jj_consume_token(LE);
{if ("" != null) return ExpressionBinaryOp.LE;}
      break;
      }
    default:
      jj_la1[99] = 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_f():jj_ntk) {
    case COLON:{
      jj_consume_token(COLON);
      step = Expression(false, false);
      break;
      }
    default:
      jj_la1[100] = 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 ("" != null) 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_2_16(int xla)
 {
    jj_la = xla; jj_lastpos = jj_scanpos = token;
    try { return !jj_3_16(); }
    catch(LookaheadSuccess ls) { return true; }
    finally { jj_save(15, xla); }
  }

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

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

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

  static private boolean jj_3R_46()
 {
    if (jj_3R_55()) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_56()) jj_scanpos = xsp;
    return false;
  }

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

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

  static private boolean jj_3R_146()
 {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_38()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

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

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

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

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

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

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

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

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

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

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

  static private boolean jj_3R_155()
 {
    if (jj_scan_token(REG_DOUBLE)) 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_186()
 {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_38()) return true;
    return false;
  }

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

  static private boolean jj_3R_79()
 {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_31()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

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

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

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

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

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

  static private boolean jj_3R_142()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_154()) {
    jj_scanpos = xsp;
    if (jj_3R_155()) {
    jj_scanpos = xsp;
    if (jj_3R_156()) {
    jj_scanpos = xsp;
    if (jj_3R_157()) return true;
    }
    }
    }
    return false;
  }

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

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

  static private boolean jj_3R_70()
 {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_29()) return true;
    return false;
  }

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

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

  static private boolean jj_3R_153()
 {
    if (jj_scan_token(FILTER)) return true;
    if (jj_scan_token(LPARENTH)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_180()) {
    jj_scanpos = xsp;
    if (jj_3R_181()) {
    jj_scanpos = xsp;
    if (jj_3R_182()) {
    jj_scanpos = xsp;
    if (jj_3R_183()) {
    jj_scanpos = xsp;
    if (jj_3R_184()) {
    jj_scanpos = xsp;
    if (jj_3R_185()) return true;
    }
    }
    }
    }
    }
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_38()) return true;
    xsp = jj_scanpos;
    if (jj_3R_186()) jj_scanpos = xsp;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_161()
 {
    if (jj_3R_38()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_187()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_91()
 {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_29()) return true;
    if (jj_scan_token(RENAME)) return true;
    if (jj_3R_29()) return true;
    return false;
  }

  static private boolean jj_3_9()
 {
    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_81()
 {
    if (jj_scan_token(LBRACE)) return true;
    if (jj_3R_29()) return true;
    if (jj_scan_token(RENAME)) return true;
    if (jj_3R_29()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_91()) { jj_scanpos = xsp; break; }
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

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

  static private boolean jj_3R_145()
 {
    if (jj_scan_token(FUNC)) return true;
    if (jj_scan_token(LPARENTH)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_162()) {
    jj_scanpos = xsp;
    if (jj_3R_163()) {
    jj_scanpos = xsp;
    if (jj_3R_164()) return true;
    }
    }
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_161()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_152()
 {
    if (jj_scan_token(DQUOTE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_178()) {
    jj_scanpos = xsp;
    if (jj_3R_179()) return true;
    }
    if (jj_scan_token(DQUOTE)) return true;
    return false;
  }

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

  static private boolean jj_3R_80()
 {
    if (jj_scan_token(DIVIDE)) return true;
    if (jj_scan_token(LBRACE)) return true;
    if (jj_3R_29()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_90()) { jj_scanpos = xsp; break; }
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

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

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

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

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

  static private boolean jj_3R_144()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_159()) {
    jj_scanpos = xsp;
    if (jj_3R_160()) return true;
    }
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_161()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_217()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_scan_token(86)) {
    jj_scanpos = xsp;
    if (jj_scan_token(89)) return true;
    }
    return false;
  }

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

  static private boolean jj_3R_158()
 {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_161()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

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

  static private boolean jj_3R_218()
 {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_217()) return true;
    return false;
  }

  static private boolean jj_3R_214()
 {
    if (jj_3R_217()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_218()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_210()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_214()) jj_scanpos = xsp;
    return false;
  }

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

  static private boolean jj_3R_143()
 {
    if (jj_3R_29()) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_158()) jj_scanpos = xsp;
    return false;
  }

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

  static private boolean jj_3R_205()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_209()) {
    jj_scanpos = xsp;
    if (jj_3R_210()) return true;
    }
    return false;
  }

  static private boolean jj_3R_59()
 {
    if (jj_scan_token(OR)) return true;
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_29()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_70()) { jj_scanpos = xsp; break; }
    }
    if (jj_scan_token(RBRACKET)) return true;
    if (jj_scan_token(OR)) return true;
    if (jj_3R_58()) return true;
    return false;
  }

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

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

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

  static private boolean jj_3R_177()
 {
    if (jj_3R_146()) return true;
    return false;
  }

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

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

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

  static private boolean jj_3R_176()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_206()) {
    jj_scanpos = xsp;
    if (jj_3R_207()) return true;
    }
    return false;
  }

  static private boolean jj_3R_175()
 {
    if (jj_scan_token(DLBRACKET)) return true;
    if (jj_3R_205()) return true;
    if (jj_scan_token(DRBRACKET)) return true;
    return false;
  }

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

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

  static private boolean jj_3R_216()
 {
    if (jj_3R_38()) return true;
    return false;
  }

  static private boolean jj_3R_174()
 {
    if (jj_scan_token(DLT)) return true;
    if (jj_3R_205()) return true;
    if (jj_scan_token(DGT)) return true;
    return false;
  }

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

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

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

  static private boolean jj_3R_151()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_174()) {
    jj_scanpos = xsp;
    if (jj_3R_175()) return true;
    }
    xsp = jj_scanpos;
    if (jj_3R_176()) {
    jj_scanpos = xsp;
    if (jj_3R_177()) return true;
    }
    return false;
  }

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

  static private boolean jj_3R_132()
 {
    if (jj_3R_145()) return true;
    return false;
  }

  static private boolean jj_3R_42()
 {
    if (jj_3R_49()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_50()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

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

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

  static private boolean jj_3R_212()
 {
    if (jj_3R_38()) return true;
    return false;
  }

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

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

  static private boolean jj_3R_128()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_129()) {
    jj_scanpos = xsp;
    if (jj_3R_130()) {
    jj_scanpos = xsp;
    if (jj_3R_131()) {
    jj_scanpos = xsp;
    if (jj_3R_132()) {
    jj_scanpos = xsp;
    if (jj_3R_133()) {
    jj_scanpos = xsp;
    if (jj_3R_134()) {
    jj_scanpos = xsp;
    if (jj_3R_135()) {
    jj_scanpos = xsp;
    if (jj_3R_136()) {
    jj_scanpos = xsp;
    if (jj_3R_137()) {
    jj_scanpos = xsp;
    if (jj_3R_138()) {
    jj_scanpos = xsp;
    if (jj_3R_139()) {
    jj_scanpos = xsp;
    if (jj_3R_140()) {
    jj_scanpos = xsp;
    if (jj_3R_141()) return true;
    }
    }
    }
    }
    }
    }
    }
    }
    }
    }
    }
    }
    return false;
  }

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

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

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

  static private boolean jj_3R_120()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_124()) {
    jj_scanpos = xsp;
    if (jj_3R_125()) return true;
    }
    return false;
  }

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

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

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

  static private boolean jj_3R_121()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_126()) {
    jj_scanpos = xsp;
    if (jj_3R_127()) return true;
    }
    if (jj_3R_120()) return true;
    return false;
  }

  static private boolean jj_3_7()
 {
    if (jj_scan_token(DQUOTE)) return true;
    if (jj_3R_29()) return true;
    if (jj_scan_token(DQUOTE)) return true;
    if (jj_3R_31()) return true;
    return false;
  }

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

  static private boolean jj_3R_204()
 {
    if (jj_3R_38()) return true;
    return false;
  }

  static private boolean jj_3R_116()
 {
    if (jj_3R_120()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_121()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3_17()
 {
    if (jj_3R_33()) return true;
    return false;
  }

  static private boolean jj_3R_203()
 {
    if (jj_scan_token(I)) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_3R_38()) return true;
    return false;
  }

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

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

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

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

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

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

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

  static private boolean jj_3R_117()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_122()) {
    jj_scanpos = xsp;
    if (jj_3R_123()) return true;
    }
    if (jj_3R_116()) return true;
    return false;
  }

  static private boolean jj_3R_199()
 {
    if (jj_3R_33()) return true;
    return false;
  }

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

  static private boolean jj_3R_172()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_199()) {
    jj_scanpos = xsp;
    if (jj_3R_200()) {
    jj_scanpos = xsp;
    if (jj_3R_201()) {
    jj_scanpos = xsp;
    if (jj_3R_202()) {
    jj_scanpos = xsp;
    if (jj_3R_203()) {
    jj_scanpos = xsp;
    if (jj_3R_204()) return true;
    }
    }
    }
    }
    }
    return false;
  }

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

  static private boolean jj_3R_113()
 {
    if (jj_3R_116()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_117()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

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

  static private boolean jj_3R_213()
 {
    if (jj_scan_token(DIVIDE)) return true;
    if (jj_scan_token(LBRACE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_215()) {
    jj_scanpos = xsp;
    if (jj_3R_216()) return true;
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

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

  static private boolean jj_3R_208()
 {
    if (jj_scan_token(LBRACE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_211()) {
    jj_scanpos = xsp;
    if (jj_3R_212()) return true;
    }
    if (jj_scan_token(RBRACE)) return true;
    xsp = jj_scanpos;
    if (jj_3R_213()) jj_scanpos = xsp;
    return false;
  }

  static private boolean jj_3R_111()
 {
    if (jj_3R_113()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_114()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

  static private boolean jj_3R_110()
 {
    if (jj_3R_111()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_112()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

  static private boolean jj_3R_108()
 {
    if (jj_scan_token(NOT)) return true;
    if (jj_3R_106()) return true;
    return false;
  }

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

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

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

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

  static private boolean jj_3R_195()
 {
    if (jj_3R_45()) return true;
    if (jj_3R_38()) return true;
    return false;
  }

  static private boolean jj_3R_194()
 {
    if (jj_3R_208()) return true;
    return false;
  }

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

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

  static private boolean jj_3R_198()
 {
    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_171()
 {
    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_197()
 {
    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_170()
 {
    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_106()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_108()) {
    jj_scanpos = xsp;
    if (jj_3R_109()) return true;
    }
    return false;
  }

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

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

  static private boolean jj_3R_169()
 {
    if (jj_scan_token(R)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_193()) jj_scanpos = xsp;
    xsp = jj_scanpos;
    if (jj_3R_194()) jj_scanpos = xsp;
    xsp = jj_scanpos;
    if (jj_3R_195()) {
    jj_scanpos = xsp;
    if (jj_3R_196()) {
    jj_scanpos = xsp;
    if (jj_3R_197()) {
    jj_scanpos = xsp;
    if (jj_3R_198()) return true;
    }
    }
    }
    return false;
  }

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

  static private boolean jj_3R_148()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_169()) {
    jj_scanpos = xsp;
    if (jj_3R_170()) {
    jj_scanpos = xsp;
    if (jj_3R_171()) return true;
    }
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_172()) return true;
    xsp = jj_scanpos;
    if (jj_3R_173()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_40()
 {
    if (jj_scan_token(LPARENTH)) return true;
    if (jj_3R_48()) return true;
    if (jj_scan_token(EQ)) return true;
    if (jj_3R_38()) return true;
    if (jj_scan_token(RPARENTH)) return true;
    return false;
  }

  static private boolean jj_3R_104()
 {
    if (jj_3R_106()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_107()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

  static private boolean jj_3R_34()
 {
    if (jj_3R_40()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_41()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

  static private boolean jj_3R_102()
 {
    if (jj_3R_104()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_105()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_30()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_34()) {
    jj_scanpos = xsp;
    if (jj_scan_token(49)) return true;
    }
    return false;
  }

  static private boolean jj_3R_103()
 {
    if (jj_scan_token(IFF)) return true;
    if (jj_3R_102()) return true;
    return false;
  }

  static private boolean jj_3R_92()
 {
    if (jj_3R_102()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_103()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

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

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

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

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

  static private boolean jj_3R_82()
 {
    if (jj_3R_92()) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_93()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_33()
 {
    if (jj_scan_token(S)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_36()) {
    jj_scanpos = xsp;
    if (jj_3R_37()) return true;
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_38()) return true;
    xsp = jj_scanpos;
    if (jj_3R_39()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_83()
 {
    if (jj_scan_token(QMARK)) return true;
    if (jj_3R_82()) return true;
    if (jj_scan_token(COLON)) return true;
    if (jj_3R_75()) return true;
    return false;
  }

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

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

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

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

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

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

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

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

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

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

  static private boolean jj_3R_96()
 {
    if (jj_3R_32()) return true;
    return false;
  }

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

  static private boolean jj_3R_57()
 {
    if (jj_scan_token(LBRACE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_66()) {
    jj_scanpos = xsp;
    if (jj_3R_67()) return true;
    }
    if (jj_scan_token(RBRACE)) return true;
    return false;
  }

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

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

  static private boolean jj_3R_47()
 {
    if (jj_scan_token(LBRACE)) return true;
    if (jj_3R_38()) return true;
    if (jj_scan_token(RBRACE)) return true;
    Token xsp;
    while (true) {
      xsp = jj_scanpos;
      if (jj_3R_57()) { jj_scanpos = xsp; break; }
    }
    return false;
  }

  static private boolean jj_3R_87()
 {
    if (jj_scan_token(GT)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_100()) {
    jj_scanpos = xsp;
    if (jj_3R_101()) return true;
    }
    return false;
  }

  static private boolean jj_3R_86()
 {
    if (jj_scan_token(GE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_98()) {
    jj_scanpos = xsp;
    if (jj_3R_99()) return true;
    }
    return false;
  }

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

  static private boolean jj_3R_84()
 {
    if (jj_scan_token(LE)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_94()) {
    jj_scanpos = xsp;
    if (jj_3R_95()) return true;
    }
    return false;
  }

  static private boolean jj_3R_76()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_84()) {
    jj_scanpos = xsp;
    if (jj_3R_85()) {
    jj_scanpos = xsp;
    if (jj_3R_86()) {
    jj_scanpos = xsp;
    if (jj_3R_87()) {
    jj_scanpos = xsp;
    if (jj_3R_88()) {
    jj_scanpos = xsp;
    if (jj_3R_89()) return true;
    }
    }
    }
    }
    }
    return false;
  }

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

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

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

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

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

  static private boolean jj_3R_60()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_71()) {
    jj_scanpos = xsp;
    if (jj_3R_72()) {
    jj_scanpos = xsp;
    if (jj_3R_73()) return true;
    }
    }
    xsp = jj_scanpos;
    if (jj_3R_74()) jj_scanpos = xsp;
    if (jj_3R_55()) return true;
    return false;
  }

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

  static private boolean jj_3R_189()
 {
    if (jj_3R_45()) return true;
    if (jj_3R_38()) return true;
    return false;
  }

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

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

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

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

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

  static private boolean jj_3R_192()
 {
    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_191()
 {
    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_190()
 {
    if (jj_scan_token(EQ)) return true;
    if (jj_scan_token(QMARK)) return true;
    return false;
  }

  static private boolean jj_3R_167()
 {
    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_55()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_60()) {
    jj_scanpos = xsp;
    if (jj_3R_61()) return true;
    }
    return false;
  }

  static private boolean jj_3R_166()
 {
    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_119()
 {
    if (jj_scan_token(NE)) return true;
    return false;
  }

  static private boolean jj_3R_115()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_118()) {
    jj_scanpos = xsp;
    if (jj_3R_119()) return true;
    }
    return false;
  }

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

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

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

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

  static private boolean jj_3R_165()
 {
    if (jj_scan_token(P)) return true;
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_188()) jj_scanpos = xsp;
    xsp = jj_scanpos;
    if (jj_3R_189()) {
    jj_scanpos = xsp;
    if (jj_3R_190()) {
    jj_scanpos = xsp;
    if (jj_3R_191()) {
    jj_scanpos = xsp;
    if (jj_3R_192()) return true;
    }
    }
    }
    return false;
  }

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

  static private boolean jj_3R_147()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_165()) {
    jj_scanpos = xsp;
    if (jj_3R_166()) {
    jj_scanpos = xsp;
    if (jj_3R_167()) return true;
    }
    }
    if (jj_scan_token(LBRACKET)) return true;
    if (jj_3R_38()) return true;
    xsp = jj_scanpos;
    if (jj_3R_168()) jj_scanpos = xsp;
    if (jj_scan_token(RBRACKET)) return true;
    return false;
  }

  static private boolean jj_3R_56()
 {
    Token xsp;
    xsp = jj_scanpos;
    if (jj_3R_62()) {
    jj_scanpos = xsp;
    if (jj_3R_63()) {
    jj_scanpos = xsp;
    if (jj_3R_64()) return true;
    }
    }
    xsp = jj_scanpos;
    if (jj_3R_65()) jj_scanpos = xsp;
    if (jj_3R_55()) return true;
    return false;
  }

  static private boolean jj_3R_187()
 {
    if (jj_scan_token(COMMA)) return true;
    if (jj_3R_38()) return true;
    return false;
  }

  static private boolean jj_3R_48()
 {
    if (jj_scan_token(REG_IDENTPRIME)) 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[101];
  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,0x8000030,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,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x0,0xa4ba0908,0x0,0x0,0x0,0x0,0x0,0x0,0x0,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,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x4012783a,0x0,0x3838,0x40003838,0x10000000,0x0,0x0,0x0,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
   }
   private static void jj_la1_init_2() {
      jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x2e08404,0x404,0x0,0x0,0x0,0x2400000,0x10000,0x2400000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,};
   }
  static final private JJCalls[] jj_2_rtns = new JJCalls[18];
  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 < 101; 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 < 101; 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 < 101; 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 < 101; 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 < 101; 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 < 101; 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();
  }

  @SuppressWarnings("serial")
  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_f() {
    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[92];
    if (jj_kind >= 0) {
      la1tokens[jj_kind] = true;
      jj_kind = -1;
    }
    for (int i = 0; i < 101; 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 < 92; 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 < 18; 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;
            case 15: jj_3_16(); break;
            case 16: jj_3_17(); break;
            case 17: jj_3_18(); 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;
  }

}

//-----------------------------------------------------------------------------------

