instr-to-kodkod/parser/PropertyParser.g4


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

parser grammar PropertyParser;
options { tokenVocab = PropertyLexer; }

prog: tag_existing;

tag_existing
   : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN formula R_PAREN
;

tag_item
   : L_PAREN ID ID R_PAREN
;

formula
   : and_operator
   | or_operator
   | not_operator
   | exists_operator
   | forall_operator
   | predicate
;

and_operator: AND_OPERATOR_KW formula (formula)+ R_PAREN;
or_operator: OR_OPERATOR_KW formula (formula)+ R_PAREN;
not_operator: NOT_OPERATOR_KW formula R_PAREN;
exists_operator: EXISTS_OPERATOR_KW ID ID formula R_PAREN;
forall_operator: FORALL_OPERATOR_KW ID ID formula R_PAREN;


predicate: L_PAREN ID (ID)* R_PAREN;