Pattern Queries Grammar, defined with ANTLR (ANother Tool for Language Recognition).

 

 

grammar PQuery;

 

pQuery

:

       (

              inequalityQuery

              | questionMark

       )*

;

 

inequalityQuery

:

       (

              WITH_PROBABILITY probability

       )? query

;

 

WITH_PROBABILITY

:

       'with probability'

       | 'WITH PROBABILITY'

;

 

questionMark

:

       WHAT_PROBABILITY query

;

 

WHAT_PROBABILITY

:

       'what is the probability of'

       | 'WHAT IS THE PROBABILITY OF'

       | '=?'

;

 

query

:

       unaryPattern

       | binaryPattern

;

 

unaryPattern

:

       notPattern

       | eventually

       | always

       | next

       | never

       | infinitelyOften

       | steadyState

;

 

binaryPattern

:

       until

       | weakUntil

       | release

       | follows

       | precedes

;

 

//!(query)

notPattern

:

       NOT query

       | NOT '(' query ')'

;

 

eventually

:

       EVENTUALLY expr

;

 

EVENTUALLY

:

       'eventually'

       | 'EVENTUALLY'

;

 

always

:

       ALWAYS expr

;

 

ALWAYS

:

       'always'

       | 'ALWAYS'

;

 

next

:

       NEXT expr

;

 

NEXT

:

       'next'

       | 'NEXT'

;

 

never

:

       NEVER expr

;

 

NEVER

:

       'never'

       | 'NEVER'

;

 

infinitelyOften

:

       INFINITELY_OFTEN expr

;

 

INFINITELY_OFTEN

:

       'infinitely-often'

       | 'INFINITELY-OFTEN'

;

 

steadyState

:

       STEADY_STATE expr

;

 

STEADY_STATE

:

       'steady-state'

       | 'STEADY-STATE'

;

 

until

:

       expr UNTIL expr

;

 

UNTIL

:

       'until'

       | 'UNTIL'

;

 

//(a W b) equivalent to !(!b U !(a | b)) equivalent to (b R (a | b))

weakUntil

:

       expr WEAK_UNTIL expr

;

 

WEAK_UNTIL

:

       'weak-until'

       | 'WEAK-UNTIL'

;

 

//(a R b), is equivalent to !(!a U !b) also equivalent to P_{!<>(1-p)}[!a U !b]

release

:

       expr RELEASE expr

;

 

RELEASE

:

       'release'

       | 'RELEASE'

;

 

follows

:

       expr FOLLOWS expr

;

 

FOLLOWS

:

       'follows'

       | 'FOLLOWS'

;

 

//e.g., a PRECEDES b is equivalent to (!b W a)

//which is also equivalent to  P_{!<>(1-p)}[b U (!a & b)]

precedes

:

       expr PRECEDES expr

;

 

PRECEDES

:

       'precedes'

       | 'PRECEDES'

;

 

expr

:

       NOT expr # notExpr

       | expr operator =

       (

              AND

              | OR

              | IMPLIES

       ) expr # binaryLogicalExpr

       | boolExpr # noParanBoolExpr

       | '(' expr ')' # paranthesesExpr

;

 

boolExpr

:

       logicalEntity

       | numericExp RELATION numericExp

       | '(' boolExpr ')'

;

 

logicalConstant

:

       TRUE

       | FALSE

;

 

FALSE

:

       'false'

       | 'FALSE'

;

 

TRUE

:

       'true'

       | 'TRUE'

;

 

logicalEntity

:

       logicalConstant

       | IDENTIFIER //boolean variable

 

;

 

NOT

:

       'NOT'

       | 'not'

       | '!'

;

 

IMPLIES

:

       'implies'

       | 'IMPLIES'

;

 

OR

:

       'or'

       | 'OR'

;

 

AND

:

       'and'

       | 'AND'

;

 

probability

:

       RELATION numericExp

;

 

RELATION

:

       '>='

       | '<='

       | '>'

       | '<'

       | '='

       | '!='

;

 

numericExp

:

       numericExp op =

       (

              '*'

              | '/'

              | '%'

       ) numericExp # multNumericExpr

       | numericExp op =

       (

              '+'

              | '-'

       ) numericExp # addNumericExpr

       | numeric # noOpNumericExpr

       | '(' numericExp ')' # parensNumericExpr

;

 

numeric

:

       IDENTIFIER

       | NUMBER

;

 

IDENTIFIER

:

       [a-zA-Z_] [a-zA-Z_0-9]*

;

 

NUMBER

:

       (

              '-'

       )?

       (

              '0' .. '9'

       )+

       (

              '.'

              (

                     '0' .. '9'

              )+

       )?

;

 

MUL

:

       '*'

;

 

DIV

:

       '/'

;

 

MOD

:

       '%'

;

 

ADD

:

       '+'

;

 

SUB

:

       '-'

;

 

MULTILINECOMMENT

:

       '/*' .*? '*/' -> skip

;

 

LINECOMMENT

:

       '//' .+?

       (

              '\n'

              | EOF

       ) -> skip

;

 

WS

:

       [ \r\t\u000C\n]+ -> skip

;