2 files changed, 43 insertions, 0 deletions

diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
new file mode 100644
index 0000000..27f1bca
--- /dev/null
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -0,0 +1,13 @@
+lexer grammar PropertyLexer;
+
+TAG_EXISTING_KW: '(tag_existing';
+AND_OPERATOR_KW: '(and';
+OR_OPERATOR_KW: '(or';
+NOT_OPERATOR_KW: '(not';
+EXISTS_OPERATOR_KW: '(exists';
+FORALL_OPERATOR_KW: '(forall';
+ID: [a-zA-Z0-9_]+;
+L_PAREN : '(';
+R_PAREN : ')';
+
+WS: [ \t\r\n]+ -> skip;
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;