Adds missing predicate from g4 to instr scripts

4 files changed, 38 insertions, 2 deletions

diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.data
index a880606..a7cc9c0 100644
--- a/data/level/control_flow_level.data
+++ b/data/level/control_flow_level.data
@@ -10,6 +10,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)
diff --git a/instr-scripts/process_internals.py b/instr-scripts/process_internals.py
index a58fc5a..6b63632 100644
--- a/instr-scripts/process_internals.py
+++ b/instr-scripts/process_internals.py
@@ -33,11 +33,12 @@ def new_element (
     return result
 
 class Process_Internals:
-    def __init__ (self, xml, id_manager, wfm_manager, output):
+    def __init__ (self, xml, id_manager, wfm_manager, process_id, output):
         self.xml = xml
         self.id_manager = id_manager
         self.wfm_manager = wfm_manager
         self.output = output
+        self.process_id = process_id
 
     def parse (self):
         start = self.xml.find("./sequential_statement_chain")
@@ -97,6 +98,17 @@ class Process_Internals:
     def handle_if_node (self, xml, prev_nodes, node_depth, extra_attributes):
         cond_node_id = new_element(self.output, self.id_manager, "node")
 
+        ## FIXME: That's a dirty hack.
+        if (self.process_id != None):
+            self.output.write(
+                "(is_start_node "
+                + cond_node_id
+                + " "
+                + self.process_id
+                + ")\n"
+            )
+            self.process_id = None
+
         for pn in prev_nodes:
             self.output.write(
                 "(node_connect "
@@ -207,6 +219,17 @@ class Process_Internals:
     ):
         node_id = new_element(self.output, self.id_manager, "node")
 
+        ## FIXME: That's a dirty hack.
+        if (self.process_id != None):
+            self.output.write(
+                "(is_start_node "
+                + node_id
+                + " "
+                + self.process_id
+                + ")\n"
+            )
+            self.process_id = None
+
         for pn in prev_nodes:
             self.output.write(
                 "(node_connect "
@@ -308,6 +331,17 @@ class Process_Internals:
     def handle_case_node (self, xml, prev_nodes, node_depth, extra_attributes):
         cond_node_id = new_element(self.output, self.id_manager, "node")
 
+        ## FIXME: That's a dirty hack.
+        if (self.process_id != None):
+            self.output.write(
+                "(is_start_node "
+                + cond_node_id
+                + " "
+                + self.process_id
+                + ")\n"
+            )
+            self.process_id = None
+
         for pn in prev_nodes:
             self.output.write(
                 "(node_connect "
diff --git a/instr-scripts/structural_level.py b/instr-scripts/structural_level.py
index 9c99b3e..a5c9763 100755
--- a/instr-scripts/structural_level.py
+++ b/instr-scripts/structural_level.py
@@ -521,6 +521,7 @@ def handle_process (
         elem,
         id_manager,
         wfm_manager,
+        local_id,
         pf
     )
     internals.parse()
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 8d1fe21..63939d7 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -238,7 +238,7 @@ sl_ctl_verifies_operator
             (
                Main.get_variable_manager().get_variable(($ps.text)).join
                (
-                  Main.get_model().get_predicate_as_relation("start_node")
+                  Main.get_model().get_predicate_as_relation("is_start_node").transpose()
                )
             )
          );