START = ctl_formula ';' ctl_formula = ap | '(' ctl_formula ')' | unop ctl_formula | ctl_formula binop ctl_formula | ae '(' ctl_formula 'U' ctl_formula ')' | untemp ctl_formula unop = '!' | '~' binop = '&' | '|' | '->' | '<-' | '<->' ae = 'A' | 'E' untemp = 'AX' | 'EX' | 'AF' | 'EF' | 'AG' | 'EG' ap = PLACE cmp INT | 'true' | 'false' cmp = '==' | '!='| '>=' | '>' | '<=' | '<' /* Comments: PLACE is a name of a place It is possible to specify several CTL formulas in one file. */