Grammars

Grammars used by the Lark parser to parse Propositional Logic, LTL_f and PLTL_f.

Propositional Logic

pl.lark

start: propositional_formula

?propositional_formula: prop_equivalence
?prop_equivalence: prop_implication (EQUIVALENCE prop_implication)*
?prop_implication: prop_or (IMPLY prop_or)*
?prop_or: prop_and (OR prop_and)*
?prop_and: prop_not (AND prop_not)*
?prop_not: NOT* prop_wrapped
?prop_wrapped: prop_atom
            | LSEPARATOR propositional_formula RSEPARATOR
?prop_atom: atom
         | prop_true
         | prop_false

atom: SYMBOL_NAME
prop_true: TRUE
prop_false: FALSE

LSEPARATOR: "("
RSEPARATOR: ")"
EQUIVALENCE: "<->" | "<=>"
IMPLY: "->" | "=>"
OR: "||" | "|"
AND: "&&" | "&"
NOT: "!" | "~"
SYMBOL_NAME: /(\w+)|(".*")/
TRUE.2: /(?i:true)/
FALSE.2: /(?i:false)/

%ignore /\s+/

LTL_f

ltlf.lark

start: ltlf_formula

?ltlf_formula:     ltlf_equivalence
?ltlf_equivalence: ltlf_implication (EQUIVALENCE ltlf_implication)*
?ltlf_implication: ltlf_or (IMPLY ltlf_or)*
?ltlf_or:          ltlf_and (OR ltlf_and)*
?ltlf_and:         ltlf_until (AND ltlf_until)*
?ltlf_until:       ltlf_release (UNTIL ltlf_release)*
?ltlf_release:     ltlf_unaryop (RELEASE ltlf_unaryop)*

?ltlf_unaryop:     ltlf_always
             |     ltlf_eventually
             |     ltlf_next
             |     ltlf_weak_next
             |     ltlf_not
             |     ltlf_wrapped

?ltlf_always:      ALWAYS ltlf_unaryop
?ltlf_eventually:  EVENTUALLY ltlf_unaryop
?ltlf_next:        NEXT ltlf_unaryop
?ltlf_weak_next:   WEAK_NEXT ltlf_unaryop
?ltlf_not:         NOT ltlf_unaryop
?ltlf_wrapped:     ltlf_atom
             |     LSEPARATOR ltlf_formula RSEPARATOR
?ltlf_atom:        ltlf_symbol
          |        ltlf_true
          |        ltlf_false
          |        ltlf_last

ltlf_symbol: SYMBOL_NAME
ltlf_true: prop_true
ltlf_false: prop_false
ltlf_last: LAST

// Operators must not be part of a word
UNTIL.2: /U(?=[^a-z]|$)/
RELEASE.2: /R(?=[^a-z]|$)/
ALWAYS.2: /G(?=[^a-z]|$)/
EVENTUALLY.2: /F(?=[^a-z]|$)/
NEXT.2: /X(?=[^a-z]|$)/
WEAK_NEXT.2: /WX(?=[^a-z]|$)/
LAST.2: /(?i:last)/

// Symbols cannot contain uppercase letters, because these are reserved
SYMBOL_NAME: /[a-z][a-z0-9_]*/

%ignore /\s+/

%import .pl.prop_true -> prop_true
%import .pl.prop_false -> prop_false
%import .pl.NOT -> NOT
%import .pl.OR -> OR
%import .pl.AND -> AND
%import .pl.EQUIVALENCE -> EQUIVALENCE
%import .pl.IMPLY -> IMPLY
%import .pl.LSEPARATOR -> LSEPARATOR
%import .pl.RSEPARATOR -> RSEPARATOR

PLTL_f

pltlf.lark

start: pltlf_formula

?pltlf_formula:     pltlf_equivalence
?pltlf_equivalence: pltlf_implication (EQUIVALENCE pltlf_implication)*
?pltlf_implication: pltlf_or (IMPLY pltlf_or)*
?pltlf_or:          pltlf_and (OR pltlf_and)*
?pltlf_and:         pltlf_since (AND pltlf_since)*
?pltlf_since:       pltlf_unaryop (SINCE pltlf_unaryop)*

?pltlf_unaryop:    pltlf_historically
             |     pltlf_once
             |     pltlf_before
             |     pltlf_not
             |     pltlf_wrapped

?pltlf_historically: HISTORICALLY pltlf_unaryop
?pltlf_once:         ONCE pltlf_unaryop
?pltlf_before:       BEFORE pltlf_unaryop
?pltlf_not:          NOT pltlf_unaryop
?pltlf_wrapped:      pltlf_atom
             |       LSEPARATOR pltlf_formula RSEPARATOR
?pltlf_atom:       pltlf_symbol
           |       pltlf_true
           |       pltlf_false
           |       pltlf_start

pltlf_symbol: SYMBOL_NAME
pltlf_true: prop_true
pltlf_false: prop_false
pltlf_start: START

// Operators must not be part of a word
SINCE.2: /S(?=[^a-z]|$)/
HISTORICALLY.2: /H(?=[^a-z]|$)/
ONCE.2: /O(?=[^a-z]|$)/
BEFORE.2: /Y(?=[^a-z]|$)/
START.2: /(?i:start)/

// Symbols cannot contain uppercase letters, because these are reserved
SYMBOL_NAME: /[a-z][a-z0-9_]*/

%ignore /\s+/

%import .pl.prop_true -> prop_true
%import .pl.prop_false -> prop_false
%import .pl.NOT -> NOT
%import .pl.OR -> OR
%import .pl.AND -> AND
%import .pl.EQUIVALENCE -> EQUIVALENCE
%import .pl.IMPLY -> IMPLY
%import .pl.LSEPARATOR -> LSEPARATOR
%import .pl.RSEPARATOR -> RSEPARATOR