| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/parser/PropertyParser.g4')
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 23 |
1 files changed, 18 insertions, 5 deletions
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 |