grammar mccproperty;



ID:
  ('a'..'z'|'A'..'Z'|'0'..'9'|'_')+;


EOL:
  ('\r' | '\n')+;

S : ('\s' | ' ')+ ;

identifier: ID;

property_set: property+;

comparer : '=' | '!=' | '<' | '<=' | '>' | '>=';
mop : '&' | '|';
operator : 'I' | 'N' | 'A' | 'E' | 'G' | 'F';
ifs : '=>' | '<=>';
x : 'X';
xor : 'xor';
space: S? ;
not : '!';
untils : 'U' | 'W';
//integer : ('0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9')+  | DIGIT+;
fragment DIGIT : [0-9] ;
integer : DIGIT+ ;


property:
  ( 'reach' | 'struct' | 'ctl' | 'ltl' )? space identifier space ':' space complex_formula space EOL
  ;

simple_formula: space (
    'true'
  | 'false'
  | '(' complex_formula ')'
  | not simple_formula
  | x integer? '~'? simple_formula
  | operator simple_formula
  | 'deadlock'
  | identifier '?' ('l0' | 'l1' | 'l2' | 'l3' | 'l4')?
 | complex_expression  comparer  complex_expression
  ) space;

complex_formula:
 simple_formula  (
							   (mop  simple_formula)+
                                                         | (xor   simple_formula)
                                                         | (ifs simple_formula)
                                                         | (untils   simple_formula)
                                                         )?
  ;


complex_expression:
	simple_expression
	( ('+' simple_expression)+
    | ('*' simple_expression)+
    | ('-' simple_expression)
    | ('/' simple_expression)
    space )?
        ;

simple_expression:

    (integer)+
  | 'bound' '(' identifier ')'
  | '|' complex_expression '|'
  | '<' anonymous_bindings '>'
  | 'marking' '(' identifier ')'
  | '(' complex_expression ')'
  ;

anonymous_bindings:
    ( identifier (',' identifier)* )?;