First shot at a grammar for the properties.

2 files changed, 96 insertions, 23 deletions

diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 27f1bca..159dec1 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -1,13 +1,31 @@
 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_]+;
+fragment SEP: [ \t\r\n]+;
+
 L_PAREN : '(';
 R_PAREN : ')';
 
-WS: [ \t\r\n]+ -> skip;
+TAG_EXISTING_KW: '(tag_existing' SEP;
+
+AND_OPERATOR_KW: '(and' SEP;
+OR_OPERATOR_KW: '(or' SEP;
+NOT_OPERATOR_KW: '(not' SEP ;
+IMPLIES_OPERATOR_KW: '(implies' SEP ;
+
+EXISTS_OPERATOR_KW: '(exists' SEP;
+FORALL_OPERATOR_KW: '(forall' SEP;
+
+CTL_VERIFIES_OPERATOR_KW: '(CTL_verifies' SEP;
+
+AX_OPERATOR_KW: '(AX' SEP;
+EX_OPERATOR_KW: '(EX' SEP;
+AG_OPERATOR_KW: '(AG' SEP;
+EG_OPERATOR_KW: '(EG' SEP;
+AF_OPERATOR_KW: '(AF' SEP;
+EF_OPERATOR_KW: '(EF' SEP;
+AU_OPERATOR_KW: '(AU' SEP;
+EU_OPERATOR_KW: '(EU' SEP;
+
+WS: SEP;
+
+ID: [a-zA-Z0-9_]+;
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 740b308..1b32722 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -4,27 +4,82 @@ options { tokenVocab = PropertyLexer; }
 prog: tag_existing;
 
 tag_existing
-   : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN formula R_PAREN
+   : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN (WS)* sl_formula (WS)* R_PAREN
 ;
 
 tag_item
-   : L_PAREN ID ID R_PAREN
+   : (WS)* L_PAREN (WS)* ID (WS)+ ID (WS)+ ID (WS)* R_PAREN (WS)*
 ;
 
-formula
-   : and_operator
-   | or_operator
-   | not_operator
-   | exists_operator
-   | forall_operator
-   | predicate
+predicate: (WS)* L_PAREN ID ((WS)+ ID)* (WS)* R_PAREN;
+
+/******************************************************************************/
+/** Structural Level **********************************************************/
+/******************************************************************************/
+/**** First Order Expressions *************************************************/
+sl_and_operator: (WS)* AND_OPERATOR_KW sl_formula (sl_formula)+ (WS)* R_PAREN;
+sl_or_operator: (WS)* OR_OPERATOR_KW sl_formula (sl_formula)+ (WS)* R_PAREN;
+sl_not_operator: (WS)* NOT_OPERATOR_KW sl_formula (WS)* R_PAREN;
+sl_implies_operator: (WS)* IMPLIES_OPERATOR_KW sl_formula sl_formula (WS)* R_PAREN;
+
+/** Quantified Expressions ****************************************************/
+sl_exists_operator:
+   (WS)* EXISTS_OPERATOR_KW ID (WS)+ ID sl_formula (WS*) R_PAREN
 ;
 
-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;
+sl_forall_operator:
+   (WS)* FORALL_OPERATOR_KW ID (WS)+ ID sl_formula (WS*) R_PAREN
+;
 
+/** Special Expressions *******************************************************/
+sl_ctl_verifies_operator:
+   (WS)* CTL_VERIFIES_OPERATOR_KW ID (WS)* bl_formula (WS)* R_PAREN
+;
 
-predicate: L_PAREN ID (ID)* R_PAREN;
+/**** Formula Definition ******************************************************/
+sl_formula:
+   predicate
+   | sl_and_operator
+   | sl_or_operator
+   | sl_not_operator
+   | sl_implies_operator
+   | sl_exists_operator
+   | sl_forall_operator
+   | sl_ctl_verifies_operator
+;
+
+/******************************************************************************/
+/** Behavioral Level **********************************************************/
+/******************************************************************************/
+/**** First Order Expressions *************************************************/
+bl_and_operator: (WS)* AND_OPERATOR_KW bl_formula (bl_formula)+ (WS)* R_PAREN;
+bl_or_operator: (WS)* OR_OPERATOR_KW bl_formula (bl_formula)+ (WS)* R_PAREN;
+bl_not_operator: (WS)* NOT_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_implies_operator: (WS)* IMPLIES_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
+
+/**** Computation Tree Logic Expressions **************************************/
+bl_ax_operator: (WS)* AX_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_ex_operator: (WS)* EX_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_ag_operator: (WS)* AG_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_eg_operator: (WS)* EG_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_af_operator: (WS)* AF_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_ef_operator: (WS)* EF_OPERATOR_KW bl_formula (WS)* R_PAREN;
+bl_au_operator: (WS)* AU_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
+bl_eu_operator: (WS)* EU_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
+
+/**** Formula Definition ******************************************************/
+bl_formula:
+   predicate
+   | bl_and_operator
+   | bl_or_operator
+   | bl_not_operator
+   | bl_implies_operator
+   | bl_ax_operator
+   | bl_ex_operator
+   | bl_ag_operator
+   | bl_eg_operator
+   | bl_af_operator
+   | bl_ef_operator
+   | bl_au_operator
+   | bl_eu_operator
+;