include "primitives.alh" include "modelling.alh" include "object_operations.alh" A B { Composite schedule { {Contains} Success success {} {Contains} Failure failure {} {Contains} ForAll unselect_all { LHS { Pre_Encapsulated_PetriNet/Port pre_ua_1 { label = "1" } } RHS { Post_Encapsulated_PetriNet/Port post_ua_1 { label = "1" value_selected = $ Boolean function value(model : Element, name : String, mapping : Element): return False! $ } } } {Contains} Atomic select { LHS { Pre_Encapsulated_PetriNet/Place pre_s_1 { label = "1" } Pre_Encapsulated_PetriNet/Port pre_s_0 { label = "0" constraint_selected = $ Boolean function constraint(value : Boolean): return bool_not(value)! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_s_0, pre_s_1){ label = "2" } } NAC { Pre_Encapsulated_PetriNet/Port nac_s_0 { label = "0" } Pre_Encapsulated_PetriNet/Port nac_s_3 { label = "3" constraint_selected = $ Boolean function constraint(value : Boolean): return value! $ } constraint = $ Boolean function constraint(model : Element, mapping : Element): return value_eq(read_attribute(model, mapping["0"], "name"), read_attribute(model, mapping["3"], "name"))! $ } RHS { Post_Encapsulated_PetriNet/Place post_s_1 { label = "1" } Post_Encapsulated_PetriNet/Port post_s_0 { label = "0" value_selected = $ Boolean function value(model : Element, name : String, mapping : Element): log("Mark as selected: " + cast_v2s(read_attribute(model, name, "name"))) return True! $ } Post_Encapsulated_PetriNet/PortPlace (post_s_0, post_s_1){ label = "2" } } } {Contains} ForAll merge_P2T { LHS { Pre_Encapsulated_PetriNet/Place pre_p2t_1 { label = "1" } Pre_Encapsulated_PetriNet/Port pre_p2t_2 { label = "2" constraint_selected = $ Boolean function constraint(value : Boolean): return value! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_p2t_2, pre_p2t_1){ label = "3" } Pre_Encapsulated_PetriNet/Place pre_p2t_4 { label = "4" } Pre_Encapsulated_PetriNet/Port pre_p2t_5 { label = "5" constraint_selected = $ Boolean function constraint(value : Boolean): return bool_not(value)! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_p2t_5, pre_p2t_4){ label = "6" } Pre_Encapsulated_PetriNet/Transition pre_p2t_7 { label = "7" } Pre_Encapsulated_PetriNet/P2T (pre_p2t_4, pre_p2t_7) { label = "8" } constraint = $ Boolean function constraint(model : Element, mapping : Element): return value_eq(read_attribute(model, mapping["2"], "name"), read_attribute(model, mapping["5"], "name"))! $ } RHS { Post_Encapsulated_PetriNet/Place post_p2t_1 { label = "1" } Post_Encapsulated_PetriNet/Port post_p2t_2 { label = "2" } Post_Encapsulated_PetriNet/PortPlace (post_p2t_2, post_p2t_1){ label = "3" } Post_Encapsulated_PetriNet/Place post_p2t_4 { label = "4" } Post_Encapsulated_PetriNet/Port post_p2t_5 { label = "5" } Post_Encapsulated_PetriNet/PortPlace (post_p2t_5, post_p2t_4){ label = "6" } Post_Encapsulated_PetriNet/Transition post_p2t_7 { label = "7" } Post_Encapsulated_PetriNet/P2T (post_p2t_4, post_p2t_7) { label = "8" } Post_Encapsulated_PetriNet/P2T (post_p2t_1, post_p2t_7) { label = "9" } } } {Contains} ForAll merge_T2P { LHS { Pre_Encapsulated_PetriNet/Place pre_t2p_1 { label = "1" } Pre_Encapsulated_PetriNet/Port pre_t2p_2 { label = "2" constraint_selected = $ Boolean function constraint(value : Boolean): return value! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_t2p_2, pre_t2p_1){ label = "3" } Pre_Encapsulated_PetriNet/Place pre_t2p_4 { label = "4" } Pre_Encapsulated_PetriNet/Port pre_t2p_5 { label = "5" constraint_selected = $ Boolean function constraint(value : Boolean): return bool_not(value)! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_t2p_5, pre_t2p_4){ label = "6" } Pre_Encapsulated_PetriNet/Transition pre_t2p_7 { label = "7" } Pre_Encapsulated_PetriNet/T2P (pre_t2p_7, pre_t2p_4) { label = "8" } constraint = $ Boolean function constraint(model : Element, mapping : Element): return value_eq(read_attribute(model, mapping["2"], "name"), read_attribute(model, mapping["5"], "name"))! $ } RHS { Post_Encapsulated_PetriNet/Place post_t2p_1 { label = "1" } Post_Encapsulated_PetriNet/Port post_t2p_2 { label = "2" } Post_Encapsulated_PetriNet/PortPlace (post_t2p_2, post_t2p_1){ label = "3" } Post_Encapsulated_PetriNet/Place post_t2p_4 { label = "4" } Post_Encapsulated_PetriNet/Port post_t2p_5 { label = "5" } Post_Encapsulated_PetriNet/PortPlace (post_t2p_5, post_t2p_4){ label = "6" } Post_Encapsulated_PetriNet/Transition post_t2p_7 { label = "7" } Post_Encapsulated_PetriNet/T2P (post_t2p_7, post_t2p_4) { label = "8" } Post_Encapsulated_PetriNet/T2P (post_t2p_7, post_t2p_1) { label = "9" } } } {Contains} ForAll remove_old { LHS { Pre_Encapsulated_PetriNet/Place pre_rem_1 { label = "1" } Pre_Encapsulated_PetriNet/Port pre_rem_2 { label = "2" constraint_selected = $ Boolean function constraint(value : Boolean): return bool_not(value)! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_rem_2, pre_rem_1){ label = "3" } } RHS { } } {Contains} ForAll copy_transitions { LHS { Pre_Encapsulated_PetriNet/Transition { label = "0" } } RHS { Post_Encapsulated_PetriNet/Transition ct1 { label = "0" } Post_PetriNet/Transition ct2 { label = "1" value_name = $ Integer function value(model : Element, name : String, mapping : Element): return read_attribute(model, mapping["0"], "name")! $ } Post_EPN2PN_transition_link (ct1, ct2){ label = "2" } } } {Contains} ForAll copy_places { LHS { Pre_Encapsulated_PetriNet/Place { label = "0" } } RHS { Post_Encapsulated_PetriNet/Place cp1 { label = "0" } Post_PetriNet/Place cp2 { label = "1" value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return read_attribute(model, mapping["0"], "tokens")! $ value_name = $ Integer function value(model : Element, name : String, mapping : Element): return read_attribute(model, mapping["0"], "name")! $ } Post_EPN2PN_place_link (cp1, cp2){ label = "2" } } } {Contains} ForAll copy_P2T { LHS { Pre_Encapsulated_PetriNet/Place cp2t_p{ label = "0" } Pre_Encapsulated_PetriNet/Transition cp2t_t{ label = "1" } Pre_Encapsulated_PetriNet/P2T (cp2t_p, cp2t_t){ label = "2" } Pre_PetriNet/Place cp2t_p2{ label = "3" } Pre_PetriNet/Transition cp2t_t2{ label = "4" } Pre_EPN2PN_place_link (cp2t_p, cp2t_p2){ label = "5" } Pre_EPN2PN_transition_link (cp2t_t, cp2t_t2){ label = "6" } } RHS { Post_Encapsulated_PetriNet/Place rhs_cp2t_p{ label = "0" } Post_Encapsulated_PetriNet/Transition rhs_cp2t_t{ label = "1" } Post_Encapsulated_PetriNet/P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){ label = "2" } Post_PetriNet/Place rhs_cp2t_p2 { label = "3" } Post_PetriNet/Transition rhs_cp2t_t2 { label = "4" } Post_EPN2PN_place_link (rhs_cp2t_p, rhs_cp2t_p2){ label = "5" } Post_EPN2PN_transition_link (rhs_cp2t_t, rhs_cp2t_t2){ label = "6" } Post_PetriNet/P2T rhs_cp2t_p2t2(rhs_cp2t_p2, rhs_cp2t_t2) { label = "7" value_weight = $ Integer function value(host_model : Element, name : String, mapping : Element): return 1! $ } } } {Contains} ForAll copy_T2P { LHS { Pre_Encapsulated_PetriNet/Place ct2p_p{ label = "0" } Pre_Encapsulated_PetriNet/Transition ct2p_t{ label = "1" } Pre_Encapsulated_PetriNet/T2P (ct2p_t, ct2p_p){ label = "2" } Pre_PetriNet/Place ct2p_p2{ label = "3" } Pre_PetriNet/Transition ct2p_t2{ label = "4" } Pre_EPN2PN_place_link (ct2p_p, ct2p_p2){ label = "5" } Pre_EPN2PN_transition_link (ct2p_t, ct2p_t2){ label = "6" } } RHS { Post_Encapsulated_PetriNet/Place rhs_ct2p_p{ label = "0" } Post_Encapsulated_PetriNet/Transition rhs_ct2p_t{ label = "1" } Post_Encapsulated_PetriNet/T2P (rhs_ct2p_t, rhs_ct2p_p){ label = "2" } Post_PetriNet/Place rhs_ct2p_p2 { label = "3" } Post_PetriNet/Transition rhs_ct2p_t2 { label = "4" } Post_EPN2PN_place_link (rhs_ct2p_p, rhs_ct2p_p2){ label = "5" } Post_EPN2PN_transition_link (rhs_ct2p_t, rhs_ct2p_t2){ label = "6" } Post_PetriNet/T2P (rhs_ct2p_t2, rhs_ct2p_p2) { label = "7" value_weight = $ Integer function value(host_model : Element, name : String, mapping : Element): return 1! $ } } } } Initial (schedule, unselect_all) {} OnSuccess (unselect_all, select) {} OnFailure (unselect_all, select) {} OnSuccess (select, select) {} OnFailure (select, merge_P2T) {} OnSuccess (merge_P2T, merge_T2P) {} OnFailure (merge_P2T, merge_T2P) {} OnSuccess (merge_T2P, remove_old) {} OnFailure (merge_T2P, remove_old) {} OnSuccess (remove_old, copy_places) {} OnFailure (remove_old, copy_places) {} OnSuccess (copy_places, copy_transitions) {} OnSuccess (copy_transitions, copy_P2T) {} OnSuccess (copy_P2T, copy_T2P) {} OnSuccess (copy_T2P, success) {} OnFailure (copy_places, copy_transitions) {} OnFailure (copy_transitions, copy_P2T) {} OnFailure (copy_P2T, copy_T2P) {} OnFailure (copy_T2P, success) {} }