Grammars

Here are reported the grammars used by the Lark parser to parse Propositional Logic, LTLf and LDLf.

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+/

LTLf

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_end

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

// 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]|$)/
END.2: /(?i:end)/
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

LDLf

ldlf.lark

start: ldlf_formula

?ldlf_formula:  ldlf_equivalence
?ldlf_equivalence: ldlf_implication (EQUIVALENCE ldlf_implication)*
?ldlf_implication: ldlf_or (IMPLY ldlf_or)*
?ldlf_or: ldlf_and (OR ldlf_and)*
?ldlf_and: ldlf_unaryop (AND ldlf_unaryop)*

?ldlf_unaryop:     ldlf_box
             |     ldlf_diamond
             |     ldlf_not
             |     ldlf_wrapped
?ldlf_box: BOXLSEPARATOR regular_expression BOXRSEPARATOR ldlf_unaryop
?ldlf_diamond: DIAMONDLSEPARATOR regular_expression DIAMONDRSEPARATOR ldlf_unaryop
?ldlf_not: NOT ldlf_unaryop
?ldlf_wrapped:    ldlf_atom
             |    LSEPARATOR ldlf_formula RSEPARATOR
?ldlf_atom:   ldlf_tt
          |   ldlf_ff
          |   ldlf_last
          |   ldlf_end
          |   ldlf_prop_true
          |   ldlf_prop_false
          |   ldlf_prop_atom

ldlf_prop_true: TRUE
ldlf_prop_false: FALSE
ldlf_prop_atom: SYMBOL_NAME

ldlf_tt: TT
ldlf_ff: FF
ldlf_last: LAST
ldlf_end: END

regular_expression: re_union

?re_union:      re_sequence (UNION re_sequence)*
?re_sequence:   re_star (SEQ re_star)*
?re_star:       re_test STAR?
?re_test:       TEST ldlf_formula
        |       re_wrapped
?re_wrapped:    re_propositional
           |    LSEPARATOR regular_expression RSEPARATOR
re_propositional: propositional_formula


BOXLSEPARATOR: "["
BOXRSEPARATOR: "]"
DIAMONDLSEPARATOR: "<"
DIAMONDRSEPARATOR: ">"
UNION: "+"
SEQ: ";"
TEST: "?"
STAR: "*"
TT.2: /(?i:tt)/
FF.2: /(?i:ff)/

%ignore /\s+/

%import .pl.propositional_formula
%import .pl.TRUE -> TRUE
%import .pl.FALSE -> FALSE
%import .pl.SYMBOL_NAME -> SYMBOL_NAME
%import .pl.EQUIVALENCE -> EQUIVALENCE
%import .pl.IMPLY -> IMPLY
%import .pl.OR -> OR
%import .pl.AND -> AND
%import .pl.NOT -> NOT
%import .pl.LSEPARATOR -> LSEPARATOR
%import .pl.RSEPARATOR -> RSEPARATOR
%import .ltlf.LAST -> LAST
%import .ltlf.END -> END