| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/parser/PropertyParser.g4')
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 new file mode 100644 index 0000000..740b308 --- /dev/null +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -0,0 +1,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; |