| program | ::= | chans | : | chandec list |
| procs | : | process list | ||
| process | ::= | vars | : | vardec list |
| body | : | transition list | ||
| transition | ::= | source | : | astate |
| target | : | astate | ||
| lab | : | label | ||
| label | ::= | guard | : | expr |
| act | : | action | ||
| action | ::= | tau | ||
| | | input_action | |||
| | | output_action | |||
| | | assign_action | |||
| astate | ::= | initstate | ||
| | | state | |||
| state | ::= | name | : | string |
| assert | : | expr | ||
| initstate | ::= | name | : | string |
| assert | : | expr | ||
| expr | ::= | b_expr | ||
| | | u_expr | |||
| | | constval | |||
| | | variable | |||
| b_expr | : | left_expr | : | expr |
| right_expr | : | expr | ||
| op | : | operand | ||
| u_expr | : | sub_expr | : | expr |
| op | : | operand | ||
| operand | ::= | PLUS |MINUS |TIMES |DIV | (Operand als Konstanten in expr) | |
| | | AND |OR |NEG | |||
| | | LESS |GREATER |LEQ |GEQ | |||
| input_action | ::= | chan | : | channel |
| var | : | variable | ||
| | | ||||
| output_action | ::= | chan | : | channel |
| val | : | expr | ||
| assign_action | ::= | var | : | variable |
| | | val | : | expr | |
| vardec | ::= | var | : | variable |
| chandec | ::= | chan | : | channel |
| variable | ::= | name | : | string |
| channel | ::= | name | : | string |
| constval | ::= | val | : | Object |