From 1d0b2f2214941f97ed8f457a052e6c59904e120c Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 18 Jul 2017 16:26:51 +0200 Subject: Solves previous problem by changing path def. Instead of the path "n1 -> n2 -> n3" being "n2 -> n3" a path starting from n1, it's now "n1 -> n2 -> n3" (still starting from n1). --- instr-to-kodkod/parser/PropertyParser.g4 | 252 +++++++++++++++++++++++-------- 1 file changed, 187 insertions(+), 65 deletions(-) (limited to 'instr-to-kodkod/parser/PropertyParser.g4') diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 2df87cb..4aeeffc 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -18,6 +18,7 @@ options @members { /* of the class */ + } prog: @@ -429,7 +430,6 @@ bl_ex_operator [Variable current_state] } ; - bl_ag_operator [Variable current_state] returns [Formula result]: @@ -447,135 +447,257 @@ bl_ag_operator [Variable current_state] { /* TODO */ $result = - Formula.replace /* That does not seem to exist. */ - ( - next_state, - current_state, - $bl_formula - ).and + $bl_formula.forAll ( - $bl_formula.forAll - ( - {n | \in contains_node} - ).forAll + next_state.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation + ( + "is_path_of" + ).transpose() /* (is_path_of path node), we want the path. */ + ).join + ( + MODEL.get_predicate_as_relation("contains_node") + ). ) ) } ; -bl_eg_operator returns [Formula result]: - (WS)* EG_OPERATOR_KW bl_formula (WS)* R_PAREN +bl_eg_operator [Variable current_state] + returns [Formula result]: + + @init + { + final Variable next_state, chosen_path; + + next_state = VARIABLE_SET.generate_new_state_variable(); + chosen_path = VARIABLE_SET.generate_new_state_variable(); + } + + (WS)* EG_OPERATOR_KW + bl_formula[next_state] + (WS)* R_PAREN + { /* TODO */ $result = - $bl_formula.forSome - ( - current_node - ).and + $bl_formula.forAll ( - $bl_formula.forSome + next_state.in ( - {n | \in contains_node} - ).forAll + chosen_path.join + ( + MODEL.get_predicate_as_relation("contains_node") + ). + ) + ).forSome + ( + chosen_path.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation + ( + "is_path_of" + ).transpose() /* (is_path_of path node), we want the path. */ + ) ) ); } ; -bl_af_operator returns [Formula result]: - (WS)* AF_OPERATOR_KW bl_formula (WS)* R_PAREN +bl_af_operator [Variable current_state] + returns [Formula result]: + + @init + { + final Variable next_state, chosen_path; + + next_state = VARIABLE_SET.generate_new_state_variable(); + chosen_path = VARIABLE_SET.generate_new_state_variable(); + } + + (WS)* AF_OPERATOR_KW + bl_formula[next_state] + (WS)* R_PAREN + { /* TODO */ $result = $bl_formula.forSome ( - current_node - ).or - ( - $bl_formula.forAll + next_state.in ( - {n | \in contains_node} - ).forSome + chosen_path.join + ( + MODEL.get_predicate_as_relation("contains_node") + ). + ) + ).forAll + ( + chosen_path.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation + ( + "is_path_of" + ).transpose() /* (is_path_of path node), we want the path. */ + ) ) ); } ; -bl_ef_operator returns [Formula result]: - (WS)* EF_OPERATOR_KW bl_formula (WS)* R_PAREN +bl_ef_operator [Variable current_state] + returns [Formula result]: + + @init + { + final Variable next_state, chosen_path; + + next_state = VARIABLE_SET.generate_new_state_variable(); + chosen_path = VARIABLE_SET.generate_new_state_variable(); + } + + (WS)* EF_OPERATOR_KW + bl_formula[next_state] + (WS)* R_PAREN + { /* TODO */ $result = $bl_formula.forSome ( - current_node - ).or - ( - $bl_formula.forSome + next_state.in ( - {n | \in contains_node} - ).forSome + chosen_path.join + ( + MODEL.get_predicate_as_relation("contains_node") + ). + ) + ).forSome + ( + chosen_path.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation + ( + "is_path_of" + ).transpose() /* (is_path_of path node), we want the path. */ + ) ) ); } ; -bl_au_operator returns [Formula result]: (WS)* AU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN +bl_au_operator [Variable current_state] + returns [Formula result]: + + @init + { + final Variable f1_state, f2_state, chosen_path; + + f1_state = VARIABLE_SET.generate_new_state_variable(); + f2_state = VARIABLE_SET.generate_new_state_variable(); + chosen_path = VARIABLE_SET.generate_new_state_variable(); + } + + (WS)* AU_OPERATOR_KW + f1=bl_formula[f1_state] + f2=bl_formula[f2_state] + (WS)* R_PAREN + { /* TODO */ $result = - $f1.forSome + $f1.forAll ( - current_node - ).and - ( - $f2.and + f1_state.in ( - $f1.forAll + f2_state.join ( - {t | \in is_before} + chosen_path.join + ( + MODEL.get_predicate_as_relation("is_before") + ).transpose() ) - ).forSome + ); + ).forSome + ( + f2_state.in ( - {n | \in contains_node} - ).forAll + chosen_path.join + ( + MODEL.get_predicate_as_relation("contains_node") + ) + ) + ).forAll + ( + chosen_path.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation("is_path_of").transpose() + ) ) ); } ; -bl_eu_operator returns [Formula result]: - (WS)* EU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN +bl_eu_operator [Variable current_state] + returns [Formula result]: + + @init + { + final Variable f1_state, f2_state, chosen_path; + + f1_state = VARIABLE_SET.generate_new_state_variable(); + f2_state = VARIABLE_SET.generate_new_state_variable(); + chosen_path = VARIABLE_SET.generate_new_state_variable(); + } + + (WS)* EU_OPERATOR_KW + f1=bl_formula[f1_state] + f2=bl_formula[f2_state] + (WS)* R_PAREN + { /* TODO */ $result = - $f1.forSome - ( - current_node - ).and + $f1.forAll ( - $f2.and + f1_state.in ( - $f1.forAll + f2_state.join ( - {t | \in is_before} + chosen_path.join + ( + MODEL.get_predicate_as_relation("is_before") + ).transpose() ) - ).forSome + ); + ).forSome + ( + f2_state.in ( - {n | \in contains_node} - ).forSome + chosen_path.join + ( + MODEL.get_predicate_as_relation("contains_node") + ) + ) + ).forSome + ( + chosen_path.in ( - {p | \in is_path_of} + current_state.join + ( + MODEL.get_predicate_as_relation("is_path_of").transpose() + ) ) ); } -- cgit v1.2.3-70-g09d2