include "primitives.alh" include "modelling.alh" include "object_operations.alh" A B { Composite schedule { {Contains} Success success {} {Contains} Failure failure {} {Contains} Atomic 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_2 { label = "2" } Pre_Encapsulated_PetriNet/PortPlace (pre_s_2, pre_s_1){ label = "3" } } RHS { Post_Encapsulated_PetriNet/Place post_s_1 { label = "1" } Post_Encapsulated_PetriNet/Port post_s_2 { label = "2" value_selected = $ Boolean function value(model : Element, name : String, mapping : Element): return True! $ } Post_Encapsulated_PetriNet/PortPlace (post_s_2, post_s_1){ label = "3" } } } {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" } 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_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" } Pre_Encapsulated_PetriNet/PortPlace (pre_p2t_5, pre_p2t_4){ label = "6" } Pre_Encapsulated_PetriNet/Transition pre_p2t_7 { label = "7" } Pre_Encapsulated_PetriNet/T2P (pre_p2t_7, pre_p2t_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_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/T2P (post_p2t_7, post_p2t_4) { label = "8" } Post_Encapsulated_PetriNet/T2P (post_p2t_7, post_p2t_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 value! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_rem_2, pre_rem_1){ label = "3" } Pre_Encapsulated_PetriNet/Place pre_rem_4 { label = "4" } Pre_Encapsulated_PetriNet/Port pre_rem_5 { label = "5" } Pre_Encapsulated_PetriNet/PortPlace (pre_rem_5, pre_rem_4){ label = "6" } } RHS { Post_Encapsulated_PetriNet/Place post_rem_1 { label = "1" } Post_Encapsulated_PetriNet/Port post_rem_2 { label = "2" } Post_Encapsulated_PetriNet/PortPlace (post_rem_2, post_rem_1){ label = "3" } } } {Contains} Atomic unselect { LHS { Pre_Encapsulated_PetriNet/Place pre_uns_1 { label = "1" } Pre_Encapsulated_PetriNet/Port pre_uns_2 { label = "2" constraint_selected = $ Boolean function constraint(value : Boolean): return value! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_uns_2, pre_uns_1){ label = "3" } } RHS { Post_Encapsulated_PetriNet/Place post_uns_1 { label = "1" } } } {Contains} ForAll copy_transitions { LHS { Pre_Encapsulated_PetriNets/Transition { label = "0" } } RHS { Post_Encapsulated_PetriNets/Transition ct1 { label = "0" } Post_PetriNets/Transition ct2 { label = "1" value_executing = $ Boolean function value(model : Element, name : String, mapping : Element): return True! $ 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_PetriNets/Place { label = "0" } } RHS { Post_Encapsulated_PetriNets/Place cp1 { label = "0" } Post_PetriNets/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_PetriNets/Place cp2t_p{ label = "0" } Pre_Encapsulated_PetriNets/Transition cp2t_t{ label = "1" } Pre_Encapsulated_PetriNets/P2T (cp2t_p, cp2t_t){ label = "2" } Pre_PetriNets/Place cp2t_p2{ label = "3" } Pre_PetriNets/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_PetriNets/Place rhs_cp2t_p{ label = "0" } Post_Encapsulated_PetriNets/Transition rhs_cp2t_t{ label = "1" } Post_Encapsulated_PetriNets/P2T rhs_cp2t_p2t (rhs_cp2t_p, rhs_cp2t_t){ label = "2" } Post_PetriNets/Place rhs_cp2t_p2 { label = "3" } Post_PetriNets/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_PetriNets/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_PetriNets/Place ct2p_p{ label = "0" } Pre_Encapsulated_PetriNets/Transition ct2p_t{ label = "1" } Pre_Encapsulated_PetriNets/T2P (ct2p_t, ct2p_p){ label = "2" } Pre_PetriNets/Place ct2p_p2{ label = "3" } Pre_PetriNets/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_PetriNets/Place rhs_ct2p_p{ label = "0" } Post_Encapsulated_PetriNets/Transition rhs_ct2p_t{ label = "1" } Post_Encapsulated_PetriNets/T2P (rhs_ct2p_t, rhs_ct2p_p){ label = "2" } Post_PetriNets/Place rhs_ct2p_p2 { label = "3" } Post_PetriNets/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_PetriNets/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) {} OnSuccess (select, merge_P2T) {} OnSuccess (merge_P2T, merge_T2P) {} OnSuccess (merge_T2P, remove_old) {} OnSuccess (remove_old, unselect) {} OnSuccess (unselect, select) {} OnFailure (select, copy_places) {} OnFailure (unselect_all, select) {} OnFailure (merge_P2T, merge_T2P) {} OnFailure (merge_T2P, remove_old) {} OnFailure (remove_old, unselect) {} OnFailure (unselect, failure) {} 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) {} }