modelverse/models/plant_to_EPN.mvc

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

Composite schedule {
    {Contains} Success success {}
    {Contains} Failure failure {}
    {Contains} ForAll finish {
        LHS {
            Pre_Encapsulated_PetriNet/Port {
                label = "0"
            }
        }
        RHS {
            Post_Encapsulated_PetriNet/Port {
                label = "0"
                value_name = $
                    String function value(model : Element, name : String, mapping : Element):
                        return string_join("plant/", read_attribute(model, name, "name"))!
                    $
            }
        }
    }
    {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 "up"!
                    $
                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 "up"!
                    $
            }
            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):
                        // Set the detected output based on the initial state
                        Element states
                        String state

                        states = allInstances(model, "PW_Plant/State")
                        while (set_len(states) > 0):
                            state = set_pop(states)
                            if (value_eq(read_attribute(model, state, "isInitial"), True)):
                                if (read_type(model, state) == "PW_Plant/ErrorState"):
                                    return 1!
                                else:
                                    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):
                        // Set the detected output based on the initial state
                        Element states
                        String state

                        states = allInstances(model, "PW_Plant/State")
                        while (set_len(states) > 0):
                            state = set_pop(states)
                            if (value_eq(read_attribute(model, state, "isInitial"), True)):
                                if (read_type(model, state) == "PW_Plant/ErrorState"):
                                    return 0!
                                else:
                                    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 0!
                    $
            }
            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_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_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 (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_PLANT2EPN_link P2E_l1 (pre_ct_0, pre_ct_3) {
                label = "5"
            }
            Pre_PLANT2EPN_link P2E_l2(pre_ct_1, pre_ct_4) {
                label = "6"
            }
            Pre_Encapsulated_PetriNet/Place pre_ct_7 {
                label = "7"
                constraint_name = $
                    Boolean function constraint(value : String):
                        return (bool_or(bool_or(value == "up", value == "neutral"), value == "down"))!
                    $
            }
            Pre_Encapsulated_PetriNet/Port pre_ct_8 {
                label = "8"
                constraint_name = $
                    Boolean function constraint(value : String):
                        return (bool_or(bool_or(value == "up", value == "neutral"), value == "down"))!
                    $
            }
            Pre_Encapsulated_PetriNet/PortPlace pp_l (pre_ct_8, pre_ct_7) {
                label = "9"
            }

            constraint = $
                Boolean function constraint(model : Element, mapping : Element):
                    String transition_type
                    String port_name
                    transition_type = read_type(model, mapping["2"])
                    port_name = read_attribute(model, mapping["8"], "name")

                    if (transition_type == "PW_Plant/OnUp"):
                        return (port_name == "up")!
                    elif (transition_type == "PW_Plant/OnNeutral"):
                        return (port_name == "neutral")!
                    elif (transition_type == "PW_Plant/OnDown"):
                        return (port_name == "down")!
                    else:
                        return False!
                    $
        }
        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 (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_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"
                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"], "objPresent"))!
                    $
            }
            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"
            }
            Post_PLANT2EPN_tlink (post_ct_2, post_ct_10) {
                label = "100"
            }
        }
    }

    {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 (pre_co_0, pre_co_1) {
                label = "2"
                constraint_objPresent = $
                    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 == "objPresent", value == "no_objPresent"))!
                    $
            }
            Pre_Encapsulated_PetriNet/PortPlace (pre_co_11, pre_co_8) {
                label = "12"
            }

            Pre_Encapsulated_PetriNet/Transition pre_co_15 {
                label = "15"
            }
            Pre_PLANT2EPN_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 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 (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_PLANT2EPN_tlink (post_co_2, post_co_15) {
                label = "100"
            }

        }
    }

    {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 (pre_de_0, pre_de_1) {
                label = "2"
            }
            Pre_Encapsulated_PetriNet/Transition pre_de_7 {
                label = "7"
            }

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

            Pre_Encapsulated_PetriNet/T2P (pre_de_7, pre_de_10) {
                label = "26"
            }

            Pre_PLANT2EPN_tlink (pre_de_2, pre_de_7) {
                label = "100"
            }

            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["2"])
                    port_name = read_attribute(host_model, mapping["11"], "name")

                    if (source_type == "PW_Plant/OnUp"):
                        return (port_name == "up")!
                    elif (source_type == "PW_Plant/OnNeutral"):
                        return (port_name == "neutral")!
                    elif (source_type == "PW_Plant/OnDown"):
                        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 (post_de_0, post_de_1){
                label = "2"
            }
            Post_Encapsulated_PetriNet/Transition post_de_7 {
                label = "7"
            }

            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/T2P (post_de_7, post_de_13) {
                label = "23"
            }
            Post_Encapsulated_PetriNet/P2T (post_de_16, post_de_7) {
                label = "24"
            }
            Post_Encapsulated_PetriNet/T2P (post_de_7, post_de_19) {
                label = "25"
            }
            Post_PLANT2EPN_tlink (post_de_2, post_de_7) {
                label = "100"
            }
        }
    }
    {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 (pre_rd_0, pre_rd_1){
                label = "2"
            }
            Pre_Encapsulated_PetriNet/Transition pre_rd_7 {
                label = "7"
            }

            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"
            }
            Pre_PLANT2EPN_tlink (pre_rd_2, pre_rd_7) {
                label = "100"
            }
        }
        RHS {
            Post_PW_Plant/ErrorState post_rd_0{
                label = "0"
            }
            Post_PW_Plant/NormalState post_rd_1{
                label = "1"
            }
            Post_PW_Plant/Transition post_rd_2 (post_rd_0, post_rd_1){
                label = "2"
            }
            Post_Encapsulated_PetriNet/Transition post_rd_7 {
                label = "7"
            }

            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"
            }
            Post_PLANT2EPN_tlink (post_rd_2, post_rd_7) {
                label = "100"
            }
        }
    }
}
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, finish) {}
OnSuccess (finish, 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, finish) {}
OnFailure (finish, failure) {}