modelverse/models/plant_to_EPN.mvc

include "primitives.alh"
include "modelling.alh"
include "object_operations.alh"

A B {
    Composite schedule {
        {Contains} Success success {}
        {Contains} Failure failure {}
        {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 "down"!
                        $
                    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 "down"!
                        $
                }
                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 "neutral"!
                        $
                    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 "neutral"!
                        $
                }
                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 "down"!
                        $
                    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 "down"!
                        $
                }
                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 "interrupt"!
                        $
                    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 "interrupt"!
                        $
                }
                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 "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 "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 "no_objDetected"!
                        $
                    value_tokens = $
                        Integer function value(model : Element, name : String, mapping : Element):
                            return 1!
                        $
                }
                Post_Encapsulated_PetriNet/Port post_ports_15 {
                    label = "15"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "no_objDetected"!
                        $
                }
                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 "objPresent"!
                        $
                    value_tokens = $
                        Integer function value(model : Element, name : String, mapping : Element):
                            return 0!
                        $
                }
                Post_Encapsulated_PetriNet/Port post_ports_16 {
                    label = "16"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "objPresent"!
                        $
                }
                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 "no_objPresent"!
                        $
                    value_tokens = $
                        Integer function value(model : Element, name : String, mapping : Element):
                            return 1!
                        $
                }
                Post_Encapsulated_PetriNet/Port post_ports_17 {
                    label = "17"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "no_objPresent"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (post_ports_17, post_ports_07) {
                    label = "27"
                }
            }
        }
        {Contains} ForAll create_states {
            LHS {
                Pre_PW_Plant/State {
                    label = "0"
                }
            }
            RHS {
                Post_PW_Plant/State post_cs_0 {
                    label = "0"
                }
                Post_Encapsulated_PetriNet/Place post_cs1 {
                    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_PLANT2EPN_link (post_cs_0, post_cs_1) {
                    label = "2"
                }
            }
        }
        {Contains} ForAll command_transition {
            LHS {
                Pre_PW_Plant/State pre_ct_0{
                    label = "0"
                }
                Pre_PW_Plant/State pre_ct_1{
                    label = "1"
                }
                Pre_PW_Plant/Transition pre_ct_2{
                    label = "2"
                }
                Pre_Encapsulated_PetriNet/Place pre_ct_3{
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_ct_4{
                    label = "4"
                }
                Pre_PLANT2EPN_link (pre_ct_0, pre_ct_3) {
                    label = "5"
                }
                Pre_PLANT2EPN_link (pre_ct_1, 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"
                }
            }
            RHS {
                Post_PW_Plant/State post_ct_0{
                    label = "0"
                }
                Post_PW_Plant/State post_ct_1{
                    label = "1"
                }
                Post_PW_Plant/Transition post_ct_2{
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_ct_3{
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_ct_4{
                    label = "4"
                }
                Post_PLANT2EPN_link (post_ct_0, post_ct_3) {
                    label = "5"
                }
                Post_PLANT2EPN_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/Transition post_ct_10 {
                    label = "10"
                }
                Post_Encapsulated_PetriNet/P2T (post_ct_3, post_ct_10) {
                    label = "11"
                }
                Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_4) {
                    label = "12"
                }
                Post_Encapsulated_PetriNet/P2T (post_ct_7, post_ct_10) {
                    label = "13"
                }
                Post_Encapsulated_PetriNet/T2P (post_ct_10, post_ct_7) {
                    label = "14"
                }
            }
        }

        {Contains} ForAll check_object {
            LHS {
                Pre_PW_Plant/State pre_co_0{
                    label = "0"
                }
                Pre_PW_Plant/State pre_co_1{
                    label = "1"
                }
                Pre_PW_Plant/Transition pre_co_2{
                    label = "2"
                    constraint_objPresent = $
                        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_PLANT2EPN_link (pre_co_0, pre_co_3) {
                    label = "5"
                }
                Pre_PLANT2EPN_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"
                }
                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 objPresent
                        String port_name
                        objPresent = read_attribute(host_model, mapping["2"], "objPresent")
                        port_name = read_attribute(host_model, mapping["11"], "name")

                        if (objPresent == "Y"):
                            return (port_name == "objPresent")!
                        elif (objPresent == "N"):
                            return (port_name == "no_objPresent")!
                        else:
                            return False!
                    $
            }
            RHS {
                Post_PW_Plant/State post_co_0{
                    label = "0"
                }
                Post_PW_Plant/State post_co_1{
                    label = "1"
                }
                Post_PW_Plant/Transition post_co_2{
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_co_3{
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_co_4{
                    label = "4"
                }
                Post_PLANT2EPN_link (post_co_0, post_co_3) {
                    label = "5"
                }
                Post_PLANT2EPN_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_8) {
                    label = "10"
                }
            }
        }

        {Contains} ForAll detect {
            LHS {
                Pre_PW_Plant/NormalState pre_de_0{
                    label = "0"
                }
                Pre_PW_Plant/ErrorState pre_de_1{
                    label = "1"
                }
                Pre_PW_Plant/Transition pre_de_2{
                    label = "2"
                }
                Pre_Encapsulated_PetriNet/Place pre_de_3{
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_de_4{
                    label = "4"
                }
                Pre_PLANT2EPN_link (pre_de_0, pre_de_3) {
                    label = "5"
                }
                Pre_PLANT2EPN_link (pre_de_1, pre_de_4) {
                    label = "6"
                }
                Pre_Encapsulated_PetriNet/Transition pre_de_7 {
                    label = "7"
                }
                Pre_Encapsulated_PetriNet/P2T (pre_de_3, pre_de_7) {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/T2P (pre_de_7, pre_de_4) {
                    label = "9"
                }

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

                Pre_Encapsulated_PetriNet/Place pre_de_13 {
                    label = "13"
                }
                Pre_Encapsulated_PetriNet/Port pre_de_14 {
                    label = "14"
                    constraint_name = $
                        Boolean function constraint(value : String):
                            return (value == "interrupt")!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_de_14, pre_de_13) {
                    label = "15"
                }

                Pre_Encapsulated_PetriNet/Place pre_de_16 {
                    label = "16"
                }
                Pre_Encapsulated_PetriNet/Port pre_de_17 {
                    label = "17"
                    constraint_name = $
                        Boolean function constraint(value : String):
                            return (value == "no_objDetected")!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_de_17, pre_de_16) {
                    label = "18"
                }

                Pre_Encapsulated_PetriNet/Place pre_de_19 {
                    label = "19"
                }
                Pre_Encapsulated_PetriNet/Port pre_de_20 {
                    label = "20"
                    constraint_name = $
                        Boolean function constraint(value : String):
                            return (value == "objDetected")!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_de_20, pre_de_19) {
                    label = "21"
                }

                constraint = $
                    Boolean function constraint (host_model : Element, mapping : Element):
                        // Check whether the bound primary places match with the state
                        String source_type
                        String port_name
                        source_type = read_type(host_model, mapping["0"])
                        port_name = read_attribute(host_model, mapping["11"], "name")

                        if (source_type == "Up"):
                            return (port_name == "up")!
                        elif (source_type == "Neutral"):
                            return (port_name == "neutral")!
                        elif (source_type == "Down"):
                            return (port_name == "down")!
                        else:
                            return False!
                    $
            }
            RHS {
                Post_PW_Plant/NormalState post_de_0{
                    label = "0"
                }
                Post_PW_Plant/ErrorState post_de_1{
                    label = "1"
                }
                Post_PW_Plant/Transition post_de_2{
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_de_3{
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_de_4{
                    label = "4"
                }
                Post_PLANT2EPN_link (post_de_0, post_de_3) {
                    label = "5"
                }
                Post_PLANT2EPN_link (post_de_1, post_de_4) {
                    label = "6"
                }
                Post_Encapsulated_PetriNet/Transition post_de_7 {
                    label = "7"
                }
                Post_Encapsulated_PetriNet/P2T (post_de_3, post_de_7) {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_4) {
                    label = "9"
                }

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

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

                Post_Encapsulated_PetriNet/Place post_de_16 {
                    label = "16"
                }
                Post_Encapsulated_PetriNet/Port post_de_17 {
                    label = "17"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_de_17, post_de_16) {
                    label = "18"
                }

                Post_Encapsulated_PetriNet/Place post_de_19 {
                    label = "19"
                }
                Post_Encapsulated_PetriNet/Port post_de_20 {
                    label = "20"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_de_20, post_de_19) {
                    label = "21"
                }

                Post_Encapsulated_PetriNet/P2T (post_de_10, post_de_7) {
                    label = "22"
                }
                Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_13) {
                    label = "23"
                }
                Post_Encapsulated_PetriNet/P2T (post_de_16, post_de_7) {
                    label = "22"
                }
                Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_19) {
                    label = "23"
                }
            }
        }
        {Contains} ForAll remove_detect {
            LHS {
                Pre_PW_Plant/ErrorState pre_rd_0{
                    label = "0"
                }
                Pre_PW_Plant/NormalState pre_rd_1{
                    label = "1"
                }
                Pre_PW_Plant/Transition pre_rd_2{
                    label = "2"
                }
                Pre_Encapsulated_PetriNet/Place pre_rd_3{
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_rd_4{
                    label = "4"
                }
                Pre_PLANT2EPN_link (pre_rd_0, pre_rd_3) {
                    label = "5"
                }
                Pre_PLANT2EPN_link (pre_rd_1, pre_rd_4) {
                    label = "6"
                }
                Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
                    label = "7"
                }
                Pre_Encapsulated_PetriNet/P2T (pre_rd_3, pre_rd_7) {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/T2P (pre_rd_7, pre_rd_4) {
                    label = "9"
                }

                Pre_Encapsulated_PetriNet/Place pre_rd_10 {
                    label = "10"
                }
                Pre_Encapsulated_PetriNet/Port pre_rd_11 {
                    label = "11"
                    constraint_name = $
                        Boolean function constraint(value : String):
                            return (value == "objDetected")!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_rd_11, pre_rd_10) {
                    label = "12"
                }

                Pre_Encapsulated_PetriNet/Place pre_rd_13 {
                    label = "13"
                }
                Pre_Encapsulated_PetriNet/Port pre_rd_14 {
                    label = "14"
                    constraint_name = $
                        Boolean function constraint(value : String):
                            return (value == "no_objDetected")!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_rd_14, pre_rd_13) {
                    label = "15"
                }
            }
            RHS {
                Post_PW_Plant/NormalState post_rd_0{
                    label = "0"
                }
                Post_PW_Plant/ErrorState post_rd_1{
                    label = "1"
                }
                Post_PW_Plant/Transition post_rd_2{
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_rd_3{
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_rd_4{
                    label = "4"
                }
                Post_PLANT2EPN_link (post_rd_0, post_rd_3) {
                    label = "5"
                }
                Post_PLANT2EPN_link (post_rd_1, post_rd_4) {
                    label = "6"
                }
                Post_Encapsulated_PetriNet/Transition post_rd_7 {
                    label = "7"
                }
                Post_Encapsulated_PetriNet/P2T (post_rd_3, post_rd_7) {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_4) {
                    label = "9"
                }

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

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

                Post_Encapsulated_PetriNet/P2T (post_rd_10, post_rd_7) {
                    label = "16"
                }
                Post_Encapsulated_PetriNet/T2P (post_rd_7, post_rd_13) {
                    label = "17"
                }
            }
        }
    }
    Initial (schedule, init_ports) {}

    OnSuccess (init_ports, create_states) {}
    OnSuccess (create_states, command_transition) {}
    OnSuccess (command_transition, check_object) {}
    OnSuccess (check_object, detect) {}
    OnSuccess (detect, remove_detect) {}
    OnSuccess (remove_detect, success) {}

    OnFailure (init_ports, create_states) {}
    OnFailure (create_states, command_transition) {}
    OnFailure (command_transition, check_object) {}
    OnFailure (check_object, detect) {}
    OnFailure (detect, remove_detect) {}
    OnFailure (remove_detect, success) {}
}