First shot at a grammar for the properties.

1 files changed, 70 insertions, 15 deletions

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
+;