public final AntlrPilarParser.action_return action()
      throws RecognitionException {
    AntlrPilarParser.action_return retval = new AntlrPilarParser.action_return();
    retval.start = input.LT(1);
    int action_StartIndex = input.index();
    Object root_0 = null;

    Token t = null;
    Token char_literal240 = null;
    Token char_literal241 = null;
    Token char_literal242 = null;
    Token char_literal244 = null;
    Token char_literal247 = null;
    Token char_literal248 = null;
    Token char_literal249 = null;
    Token char_literal250 = null;
    Token char_literal252 = null;
    Token char_literal255 = null;
    Token char_literal258 = null;
    AntlrPilarParser.exp_return e1 = null;

    AntlrPilarParser.exp_return e2 = null;

    AntlrPilarParser.annotationList_return annotationList243 = null;

    AntlrPilarParser.exp_return exp245 = null;

    AntlrPilarParser.annotationList_return annotationList246 = null;

    AntlrPilarParser.annotationList_return annotationList251 = null;

    AntlrPilarParser.exp_return exp253 = null;

    AntlrPilarParser.annotationList_return annotationList254 = null;

    AntlrPilarParser.exp_return exp256 = null;

    AntlrPilarParser.annotationList_return annotationList257 = null;

    AntlrPilarParser.assignment_return assignment259 = null;

    AntlrPilarParser.startThread_return startThread260 = null;

    AntlrPilarParser.extCall_return extCall261 = null;

    Object t_tree = null;
    Object char_literal240_tree = null;
    Object char_literal241_tree = null;
    Object char_literal242_tree = null;
    Object char_literal244_tree = null;
    Object char_literal247_tree = null;
    Object char_literal248_tree = null;
    Object char_literal249_tree = null;
    Object char_literal250_tree = null;
    Object char_literal252_tree = null;
    Object char_literal255_tree = null;
    Object char_literal258_tree = null;
    RewriteRuleTokenStream stream_170 = new RewriteRuleTokenStream(adaptor,
        "token 170");
    RewriteRuleTokenStream stream_198 = new RewriteRuleTokenStream(adaptor,
        "token 198");
    RewriteRuleTokenStream stream_199 = new RewriteRuleTokenStream(adaptor,
        "token 199");
    RewriteRuleTokenStream stream_175 = new RewriteRuleTokenStream(adaptor,
        "token 175");
    RewriteRuleTokenStream stream_172 = new RewriteRuleTokenStream(adaptor,
        "token 172");
    RewriteRuleTokenStream stream_169 = new RewriteRuleTokenStream(adaptor,
        "token 169");
    RewriteRuleTokenStream stream_197 = new RewriteRuleTokenStream(adaptor,
        "token 197");
    RewriteRuleSubtreeStream stream_exp = new RewriteRuleSubtreeStream(adaptor,
        "rule exp");
    RewriteRuleSubtreeStream stream_annotationList = new RewriteRuleSubtreeStream(
        adaptor, "rule annotationList");
    try {
      if (state.backtracking > 0 && alreadyParsedRule(input, 64)) {
        return retval;
      }
      // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:492:2: (t= 'assert' '(' e1= exp ',' e2= exp ')' annotationList ';' -> ^( ASSERTM[$t] $e1 $e2 annotationList ) | t= 'assert' exp annotationList ';' -> ^( ASSERT[$t] exp annotationList ) | t= 'assume' '(' e1= exp ',' e2= exp ')' annotationList ';' -> ^( ASSUMEM[$t] $e1 $e2 annotationList ) | t= 'assume' exp annotationList ';' -> ^( ASSUME[$t] exp annotationList ) | t= 'throw' exp annotationList ';' -> ^( THROW[$t] exp annotationList ) | assignment | startThread | extCall )
      int alt79 = 8;
      alt79 = dfa79.predict(input);
      switch (alt79) {
        case 1:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:492:4: t= 'assert' '(' e1= exp ',' e2= exp ')' annotationList ';'
        {
          t = (Token) match(input, 197, FOLLOW_197_in_action4505);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_197.add(t);

          char_literal240 = (Token) match(input, 169, FOLLOW_169_in_action4507);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_169.add(char_literal240);

          pushFollow(FOLLOW_exp_in_action4511);
          e1 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(e1.getTree());
          char_literal241 = (Token) match(input, 172, FOLLOW_172_in_action4513);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_172.add(char_literal241);

          pushFollow(FOLLOW_exp_in_action4517);
          e2 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(e2.getTree());
          char_literal242 = (Token) match(input, 170, FOLLOW_170_in_action4519);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_170.add(char_literal242);

          pushFollow(FOLLOW_annotationList_in_action4524);
          annotationList243 = annotationList();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            stream_annotationList.add(annotationList243.getTree());
          char_literal244 = (Token) match(input, 175, FOLLOW_175_in_action4526);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_175.add(char_literal244);

          // AST REWRITE
          // elements: e1, e2, annotationList
          // token labels: 
          // rule labels: retval, e1, e2
          // token list labels: 
          // rule list labels: 
          // wildcard labels: 
          if (state.backtracking == 0) {
            retval.tree = root_0;
            RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
                adaptor, "rule retval", retval != null ? retval.tree : null);
            RewriteRuleSubtreeStream stream_e1 = new RewriteRuleSubtreeStream(
                adaptor, "rule e1", e1 != null ? e1.tree : null);
            RewriteRuleSubtreeStream stream_e2 = new RewriteRuleSubtreeStream(
                adaptor, "rule e2", e2 != null ? e2.tree : null);

            root_0 = (Object) adaptor.nil();
            // 493:41: -> ^( ASSERTM[$t] $e1 $e2 annotationList )
            {
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:493:44: ^( ASSERTM[$t] $e1 $e2 annotationList )
              {
                Object root_1 = (Object) adaptor.nil();
                root_1 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(ASSERTM, t),
                    root_1);

                adaptor.addChild(root_1, stream_e1.nextTree());
                adaptor.addChild(root_1, stream_e2.nextTree());
                adaptor.addChild(root_1, stream_annotationList.nextTree());

                adaptor.addChild(root_0, root_1);
              }

            }

            retval.tree = root_0;
          }
        }
          break;
        case 2:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:494:4: t= 'assert' exp annotationList ';'
        {
          t = (Token) match(input, 197, FOLLOW_197_in_action4566);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_197.add(t);

          pushFollow(FOLLOW_exp_in_action4568);
          exp245 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(exp245.getTree());
          pushFollow(FOLLOW_annotationList_in_action4570);
          annotationList246 = annotationList();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            stream_annotationList.add(annotationList246.getTree());
          char_literal247 = (Token) match(input, 175, FOLLOW_175_in_action4572);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_175.add(char_literal247);

          // AST REWRITE
          // elements: exp, annotationList
          // token labels: 
          // rule labels: retval
          // token list labels: 
          // rule list labels: 
          // wildcard labels: 
          if (state.backtracking == 0) {
            retval.tree = root_0;
            RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
                adaptor, "rule retval", retval != null ? retval.tree : null);

            root_0 = (Object) adaptor.nil();
            // 494:41: -> ^( ASSERT[$t] exp annotationList )
            {
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:494:44: ^( ASSERT[$t] exp annotationList )
              {
                Object root_1 = (Object) adaptor.nil();
                root_1 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(ASSERT, t),
                    root_1);

                adaptor.addChild(root_1, stream_exp.nextTree());
                adaptor.addChild(root_1, stream_annotationList.nextTree());

                adaptor.addChild(root_0, root_1);
              }

            }

            retval.tree = root_0;
          }
        }
          break;
        case 3:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:495:4: t= 'assume' '(' e1= exp ',' e2= exp ')' annotationList ';'
        {
          t = (Token) match(input, 198, FOLLOW_198_in_action4593);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_198.add(t);

          char_literal248 = (Token) match(input, 169, FOLLOW_169_in_action4595);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_169.add(char_literal248);

          pushFollow(FOLLOW_exp_in_action4599);
          e1 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(e1.getTree());
          char_literal249 = (Token) match(input, 172, FOLLOW_172_in_action4601);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_172.add(char_literal249);

          pushFollow(FOLLOW_exp_in_action4605);
          e2 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(e2.getTree());
          char_literal250 = (Token) match(input, 170, FOLLOW_170_in_action4607);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_170.add(char_literal250);

          pushFollow(FOLLOW_annotationList_in_action4612);
          annotationList251 = annotationList();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            stream_annotationList.add(annotationList251.getTree());
          char_literal252 = (Token) match(input, 175, FOLLOW_175_in_action4614);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_175.add(char_literal252);

          // AST REWRITE
          // elements: e2, annotationList, e1
          // token labels: 
          // rule labels: retval, e1, e2
          // token list labels: 
          // rule list labels: 
          // wildcard labels: 
          if (state.backtracking == 0) {
            retval.tree = root_0;
            RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
                adaptor, "rule retval", retval != null ? retval.tree : null);
            RewriteRuleSubtreeStream stream_e1 = new RewriteRuleSubtreeStream(
                adaptor, "rule e1", e1 != null ? e1.tree : null);
            RewriteRuleSubtreeStream stream_e2 = new RewriteRuleSubtreeStream(
                adaptor, "rule e2", e2 != null ? e2.tree : null);

            root_0 = (Object) adaptor.nil();
            // 496:41: -> ^( ASSUMEM[$t] $e1 $e2 annotationList )
            {
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:496:44: ^( ASSUMEM[$t] $e1 $e2 annotationList )
              {
                Object root_1 = (Object) adaptor.nil();
                root_1 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(ASSUMEM, t),
                    root_1);

                adaptor.addChild(root_1, stream_e1.nextTree());
                adaptor.addChild(root_1, stream_e2.nextTree());
                adaptor.addChild(root_1, stream_annotationList.nextTree());

                adaptor.addChild(root_0, root_1);
              }

            }

            retval.tree = root_0;
          }
        }
          break;
        case 4:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:497:4: t= 'assume' exp annotationList ';'
        {
          t = (Token) match(input, 198, FOLLOW_198_in_action4654);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_198.add(t);

          pushFollow(FOLLOW_exp_in_action4656);
          exp253 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(exp253.getTree());
          pushFollow(FOLLOW_annotationList_in_action4658);
          annotationList254 = annotationList();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            stream_annotationList.add(annotationList254.getTree());
          char_literal255 = (Token) match(input, 175, FOLLOW_175_in_action4660);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_175.add(char_literal255);

          // AST REWRITE
          // elements: annotationList, exp
          // token labels: 
          // rule labels: retval
          // token list labels: 
          // rule list labels: 
          // wildcard labels: 
          if (state.backtracking == 0) {
            retval.tree = root_0;
            RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
                adaptor, "rule retval", retval != null ? retval.tree : null);

            root_0 = (Object) adaptor.nil();
            // 497:41: -> ^( ASSUME[$t] exp annotationList )
            {
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:497:44: ^( ASSUME[$t] exp annotationList )
              {
                Object root_1 = (Object) adaptor.nil();
                root_1 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(ASSUME, t),
                    root_1);

                adaptor.addChild(root_1, stream_exp.nextTree());
                adaptor.addChild(root_1, stream_annotationList.nextTree());

                adaptor.addChild(root_0, root_1);
              }

            }

            retval.tree = root_0;
          }
        }
          break;
        case 5:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:498:4: t= 'throw' exp annotationList ';'
        {
          t = (Token) match(input, 199, FOLLOW_199_in_action4681);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_199.add(t);

          pushFollow(FOLLOW_exp_in_action4683);
          exp256 = exp();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_exp.add(exp256.getTree());
          pushFollow(FOLLOW_annotationList_in_action4685);
          annotationList257 = annotationList();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            stream_annotationList.add(annotationList257.getTree());
          char_literal258 = (Token) match(input, 175, FOLLOW_175_in_action4687);
          if (state.failed) return retval;
          if (state.backtracking == 0) stream_175.add(char_literal258);

          // AST REWRITE
          // elements: annotationList, exp
          // token labels: 
          // rule labels: retval
          // token list labels: 
          // rule list labels: 
          // wildcard labels: 
          if (state.backtracking == 0) {
            retval.tree = root_0;
            RewriteRuleSubtreeStream stream_retval = new RewriteRuleSubtreeStream(
                adaptor, "rule retval", retval != null ? retval.tree : null);

            root_0 = (Object) adaptor.nil();
            // 498:41: -> ^( THROW[$t] exp annotationList )
            {
              // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:498:44: ^( THROW[$t] exp annotationList )
              {
                Object root_1 = (Object) adaptor.nil();
                root_1 = (Object) adaptor.becomeRoot(
                    (Object) adaptor.create(THROW, t),
                    root_1);

                adaptor.addChild(root_1, stream_exp.nextTree());
                adaptor.addChild(root_1, stream_annotationList.nextTree());

                adaptor.addChild(root_0, root_1);
              }

            }

            retval.tree = root_0;
          }
        }
          break;
        case 6:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:499:4: assignment
        {
          root_0 = (Object) adaptor.nil();

          pushFollow(FOLLOW_assignment_in_action4707);
          assignment259 = assignment();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            adaptor.addChild(root_0, assignment259.getTree());

        }
          break;
        case 7:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:500:4: startThread
        {
          root_0 = (Object) adaptor.nil();

          pushFollow(FOLLOW_startThread_in_action4713);
          startThread260 = startThread();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            adaptor.addChild(root_0, startThread260.getTree());

        }
          break;
        case 8:
        // /Users/robby/Repositories/sireum-parser/sireum-parser/src/main/java/org/sireum/pilar/parser/AntlrPilar.g:501:4: extCall
        {
          root_0 = (Object) adaptor.nil();

          pushFollow(FOLLOW_extCall_in_action4718);
          extCall261 = extCall();

          state._fsp--;
          if (state.failed) return retval;
          if (state.backtracking == 0)
            adaptor.addChild(root_0, extCall261.getTree());

        }
          break;

      }
      retval.stop = input.LT(-1);

      if (state.backtracking == 0) {

        retval.tree = (Object) adaptor.rulePostProcessing(root_0);
        adaptor.setTokenBoundaries(retval.tree, retval.start, retval.stop);
      }
    } catch (RecognitionException re) {
      reportError(re);
      recover(input, re);
      retval.tree = (Object) adaptor.errorNode(
          input,
          retval.start,
          input.LT(-1),
          re);

    } finally {
      if (state.backtracking > 0) {
        memoize(input, 64, action_StartIndex);
      }
    }
    return retval;
  }