modelverse/models/control_to_EPN.mvc

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 1!
                        $
                }
                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 1!
                        $
                }
                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):
                            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):
                            return 1!
                        $
                }
                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):
                            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_1, pre_ct_3) {
                    label = "5"
                }
                Pre_CTRL2EPN_link (pre_ct_2, pre_ct_4) {
                    label = "6"
                }

                Pre_Encapsulated_PetriNet/Place pre_ct_7 {
                    label = "7"
                }
                Pre_Encapsulated_PetriNet/Port pre_ct_8 {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_ct_8, pre_ct_7) {
                    label = "9"
                }

                Pre_Encapsulated_PetriNet/Place pre_ct_10 {
                    label = "10"
                }
                Pre_Encapsulated_PetriNet/Port pre_ct_11 {
                    label = "11"
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_ct_11, pre_ct_10) {
                    label = "12"
                }

                Pre_Encapsulated_PetriNet/Place pre_ct_13 {
                    label = "13"
                }
                Pre_Encapsulated_PetriNet/Port pre_ct_14 {
                    label = "14"
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_ct_14, pre_ct_13) {
                    label = "15"
                }

                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_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_8 {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_ct_8, post_ct_7) {
                    label = "9"
                }

                Post_Encapsulated_PetriNet/Place post_ct_10 {
                    label = "10"
                }
                Post_Encapsulated_PetriNet/Port post_ct_11 {
                    label = "11"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_ct_11, post_ct_10) {
                    label = "12"
                }

                Post_Encapsulated_PetriNet/Place post_ct_13 {
                    label = "13"
                }
                Post_Encapsulated_PetriNet/Port post_ct_14 {
                    label = "14"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_ct_14, post_ct_13) {
                    label = "15"
                }

                Post_Encapsulated_PetriNet/Transition post_ct_16 {
                    label = "16"
                }

                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"
                }
            }
        }

        {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_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_3 {
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_co_4 {
                    label = "4"
                }
                Pre_CTRL2EPN_link (pre_co_0, pre_co_3) {
                    label = "5"
                }
                Pre_CTRL2EPN_link (pre_co_1, pre_co_4) {
                    label = "6"
                }
                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_Encapsulated_PetriNet/P2T (pre_co_3, pre_co_15) {
                    label = "16"
                }
                Pre_Encapsulated_PetriNet/T2P (pre_co_15, pre_co_4) {
                    label = "17"
                }

                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_0, post_co_1) {
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_co_3 {
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_co_4 {
                    label = "4"
                }
                Post_CTRL2EPN_link (post_co_0, post_co_3) {
                    label = "5"
                }
                Post_CTRL2EPN_link (post_co_1, post_co_4) {
                    label = "6"
                }
                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_3, post_co_15) {
                    label = "16"
                }
                Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
                    label = "17"
                }
                Post_Encapsulated_PetriNet/P2T (post_co_8, post_co_15) {
                    label = "9"
                }
                Post_Encapsulated_PetriNet/T2P (post_co_15, post_co_4) {
                    label = "10"
                }
            }
        }

        {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 == "Up"):
                            return (p_name == "up")!
                        elif (s_err_type == "Neutral"):
                            return (p_name == "neutral")!
                        elif (s_err_type == "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"
                }
                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 == "Up"):
                            return (p_name == "up")!
                        elif (s_err_type == "Neutral"):
                            return (p_name == "neutral")!
                        elif (s_err_type == "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"
                }
                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) {}
}