First shot at depths operators.

11 files changed, 245 insertions, 22 deletions

diff --git a/ast-to-instr/src/Depths.java b/ast-to-instr/src/Depths.java
new file mode 100644
index 0000000..ade01c8
--- /dev/null
+++ b/ast-to-instr/src/Depths.java
@@ -0,0 +1,72 @@
+import java.util.Map;
+import java.util.HashMap;
+
+public class Depths
+{
+   private static final Map<Integer, IDs> TO_ID;
+   private static final OutputFile DEPTHS_OUTPUT;
+   private static int highest_depth;
+
+   static
+   {
+      highest_depth = -1;
+
+      TO_ID = new HashMap<Integer, IDs>();
+
+      /* TODO: filename as a param? */
+      DEPTHS_OUTPUT = OutputFile.new_output_file("depths.mod");
+   }
+
+   private Depths () {} /* Utility class. */
+
+   public static IDs get_id_from_depth
+   (
+      final String depth
+   )
+   {
+      return get_id_from_depth(Integer.valueOf(depth));
+   }
+
+   public static IDs get_id_from_depth
+   (
+      final Integer depth
+   )
+   {
+      IDs result;
+
+      result = TO_ID.get(depth);
+
+      if (result == null)
+      {
+         result = IDs.generate_new_id(DEPTHS_OUTPUT, "depth");
+
+         TO_ID.put(depth, result);
+      }
+
+      if (depth.intValue() > highest_depth)
+      {
+         highest_depth = depth.intValue();
+      }
+
+      return result;
+   }
+
+   public static void generate_predicates ()
+   {
+      for
+      (
+         int current_depth = highest_depth;
+         current_depth > 0;
+         --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))
+         );
+      }
+   }
+}
diff --git a/ast-to-instr/src/Main.java b/ast-to-instr/src/Main.java
index 5bc45a0..0e24f57 100644
--- a/ast-to-instr/src/Main.java
+++ b/ast-to-instr/src/Main.java
@@ -87,6 +87,8 @@ public class Main
 
       parse_content(vhdl_files);
 
+      Depths.generate_predicates();
+
       OutputFile.close_all();
    }
 
diff --git a/ast-to-instr/src/Strings.java b/ast-to-instr/src/Strings.java
index 67189ad..a03070b 100644
--- a/ast-to-instr/src/Strings.java
+++ b/ast-to-instr/src/Strings.java
@@ -18,7 +18,7 @@ public class Strings
 
    public static IDs get_id_from_string
    (
-      String string
+      final String string
    )
    {
       return get_id_from_string(Main.get_main_output(), string);
diff --git a/ast-to-instr/src/VHDLCSNode.java b/ast-to-instr/src/VHDLCSNode.java
index f500345..6682613 100644
--- a/ast-to-instr/src/VHDLCSNode.java
+++ b/ast-to-instr/src/VHDLCSNode.java
@@ -130,10 +130,7 @@ public class VHDLCSNode extends VHDLNode
          output,
          "depth",
          local_id,
-         Strings.get_id_from_string
-         (
-            Integer.toString(depth)
-         )
+         Depths.get_id_from_depth(new Integer(depth))
       );
    }
 
diff --git a/ast-to-instr/src/VHDLISNode.java b/ast-to-instr/src/VHDLISNode.java
index 3c293cd..4883080 100644
--- a/ast-to-instr/src/VHDLISNode.java
+++ b/ast-to-instr/src/VHDLISNode.java
@@ -128,10 +128,7 @@ public class VHDLISNode extends VHDLNode
          output,
          "depth",
          local_id,
-         Strings.get_id_from_string
-         (
-            Integer.toString(depth)
-         )
+         Depths.get_id_from_depth(new Integer(depth))
       );
    }
 
diff --git a/ast-to-instr/src/VHDLSSASNode.java b/ast-to-instr/src/VHDLSSASNode.java
index b638f81..944ad18 100644
--- a/ast-to-instr/src/VHDLSSASNode.java
+++ b/ast-to-instr/src/VHDLSSASNode.java
@@ -122,10 +122,7 @@ public class VHDLSSASNode extends VHDLNode
          output,
          "depth",
          local_id,
-         Strings.get_id_from_string
-         (
-            Integer.toString(depth)
-         )
+         Depths.get_id_from_depth(new Integer(depth))
       );
    }
 
diff --git a/ast-to-instr/src/VHDLWNode.java b/ast-to-instr/src/VHDLWNode.java
index 4052229..b893c7a 100644
--- a/ast-to-instr/src/VHDLWNode.java
+++ b/ast-to-instr/src/VHDLWNode.java
@@ -117,10 +117,7 @@ public class VHDLWNode extends VHDLNode
          output,
          "depth",
          local_id,
-         Strings.get_id_from_string
-         (
-            Integer.toString(depth)
-         )
+         Depths.get_id_from_depth(new Integer(depth))
       );
    }
 
diff --git a/data/level/control_flow_level.lvl b/data/level/control_flow_level.lvl
index 3b11efe..106235d 100644
--- a/data/level/control_flow_level.lvl
+++ b/data/level/control_flow_level.lvl
@@ -5,7 +5,7 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (add_type node)
-(add_type node_depth)
+(add_type depth)
 
 ;; Redundancies
 (add_type process)
@@ -16,9 +16,7 @@
 ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (add_predicate is_start_node node process)
-(add_predicate has_kind node string)
 (add_predicate has_option node string)
-(add_predicate has_depth node node_depth)
 (add_predicate node_connect node node)
 
 ;;; To be removed soon.
@@ -29,6 +27,8 @@
 (add_predicate is_read_element node string string)
 (add_predicate is_terminal node)
 
+(add_predicate is_lower_than depth depth)
+
 (add_function label node string)
 (add_function kind node string)
-(add_function depth node string)
+(add_function depth node depth)
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);
+   }
 ;