| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | data/level/control_flow_level.data | 1 | ||||
| -rw-r--r-- | instr-scripts/process_internals.py | 36 | ||||
| -rwxr-xr-x | instr-scripts/structural_level.py | 1 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 2 |
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() ) ) ); |