| summaryrefslogtreecommitdiff |
path: root/instr-to-kodkod
diff options
Diffstat (limited to 'instr-to-kodkod')
| -rw-r--r-- | instr-to-kodkod/Makefile | 6 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyLexer.g4 | 3 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 154 |
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); + } ; |