include "primitives.alh" include "modelling.alh" include "object_operations.alh" All_RAM Control2EPN { Composite schedule { {Contains} Failure failure {} {Contains} Success success {} {Contains} Atomic init_ports { LHS {} RHS { Post_Encapsulated_PetriNet/Place post_ports_00 { label = "00" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdDown"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_10 { label = "10" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdDown"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_10, post_ports_00) { label = "20" } Post_Encapsulated_PetriNet/Place post_ports_01 { label = "01" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdNeutral"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_11 { label = "11" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdNeutral"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_11, post_ports_01) { label = "21" } Post_Encapsulated_PetriNet/Place post_ports_02 { label = "02" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdUp"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_12 { label = "12" value_name = $ String function value(model : Element, name : String, mapping : Element): return "cmdUp"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_12, post_ports_02) { label = "22" } Post_Encapsulated_PetriNet/Place post_ports_03 { label = "03" value_name = $ String function value(model : Element, name : String, mapping : Element): return "objDetected"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_13 { label = "13" value_name = $ String function value(model : Element, name : String, mapping : Element): return "objDetected"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_13, post_ports_03) { label = "23" } Post_Encapsulated_PetriNet/Place post_ports_04 { label = "04" value_name = $ String function value(model : Element, name : String, mapping : Element): return "no_objDetected"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_14 { label = "14" value_name = $ String function value(model : Element, name : String, mapping : Element): return "no_objDetected"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_14, post_ports_04) { label = "24" } Post_Encapsulated_PetriNet/Place post_ports_05 { label = "05" value_name = $ String function value(model : Element, name : String, mapping : Element): return "up"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): // Set the detected output based on the initial state Element states String state states = allInstances(model, "PW_Control/State") while (read_nr_out(states) > 0): state = set_pop(states) if (value_eq(read_attribute(model, state, "isInitial"), True)): if (read_type(model, state) == "PW_Control/Up"): return 1! else: return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_15 { label = "15" value_name = $ String function value(model : Element, name : String, mapping : Element): return "up"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_15, post_ports_05) { label = "25" } Post_Encapsulated_PetriNet/Place post_ports_06 { label = "06" value_name = $ String function value(model : Element, name : String, mapping : Element): return "neutral"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): // Set the detected output based on the initial state Element states String state states = allInstances(model, "PW_Control/State") while (read_nr_out(states) > 0): state = set_pop(states) if (value_eq(read_attribute(model, state, "isInitial"), True)): if (read_type(model, state) == "PW_Control/Neutral"): return 1! else: return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_16 { label = "16" value_name = $ String function value(model : Element, name : String, mapping : Element): return "neutral"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_16, post_ports_06) { label = "26" } Post_Encapsulated_PetriNet/Place post_ports_07 { label = "07" value_name = $ String function value(model : Element, name : String, mapping : Element): return "down"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): // Set the detected output based on the initial state Element states String state states = allInstances(model, "PW_Control/State") while (read_nr_out(states) > 0): state = set_pop(states) if (value_eq(read_attribute(model, state, "isInitial"), True)): if (read_type(model, state) == "PW_Control/Down"): return 1! else: return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_17 { label = "17" value_name = $ String function value(model : Element, name : String, mapping : Element): return "down"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_17, post_ports_07) { label = "27" } Post_Encapsulated_PetriNet/Place post_ports_08 { label = "08" value_name = $ String function value(model : Element, name : String, mapping : Element): return "interrupt"! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): return 0! $ } Post_Encapsulated_PetriNet/Port post_ports_18 { label = "18" value_name = $ String function value(model : Element, name : String, mapping : Element): return "interrupt"! $ } Post_Encapsulated_PetriNet/PortPlace (post_ports_18, post_ports_08) { label = "28" } } } {Contains} ForAll create_states { LHS { Pre_PW_Control/State { label = "0" } } RHS { Post_PW_Control/State post_cs_0 { label = "0" } Post_Encapsulated_PetriNet/Place post_cs_1 { label = "1" value_name = $ String function value(model : Element, name : String, mapping : Element): return read_attribute(model, mapping["0"], "name")! $ value_tokens = $ Integer function value(model : Element, name : String, mapping : Element): if (value_eq(read_attribute(model, mapping["0"], "isInitial"), True)): return 1! else: return 0! $ } Post_CTRL2EPN_link (post_cs_0, post_cs_1) { label = "2" } } } {Contains} ForAll create_transitions { LHS { Pre_PW_Control/State pre_ct_0 { label = "0" } Pre_PW_Control/State pre_ct_1 { label = "1" } Pre_PW_Control/Transition pre_ct_2 (pre_ct_0, pre_ct_1) { label = "2" } Pre_Encapsulated_PetriNet/Place pre_ct_3 { label = "3" } Pre_Encapsulated_PetriNet/Place pre_ct_4 { label = "4" } Pre_CTRL2EPN_link (pre_ct_0, pre_ct_3) { label = "5" } Pre_CTRL2EPN_link (pre_ct_1, pre_ct_4) { label = "6" } Pre_Encapsulated_PetriNet/Port pre_ct_9 { label = "9" constraint_name = $ Boolean function constraint(value : String): return bool_or(bool_or(value == "up", value == "neutral"), value == "down")! $ } Pre_Encapsulated_PetriNet/Place pre_ct_7 { label = "7" } Pre_Encapsulated_PetriNet/PortPlace (pre_ct_9, pre_ct_7) { label = "8" } Pre_Encapsulated_PetriNet/Port pre_ct_12 { label = "12" constraint_name = $ Boolean function constraint(value : String): return bool_or(bool_or(value == "up", value == "neutral"), value == "down")! $ } Pre_Encapsulated_PetriNet/Place pre_ct_10 { label = "10" } Pre_Encapsulated_PetriNet/PortPlace (pre_ct_12, pre_ct_10) { label = "11" } Pre_Encapsulated_PetriNet/Port pre_ct_15 { label = "15" constraint_name = $ Boolean function constraint(value : String): return bool_or(bool_or(value == "cmdUp", value == "cmdNeutral"), value == "cmdDown")! $ } Pre_Encapsulated_PetriNet/Place pre_ct_13 { label = "13" } Pre_Encapsulated_PetriNet/PortPlace (pre_ct_15, pre_ct_13) { label = "14" } constraint = $ Boolean function constraint (host_model : Element, mapping : Element): // Check whether the bound primary places match with the state String type_0 String type_1 String type_2 String name_9 String name_12 String name_15 type_0 = read_type(host_model, mapping["0"]) type_1 = read_type(host_model, mapping["1"]) type_2 = read_type(host_model, mapping["2"]) name_9 = read_attribute(host_model, mapping["9"], "name") name_12 = read_attribute(host_model, mapping["12"], "name") name_15 = read_attribute(host_model, mapping["15"], "name") // Source part if (type_0 == "PW_Control/Up"): if (name_9 != "up"): return False! elif (type_0 == "PW_Control/Neutral"): if (name_9 != "neutral"): return False! elif (type_0 == "PW_Control/Down"): if (name_9 != "down"): return False! // Target part if (type_1 == "PW_Control/Up"): if (name_12 != "up"): return False! elif (type_1 == "PW_Control/Neutral"): if (name_12 != "neutral"): return False! elif (type_1 == "PW_Control/Down"): if (name_12 != "down"): return False! // Link part if (type_2 == "PW_Control/UpPressed"): if (name_15 != "cmdUp"): return False! elif (type_2 == "PW_Control/NonePressed"): if (name_15 != "cmdNeutral"): return False! elif (type_2 == "PW_Control/DownPressed"): if (name_15 != "cmdDown"): return False! // All passed, so OK! return True! $ } RHS { Post_PW_Control/State post_ct_0 { label = "0" } Post_PW_Control/State post_ct_1 { label = "1" } Post_PW_Control/Transition post_ct_2 (post_ct_0, post_ct_1) { label = "2" } Post_Encapsulated_PetriNet/Place post_ct_3 { label = "3" } Post_Encapsulated_PetriNet/Place post_ct_4 { label = "4" } Post_CTRL2EPN_link (post_ct_0, post_ct_3) { label = "5" } Post_CTRL2EPN_link (post_ct_1, post_ct_4) { label = "6" } Post_Encapsulated_PetriNet/Place post_ct_7 { label = "7" } Post_Encapsulated_PetriNet/Port post_ct_9 { label = "9" } Post_Encapsulated_PetriNet/PortPlace (post_ct_9, post_ct_7) { label = "8" } Post_Encapsulated_PetriNet/Place post_ct_10 { label = "10" } Post_Encapsulated_PetriNet/Port post_ct_12 { label = "12" } Post_Encapsulated_PetriNet/PortPlace (post_ct_12, post_ct_10) { label = "11" } Post_Encapsulated_PetriNet/Place post_ct_13 { label = "13" } Post_Encapsulated_PetriNet/Port post_ct_15 { label = "15" } Post_Encapsulated_PetriNet/PortPlace (post_ct_15, post_ct_13) { label = "14" } Post_Encapsulated_PetriNet/Transition post_ct_16 { label = "16" value_name = $ String function value(model : Element, name : String, mapping : Element): return string_join(string_join(read_attribute(model, mapping["0"], "name"), read_type(model, mapping["2"])), read_attribute(model, mapping["2"], "objDetected"))! $ } Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_16) { label = "17" } Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_4) { label = "18" } Post_Encapsulated_PetriNet/P2T (post_ct_7, post_ct_16) { label = "19" } Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_10) { label = "20" } Post_Encapsulated_PetriNet/P2T (post_ct_13, post_ct_16) { label = "21" } Post_Encapsulated_PetriNet/T2P (post_ct_16, post_ct_13) { label = "22" } Post_CTRL2EPN_tlink (post_ct_2, post_ct_16) { label = "100" } } } {Contains} ForAll check_object { LHS { Pre_PW_Control/State pre_co_0 { label = "0" } Pre_PW_Control/State pre_co_1 { label = "1" } Pre_PW_Control/Transition pre_co_2 (pre_co_0, pre_co_1) { label = "2" constraint_objDetected = $ Boolean function constraint(value : String): return (bool_or(value == "Y", value == "N"))! $ } Pre_Encapsulated_PetriNet/Place pre_co_8 { label = "8" } Pre_Encapsulated_PetriNet/Port pre_co_11 { label = "11" constraint_name = $ Boolean function constraint(value : String): return (bool_or(value == "objDetected", value == "no_objDetected"))! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_co_11, pre_co_8) { label = "12" } Pre_Encapsulated_PetriNet/Transition pre_co_15 { label = "15" } Pre_CTRL2EPN_tlink (pre_co_2, pre_co_15) { label = "100" } constraint = $ Boolean function constraint (host_model : Element, mapping : Element): // Check whether the bound primary places match with the state String s1_value String ps1_type s1_value = read_attribute(host_model, mapping["2"], "objDetected") ps1_type = read_attribute(host_model, mapping["11"], "name") if (s1_value == "Y"): return (ps1_type == "objDetected")! elif (s1_value == "N"): return (ps1_type == "no_objDetected")! else: return False! $ } RHS { Post_PW_Control/State post_co_0 { label = "0" } Post_PW_Control/State post_co_1 { label = "1" } Post_PW_Control/Transition post_co_2 (post_co_0, post_co_1) { label = "2" } Post_Encapsulated_PetriNet/Place post_co_8 { label = "8" } Post_Encapsulated_PetriNet/Port post_co_11 { label = "11" } Post_Encapsulated_PetriNet/PortPlace (post_co_11, post_co_8) { label = "12" } Post_Encapsulated_PetriNet/Transition post_co_15 { label = "15" } Post_Encapsulated_PetriNet/P2T (post_co_8, post_co_15) { label = "9" } Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_8) { label = "10" } Post_CTRL2EPN_tlink (post_co_2, post_co_15) { label = "100" } } } {Contains} ForAll fix_interrupt { LHS { Pre_PW_Control/State pre_fi_0 { label = "0" } Pre_PW_Control/State pre_fi_1 { label = "1" constraint_isError = $ Boolean function constraint(value : Boolean): return value! $ } Pre_Encapsulated_PetriNet/Place pre_fi_2 { label = "2" } Pre_Encapsulated_PetriNet/Place pre_fi_3 { label = "3" } Pre_CTRL2EPN_link (pre_fi_0, pre_fi_2) { label = "4" } Pre_CTRL2EPN_link (pre_fi_1, pre_fi_3) { label = "5" } Pre_Encapsulated_PetriNet/Place pre_fi_6 { label = "6" } Pre_Encapsulated_PetriNet/Place pre_fi_12 { label = "12" } Pre_Encapsulated_PetriNet/Port pre_fi_13 { label = "13" } Pre_Encapsulated_PetriNet/PortPlace (pre_fi_13, pre_fi_12) { label = "14" } Pre_Encapsulated_PetriNet/Port pre_fi_15 { label = "15" constraint_name = $ Boolean function constraint(value : String): return (value == "interrupt")! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_fi_15, pre_fi_6) { label = "16" } constraint = $ Boolean function constraint (host_model : Element, mapping : Element): // Check whether the bound primary places match with the state String s_err_type String p_name s_err_type = read_type(host_model, mapping["1"]) p_name = read_attribute(host_model, mapping["13"], "name") if (s_err_type == "PW_Control/Up"): return (p_name == "up")! elif (s_err_type == "PW_Control/Neutral"): return (p_name == "neutral")! elif (s_err_type == "PW_Control/Down"): return (p_name == "down")! else: return False! $ } RHS { Post_PW_Control/State post_fi_0 { label = "0" } Post_PW_Control/State post_fi_1 { label = "1" } Post_Encapsulated_PetriNet/Place post_fi_2 { label = "2" } Post_Encapsulated_PetriNet/Place post_fi_3 { label = "3" } Post_CTRL2EPN_link (post_fi_0, post_fi_2) { label = "4" } Post_CTRL2EPN_link (post_fi_1, post_fi_3) { label = "5" } Post_Encapsulated_PetriNet/Place post_fi_6 { label = "6" } Post_Encapsulated_PetriNet/Place post_fi_12 { label = "12" } Post_Encapsulated_PetriNet/Port post_fi_13 { label = "13" } Post_Encapsulated_PetriNet/PortPlace (post_fi_13, post_fi_12) { label = "14" } Post_Encapsulated_PetriNet/Port post_fi_15 { label = "15" } Post_Encapsulated_PetriNet/PortPlace (post_fi_15, post_fi_6) { label = "16" } Post_Encapsulated_PetriNet/Transition post_fi_7 { label = "7" value_name = $ String function value(model : Element, name : String, mapping : Element): return string_join(read_attribute(model, mapping["0"], "name"), "_onInterrupt")! $ } Post_Encapsulated_PetriNet/P2T (post_fi_2, post_fi_7) { label = "8" } Post_Encapsulated_PetriNet/T2P (post_fi_7, post_fi_3) { label = "9" } Post_Encapsulated_PetriNet/P2T (post_fi_6, post_fi_7) { label = "10" } Post_Encapsulated_PetriNet/T2P (post_fi_7, post_fi_12) { label = "11" } } } {Contains} ForAll fix_interrupt_self { LHS { Pre_PW_Control/State pre_fis_0 { label = "0" constraint_isError = $ Boolean function constraint(value : Boolean): return value! $ } Pre_Encapsulated_PetriNet/Place pre_fis_1 { label = "1" } Pre_CTRL2EPN_link (pre_fis_0, pre_fis_1) { label = "2" } Pre_Encapsulated_PetriNet/Place pre_fis_3 { label = "3" } Pre_Encapsulated_PetriNet/Port pre_fis_4 { label = "4" constraint_name = $ Boolean function constraint(value : String): return (value == "interrupt")! $ } Pre_Encapsulated_PetriNet/PortPlace (pre_fis_4, pre_fis_3) { label = "5" } Pre_Encapsulated_PetriNet/Place pre_fis_6 { label = "6" } Pre_Encapsulated_PetriNet/Port pre_fis_7 { label = "7" } Pre_Encapsulated_PetriNet/PortPlace (pre_fis_7, pre_fis_6) { label = "8" } constraint = $ Boolean function constraint (host_model : Element, mapping : Element): // Check whether the bound primary places match with the state String s_err_type String p_name s_err_type = read_type(host_model, mapping["0"]) p_name = read_attribute(host_model, mapping["7"], "name") if (s_err_type == "PW_Control/Up"): return (p_name == "up")! elif (s_err_type == "PW_Control/Neutral"): return (p_name == "neutral")! elif (s_err_type == "PW_Control/Down"): return (p_name == "down")! else: return False! $ } RHS { Post_PW_Control/State post_fis_0 { label = "0" } Post_Encapsulated_PetriNet/Place post_fis_1 { label = "1" } Post_CTRL2EPN_link (post_fis_0, post_fis_1) { label = "2" } Post_Encapsulated_PetriNet/Place post_fis_3 { label = "3" } Post_Encapsulated_PetriNet/Port post_fis_4 { label = "4" } Post_Encapsulated_PetriNet/PortPlace (post_fis_4, post_fis_3) { label = "5" } Post_Encapsulated_PetriNet/Place post_fis_6 { label = "6" } Post_Encapsulated_PetriNet/Port post_fis_7 { label = "7" } Post_Encapsulated_PetriNet/PortPlace (post_fis_7, post_fis_6) { label = "8" } Post_Encapsulated_PetriNet/Transition post_fis_9 { label = "9" value_name = $ String function value(model : Element, name : String, mapping : Element): return string_join(read_attribute(model, mapping["0"], "name"), "_onInterrupt")! $ } Post_Encapsulated_PetriNet/P2T (post_fis_3, post_fis_9) { label = "10" } Post_Encapsulated_PetriNet/T2P (post_fis_9, post_fis_6) { label = "11" } Post_Encapsulated_PetriNet/P2T (post_fis_1, post_fis_9) { label = "12" } Post_Encapsulated_PetriNet/T2P (post_fis_9, post_fis_1) { label = "13" } } } } Initial (schedule, init_ports) {} OnSuccess (init_ports, create_states) {} OnSuccess (create_states, create_transitions) {} OnSuccess (create_transitions, check_object) {} OnSuccess (check_object, fix_interrupt) {} OnSuccess (fix_interrupt, fix_interrupt_self) {} OnSuccess (fix_interrupt_self, success) {} OnFailure (init_ports, create_states) {} OnFailure (create_states, create_transitions) {} OnFailure (create_transitions, check_object) {} OnFailure (check_object, fix_interrupt) {} OnFailure (fix_interrupt, fix_interrupt_self) {} OnFailure (fix_interrupt_self, success) {} }