Letter = 'a' .. 'z' | 'A' .. 'Z'
Digit = '0' .. '9'
Ident = Letter { Letter | Digit }
Var = Ident | '_'
Numeral = [ '-' ] ( Digit | Numeral Digit )
Bool = 'true' | 'false'

Aop = '+' | '-' | '*' | '/' | '%'                                                   (* arithmetic operation *)
Aexp = Aterm { Aop Term }                                                           (* arithmetic expression *)
Aterm
    = Ident                                                                         (* variable *)
    | Numeral                                                                       (* value *)
    | 'time' Stm                                                                    (* time statement *)
    | '(' Aexp ')'                                                                  (* parenthesized expression *)

Rop = '=' | '#' | '<' | '<=' | '>' | '>='                                           (* relation operation *)
Bop = 'and' | 'or'                                                                  (* boolean operation *)
Bexp = Bterm { Bop Bterm }                                                          (* boolean expression *)
Bterm
    = Bool                                                                          (* value *)
    | 'not' Bexp                                                                    (* negation *)
    | Aexp Rop Aexp                                                                 (* relation *)
    | '(' Bexp ')'                                                                  (* parenthesized expression *)

Dop = ':=' | '+=' | '-=' | '*=' | '/=' | '%='                                       (* definition operator *)
Stm
    = 'skip'                                                                        (* no-op *)
    | Var Dop Aexp                                                                  (* variable definition *)
    | Stm ';' Stm                                                                   (* sequence *)
    | 'if' Bexp 'then' Stm 'else' Stm 'end'                                         (* conditional *)
    | 'while' Bexp 'do' Stm 'end'                                                   (* iteration *)
    | 'print' Aexp                                                                  (* print arithmetic expression *)
    | 'read' Var                                                                    (* read input into variable *)
    | 'var' Var Dop Aexp 'in' Stm 'end'                                             (* local variable definition *)
    | Stm 'par' Stm                                                                 (* parallelization *)
    | Stm '[]' Stm                                                                  (* non-determinism *)
    | 'procedure' Ident '(' Params ';' Rets ')' 'begin' Stm 'end'                   (* procedure definition *)
    | Ident '(' Args ';' Rets ')'                                                   (* procedure invocation *)
    | 'break'                                                                       (* break flag *)
    | 'revert' Stm 'if' Bexp                                                        (* conditional revert *)
    | 'match' Aexp 'on' { Numeral ':' Stm ',' } 'default:' Stm                      (* pattern match *)
    | 'havoc' x                                                                     (* random variable definition *)
    | 'assert' Bexp                                                                 (* assertion *)
    | 'flip' '(' Numeral ')' Stm 'flop' Stm 'end'                                   (* alternating branching *)
    | 'raise' Aexp                                                                  (* raise exception *)
    | 'try' Stm 'catch' Ident 'with' Stm 'end'                                      (* try catch block *)
    | '(' Stm ')'                                                                   (* parenthesized statement *)

Args = [ Aexp { ',' Aexp } ]                                                        (* zero or more comma separated Aexp *)
Params = [ Ident { ',' Ident } ]                                                    (* '' .. Ident *)
Rets = [ Var { ',' Var } ]                                                          (* '' .. Var *)