assertion

            : '#' 'assert' definitionRef           

            (

                        ( '|=' ( '(' | ')' | '[]' | '<>' | (ID - 'X') | STRING | '!' | '?' | '&&' | '||' | '->' | '<->' | '/\\' | '\\/' | '.' | INT )+ ) // 'X' is not allowed in LTL

                                    |  'deadlockfree' 

                                    |  'deterministic'

                                    |  'nonterminating'

                                    |  'reaches' ID withClause?

                                    |  'refines' definitionRef

                                    |  'refines' '<F>' definitionRef

                                    |  'refines' '<FD>' definitionRef

                             |  'refines' '<T>' definitionRef   //timed refinement

            )

            ';'

            ;

//process definitions

definition

            : ID ('(' (ID (',' ID )*)? ')')? '=' interleaveExpr ';'

            ;          

interleaveExpr

            : parallelExpr ('|||' parallelExpr)*                       

            | '|||' (paralDef (';' paralDef )*) '@' interleaveExpr

            ;

parallelExpr

            : internalChoiceExpr ('||' internalChoiceExpr)*

            | '||' (paralDef (';' paralDef )*) '@' interleaveExpr

            ;

paralDef

            : ID ':' '{' additiveExpression (',' additiveExpression)*  '}'

            | ID ':' '{' additiveExpression '..' additiveExpression  '}'

            ;          

paralDef2                    

            : '{' '..' '}'

            | '{' additiveExpression '}'

            ;

internalChoiceExpr

            : externalChoiceExpr ('<>' externalChoiceExpr)*

            | '<>' (paralDef (';' paralDef )*) '@' interleaveExpr

            ;

externalChoiceExpr

            : interruptExpr ('[]' interruptExpr)*

            | '[]' (paralDef (';' paralDef )*) '@' interleaveExpr

            ;

interruptExpr

            : hidingExpr ('interrupt' ('['expression']')? hidingExpr)*  //if there is a time expression, it is a timed interrupt

            ;

hidingExpr

            : sequentialExpr ('\' '{' eventName  (',' eventName )* '}')?

            ;

sequentialExpr

            : guardExpr (';' guardExpr)*

            ;

guardExpr

            : timeoutExpr

            | '[' conditionalOrExpression ']' timeoutExpr

            ;

timeoutExpr
          : withinExpr ('timeout'^ '['! expression ']'! withinExpr)*  
          ;
 

withinExpr 
          : deadlineExpr
          |  deadlineExpr 'within' '[' expression (',' expression)? ']'
          ;

deadlineExpr
          : waituntilExpr 'deadline' '[' expression ']' 

     | waituntilExpr 
          ; 

waituntilExpr
          : channelExpr 'waituntil' '[' expression ']' 

     | channelExpr 
          ;

channelExpr

             : ID '!' expression ('.' expression)*  ('->'|'->>') eventExpr

             | ID '?' ('[' conditionalOrExpression ']')? expression ('.' expression)*  ('->'|'->>') eventExpr  //here expression is either a single variable or expression that has no global variables. Optional conditionalOrExpression is the guard condition that stop the channel input event if the condition is false. 

             | eventExpr

             ;

eventExpr

             : eventM (block)? ('->'|'->>') eventExpr //->> means urgent event, which takes no time.

             | block ('->'|'->>') eventExpr //un-labeled program, which is same as: tau block '->' eventExpr

             | caseExpr

             ;

caseExpr: 'case'

              '{'

                        caseCondition+

                        ('default' ':' elsec=interleaveExpr)?

               '}'

            | ifExpr

            ;

caseCondition

            : (conditionalOrExpression ':' interleaveExpr)

            ;

ifExpr  :  atomicIfExpr  

            | ifExprs

            ;

ifExprs

            : 'if' '(' conditionalOrExpression ')' '{' interleaveExpr  '}' ('else' ifBlock )? 

            | 'ifa' '(' conditionalOrExpression ')' '{' interleaveExpr  '}' ('else' ifBlock )? 

            | 'ifb' '(' conditionalOrExpression ')' '{' interleaveExpr  '}'  

            ;

ifBlock

            : ifExprs

            | '{' interleaveExpr '}'

            ;

atomicExpr  

            : atom 

            | 'atomic' '{' interleaveExpr  '}'

            ;

atom   :   ID  ('(' (expression (',' expression )*)?  ')')?

            |   'Skip' ('(' ')')?

            |   'Stop' ('(' ')')?

            |   'Wait' '[' expression (',' expression)? ']'  

            |   '(' interleaveExpr ')'

            ;        

eventM

            :  eventName

            ;          

eventName

            : ID ( '.' additiveExpression)*

            ;