EBNF for ATL and LCGS

Below is the grammar of LCGS programs in extended Backus–Naur form.

start := (constdecl semicolon | simpledecl semicolon | moduledecl)*

simpledecl := labeldecl
    | vardecl
    | playerdecl
    | statevarchangedecl
    | transitondecl

constdecl := "const" identifier eq expr;
labeldecl := "label" identifier eq expr
playerdecl := "player" identifier eq identifier relabeling?

templatedecl := "template" identifier (simpledecl semicolon)* "endtemplate"

vardecl := identifier colon type "init" expr

transitiondecl := lbrac identifier rbrac expr

statevarchangedecl := identifier prime eq expr

relabeling := lbrac (identifier eq identifier (comma identifier eq identifier)*)? rbrac

type := lbrac expr rangedots expr rbrac

param := lbrac identifier colon type (comma identifier colon type)* rbrac

expr := identifier
    | identifier dot identifier
    | int
    | not expr
    | expr binop expr
    | expr questionmark expr colon expr
    | lpar expr rpar
    | "max" lpar expr (comma expr)* rpar
    | "min" lpar expr (comma expr)* rpar
	...

comma := ","
dot := "."
semicolon := ";"
colon := ":"
assign := "="

binop := and | or | xor | implies | eq | neq | gt | lt | geq | leq | plus | minus | mult | fdiv
not := "!"
eq := "=="
neq := "!="
gt := ">"
lt := "<"
geq := ">="
leq := "<="
and := "&&"
or := "||"
xor := "^"
implies := "->"
questionmark := "?"
plus := "+"
minus := "-"
mult := "*"
fdiv := "/"

lpar := "("
rpar := ")"
lbrac := "["
rbrac := "]"
quote := "\""
prime := "'"
rangedots := ".."

identifier = [a-zA-Z] ([_a-zA-Z0-9])*
int := [1-9] [0-9]* | [0-9] // 0 interpreted as false, all other is true

Below is the grammar for ATL formula in extended Backus–Naur form.

start := phi

phi := paren |
        proposition |
        not |
        or |
        and |
        bool |
        coallition temporal_phi

paren := "(" phi ")"

coallition := "<<" players ">>" | "[[" players "]]"

temporal_phi := next | until | eventually | invariant

next := "X" phi
until := "(" phi "U" phi ")"
eventually := "F" phi
invariant := "G" phi

enforce_next := enforce_players next
enforce_until := enforce_players until
enforce_eventually := enforce_players eventually
enforce_invariant := enforce_players invariant

despite_next := despite_players next
despite_until := despite_players until
despite_eventually := despite_players eventually
despite_invariant := despite_players invariant

proposition := identifier
not := "!" phi
or := phi "|" phi
and := phi "&" phi

bool := "true" | "false"
players := identifier | identifier "," players
identifier := [a-zA-Z0-9]+