antlr gated predicate

Question

This is a follow-up question from Antlr superfluous Predicate required? where I stated my problem in a simplified way, however it could not be solved there.
I have the following grammar and when I delete the {true}?=> predicates, the text is not recognized anymore. The input string is MODULE main LTLSPEC H {} {} {o} FALSE;. Note that the trailing ; is not tokenized as EOC, but as IGNORE. When I add {true}?=> to the EOC rule ; is tokenized as EOC.
I tried this from command-line with antlr-v3.3 and v3.4 without difference. Thanks in advance, I appreciate your help.

grammar NusmvInput;

options {
  language = Java;
}    
@parser::members{
public static void main(String[] args) throws Exception {
    NusmvInputLexer lexer = new NusmvInputLexer(new ANTLRStringStream("MODULE main LTLSPEC H {} {} {o} FALSE;"));
    NusmvInputParser parser = new NusmvInputParser(new CommonTokenStream(lexer));
    parser.specification();
  }
}    
@lexer::members{
    private boolean inLTL = false;
} 

specification : 
     module+ EOF
     ;
module : 
    MODULE module_decl    
    ;

module_decl : 
    NAME parameter_list ;
parameter_list 
    : ( LP (parameter ( COMMA parameter )*)? RP )?
    ;    
parameter
    : (NAME | INTEGER )
    ;    
/**************
*** LEXER
**************/
COMMA
    :{!inLTL}?=> ','
    ; 
OTHER 
    : {!inLTL}?=>( '&' | '|' | 'xor' | 'xnor' | '=' | '!' |
     '<' | '>' | '-' | '+' | '*' | '/' |
      'mod' | '[' | ']' | '?')
      ;     
RCP
      : {!inLTL}?=>'}'
      ;      
LCP
      : {!inLTL}?=>'{'
      ;
LP 
    : {!inLTL}?=>'('
    ;
RP 
    : {!inLTL}?=>')'
    ;   
MODULE
    : {true}?=> 'MODULE' {inLTL = false;}
    ;
LTLSPEC
    : {true}?=> 'LTLSPEC' 
    {inLTL = true; skip(); }
    ;  
EOC 
    : ';' 
    {
        if (inLTL){
            inLTL = false;
            skip();
        }
    }
    ;   
WS 
    : (' ' | '\t' | '\n' | '\r')+ {$channel = HIDDEN;} 
    ;
COMMENT 
    :  '--' .* ('\n' | '\r') {$channel = HIDDEN;} 
    ; 
INTEGER 
    : {!inLTL}?=> ('0'..'9')+
    ;
NAME 
    :{!inLTL}?=> ('A'..'Z' | 'a'..'z') ('a'..'z' | 'A'..'Z' | '0'..'9' | '_' | '$' | '#' | '-')*
    ;
IGNORE
    : {inLTL}?=> . {skip();}
    ;

Just glancing over your grammar, I already see 2 errors: a `^` in the `module` rule while there's no `output=AST` present in the options, and the `specification` rule ends with a `-` (minus) sign. — Bart Kiers, Jul 10 '12 at 14:03
Sorry for that. I removed the tree-rewritting after copying the code into stackoverflow, and forgot those. — Heinrich Ody, Jul 10 '12 at 14:16

score 1 · Accepted Answer · answered Jul 10 '12 at 15:59

It seems that without a predicate before MODULE and LTLSPEC, the NAME gets precedence over them even if these tokens are defined before the NAME token. Whether this is by design or a bug, I don't know.

However, the way you're trying to solve it seems rather complicated. As far as I can see, you seem to want to ignore (or skip) input starting with LTLSPEC and ending with a semi colon. Why not do something like this instead:

specification  : module+ EOF;
module         : MODULE module_decl;
module_decl    : NAME parameter_list;
parameter_list : (LP (parameter ( COMMA parameter )*)? RP)?;    
parameter      : (NAME | INTEGER);    

MODULE  : 'MODULE';
LTLSPEC : 'LTLSPEC' ~';'* ';' {skip();};
COMMA   : ','; 
OTHER   : ( '&' | '|' | 'xor' | 'xnor' | '=' | '!' |
            '<' | '>' | '-' | '+' | '*' | '/' |
           'mod' | '[' | ']' | '?')
        ;     
RCP     : '}';      
LCP     : '{';
LP      : '(';
RP      : ')';   
EOC     : ';';   
WS      : (' ' | '\t' | '\n' | '\r')+ {$channel = HIDDEN;};
COMMENT : '--' .* ('\n' | '\r') {$channel = HIDDEN;}; 
INTEGER : ('0'..'9')+;
NAME    : ('A'..'Z' | 'a'..'z') ('a'..'z' | 'A'..'Z' | '0'..'9' | '_' | '$' | '#' | '-')*;

You cannot see it from this example, but `LTLSPEC` _may_ be finished by `;`. It could also be finished by `MODULE`, or by another `LTLSPEC`. When I try something like `(~(MODULE | LTLSPEC))*` it strangely does not work, don't remember the error right now though. — Heinrich Ody, Jul 11 '12 at 07:52
I think I can basically take your suggestion if I add before anything that finishes the `LTLSPEC`-part a artificial `END`-token and then: `LTLSPEC : 'LTLSPEC' ~END* {skip();};` — Heinrich Ody, Jul 11 '12 at 08:02
@HeinrichOdy, beware that the negation, `~`, only works on single chars! (or rules that match a single char). See this Q&A: http://stackoverflow.com/questions/8284919/negating-inside-lexer-and-parser-rules — Bart Kiers, Jul 11 '12 at 08:23

antlr gated predicate

1 Answers1