Fixes multiple issues with depths.

3 files changed, 30 insertions, 13 deletions

diff --git a/ast-to-instr/src/Depths.java b/ast-to-instr/src/Depths.java
index ade01c8..400ff58 100644
--- a/ast-to-instr/src/Depths.java
+++ b/ast-to-instr/src/Depths.java
@@ -60,13 +60,16 @@ public class Depths
          --current_depth
       )
       {
-         Predicates.add_entry
-         (
-            DEPTHS_OUTPUT,
-            "is_lower_than",
-            get_id_from_depth(new Integer(current_depth - 1)),
-            get_id_from_depth(new Integer(current_depth))
-         );
+         for (int i = 0; i < current_depth; ++i)
+         {
+            Predicates.add_entry
+            (
+               DEPTHS_OUTPUT,
+               "is_lower_than",
+               get_id_from_depth(new Integer(i)),
+               get_id_from_depth(new Integer(current_depth))
+            );
+         }
       }
    }
 }
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 705f3e2..fa91a23 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -11,7 +11,8 @@ LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 #PROPERTY_FILE = ../data/property/impossible_processes.pro
 #PROPERTY_FILE = ../data/property/incrementer.pro
 #PROPERTY_FILE = ../data/property/combinational_processes.pro
-PROPERTY_FILE = ../data/property/likely_a_clock.pro
+#PROPERTY_FILE = ../data/property/likely_a_clock.pro
+PROPERTY_FILE = ../data/property/cnes/CNE*.pro
 VAR_PREFIX = "_anon_"
 
 ## Executables #################################################################
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 5c93eac..40cb2aa 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -1047,9 +1047,10 @@ bl_depth_no_parent_operator [Variable current_node]
    (WS)* R_PAREN
 
    {
-      final Relation depth_relation;
+      final Relation depth_relation, lower_than_relation;
 
       depth_relation = Main.get_model().get_predicate_as_relation("depth");
+      lower_than_relation = Main.get_model().get_predicate_as_relation("depth");
 
       $result =
          node_of_path.join
@@ -1057,13 +1058,13 @@ bl_depth_no_parent_operator [Variable current_node]
             depth_relation
          ).product
          (
-            node_for_f.join(depth_relation)
+            current_node.join(depth_relation)
          ).in
          (
-            Main.get_model().get_predicate_as_relation("is_lower_than")
+            lower_than_relation
          ).not
          (
-            /* (not (is_lower_than [depth node_of_path] [depth node_for_f])) */
+            /* (not (is_lower_than [depth node_of_path] [depth current_node])) */
          ).forAll
          (
             node_of_path.oneOf
@@ -1078,7 +1079,19 @@ bl_depth_no_parent_operator [Variable current_node]
             )
          ).and
          (
-            ($bl_formula.result)
+            ($bl_formula.result).and
+            (
+               current_node.join
+               (
+                  depth_relation
+               ).product
+               (
+                  node_for_f
+               ).in
+               (
+                  lower_than_relation
+               ).not()
+            )
          ).forSome
          (
             node_for_f.oneOf