BNF for SpecParse.jj

NON-TERMINALS

Ltl	::=	LtlUntil ( "." )?
LtlUntil	::=	LtlWhile ( "U" LtlWhile )*
LtlWhile	::=	LtlImplied ( "W" LtlImplied )*
LtlImplied	::=	LtlOr ( "<=" LtlOr )?
LtlOr	::=	LtlAnd ( "\\/" LtlAnd )*
LtlAnd	::=	LtlMonadic ( "/\\" LtlMonadic )*
LtlMonop	::=	( "[]" \| "G" )
	\|	( "<>" \| "F" )
LtlMonadic	::=	"(" LtlUntil ")"
	\|	LtlMonop LtlMonadic
	\|	"O" LtlMonadic
	\|	( "!" \| "~" \| "\u00ac" ) LtlMonadic
	\|	TlProp
CtlStarSpec	::=	CtlSpec ( "." )?
CtlSpec	::=	CtlComplexSpec
	\|	CtlSimpleSpec
CtlComplexSpec	::=	"X" CtlSpec
	\|	CtlUntilRelease CtlSpecPair
	\|	CtlSometimeAlways CtlSpec
	\|	CtlPathQuant CtlQuantified
CtlUQuant	::=	"X" CtlSpec
	\|	CtlSometimeAlways CtlSpec
CtlXQuant	::=	CtlPrefix CtlSpec
	\|	CtlSpec
CtlFGQuant	::=	CtlPrefix CtlSpec
	\|	CtlSpec
CtlQuantified	::=	CtlUNum CtlUQuant
	\|	"X" CtlXQuant
	\|	CtlUntilRelease CtlSpecPair
	\|	CtlSometimeAlways CtlFGQuant
	\|	CtlSimpleSpec
CtlSimpleSpec	::=	"(" CtlSpec ")"
	\|	"~" TlProp
	\|	TlProp
	\|	"t"
	\|	"f"
	\|	CtlBoolConnect CtlSpecPair
CtlSpecPair	::=	"(" CtlSpec "," CtlSpec ")"
CtlPrefix	::=	"_" "{" TlProp "}" "_"
CtlSometimeAlways	::=	"F"
	\|	"G"
CtlUntilRelease	::=	"U"
	\|	"V"
CtlBoolConnect	::=	"&"
	\|	"\|"
CtlPathQuant	::=	"A"
	\|	"E"
CtlUNum	::=	"_" TlProp "_"
TlProp	::=	( "p" )? <NUMBER>