First shot at depths operators.

3 files changed, 162 insertions, 1 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 1b59ccd..705f3e2 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,6 +1,10 @@
 ## Target(s) Configuration #####################################################
 #MODEL_FILES = $(wildcard ../data/instructions/*.mod)
-MODEL_FILES = ../ast-to-instr/structural.mod $(wildcard ../ast-to-instr/cfg_*.mod) $(wildcard ../cfg-to-paths/*.mod)
+MODEL_FILES = \
+	../ast-to-instr/structural.mod \
+	../ast-to-instr/depths.mod \
+	$(wildcard ../ast-to-instr/cfg_*.mod) \
+	$(wildcard ../cfg-to-paths/*.mod)
 MAP_FILES = $(wildcard ../ast-to-instr/*.map)
 LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 #PROPERTY_FILE = ../data/property/unread_waveforms.pro
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 9fcad29..64fccb0 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -28,6 +28,9 @@ EF_OPERATOR_KW: '(EF' SEP;
 AU_OPERATOR_KW: '(AU' SEP;
 EU_OPERATOR_KW: '(EU' SEP;
 
+DEPTH_NO_PARENT_OPERATOR_KW: '(does_not_reach_parent_before' SEP;
+DEPTH_NO_CHANGE_OPERATOR_KW: '(does_not_change_depth_before' 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 29e91d2..5c93eac 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -1028,6 +1028,152 @@ bl_eu_operator [Variable current_node]
    }
 ;
 
+/**** Depth Operators *********************************************************/
+bl_depth_no_parent_operator [Variable current_node]
+   returns [Formula result]
+
+   @init
+   {
+      final Variable node_of_path, node_for_f, chosen_path;
+
+      node_of_path = Main.get_variable_manager().generate_new_variable();
+      node_for_f = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
+   }
+
+   :
+   (WS)* DEPTH_NO_PARENT_OPERATOR_KW
+      bl_formula[node_for_f]
+   (WS)* R_PAREN
+
+   {
+      final Relation depth_relation;
+
+      depth_relation = Main.get_model().get_predicate_as_relation("depth");
+
+      $result =
+         node_of_path.join
+         (
+            depth_relation
+         ).product
+         (
+            node_for_f.join(depth_relation)
+         ).in
+         (
+            Main.get_model().get_predicate_as_relation("is_lower_than")
+         ).not
+         (
+            /* (not (is_lower_than [depth node_of_path] [depth node_for_f])) */
+         ).forAll
+         (
+            node_of_path.oneOf
+            (
+               node_for_f.join
+               (
+                  chosen_path.join
+                  (
+                     Main.get_model().get_predicate_as_relation("is_before")
+                  ).transpose()
+               )
+            )
+         ).and
+         (
+            ($bl_formula.result)
+         ).forSome
+         (
+            node_for_f.oneOf
+            (
+               chosen_path.join
+               (
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
+            )
+         ).forAll
+         (
+            chosen_path.oneOf
+            (
+               current_node.join
+               (
+                  Main.get_model().get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose()
+               )
+            )
+         );
+   }
+;
+
+bl_depth_no_change_operator [Variable current_node]
+   returns [Formula result]
+
+   @init
+   {
+      final Variable node_of_path, node_for_f, chosen_path;
+
+      node_of_path = Main.get_variable_manager().generate_new_variable();
+      node_for_f = Main.get_variable_manager().generate_new_variable();
+      chosen_path = Main.get_variable_manager().generate_new_variable();
+   }
+
+   :
+   (WS)* DEPTH_NO_PARENT_OPERATOR_KW
+      bl_formula[node_for_f]
+   (WS)* R_PAREN
+
+   {
+      final Relation depth_relation;
+
+      depth_relation = Main.get_model().get_predicate_as_relation("depth");
+
+      $result =
+         node_of_path.join
+         (
+            depth_relation
+         ).eq
+         (
+            node_for_f.join(depth_relation)
+         /* (eq? [depth node_of_path] [depth node_for_f]) */
+         ).forAll
+         (
+            node_of_path.oneOf
+            (
+               node_for_f.join
+               (
+                  chosen_path.join
+                  (
+                     Main.get_model().get_predicate_as_relation("is_before")
+                  ).transpose()
+               )
+            )
+         ).and
+         (
+            ($bl_formula.result)
+         ).forSome
+         (
+            node_for_f.oneOf
+            (
+               chosen_path.join
+               (
+                  Main.get_model().get_predicate_as_relation("contains_node")
+               )
+            )
+         ).forAll
+         (
+            chosen_path.oneOf
+            (
+               current_node.join
+               (
+                  Main.get_model().get_predicate_as_relation
+                  (
+                     "is_path_of"
+                  ).transpose()
+               )
+            )
+         );
+   }
+;
+
 /**** Formula Definition ******************************************************/
 bl_formula [Variable current_node]
    returns [Formula result]:
@@ -1084,4 +1230,12 @@ bl_formula [Variable current_node]
    {
       $result = ($bl_eu_operator.result);
    }
+   | bl_depth_no_parent_operator[current_node]
+   {
+      $result = ($bl_depth_no_parent_operator.result);
+   }
+   | bl_depth_no_change_operator[current_node]
+   {
+      $result = ($bl_depth_no_change_operator.result);
+   }
 ;