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

All_RAM Control2EPN {
    Composite schedule {
        {Contains} Failure failure {}
        {Contains} Success success {}
        {Contains} Atomic init_ports {
            LHS {}
            RHS {
                Post_Encapsulated_PetriNet/Place init_place_0 {
                    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 init_port_0 {
                    label = "10"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "cmdDown"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_0, init_place_0) {
                    label = "20"
                }

                Post_Encapsulated_PetriNet/Place init_place_1 {
                    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 init_port_1 {
                    label = "11"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "cmdNeutral"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_1, init_place_1) {
                    label = "21"
                }
                Post_Encapsulated_PetriNet/Place init_place_2 {
                    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 init_port_2 {
                    label = "12"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "cmdUp"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_2, init_place_2) {
                    label = "22"
                }
                Post_Encapsulated_PetriNet/Place init_place_3 {
                    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 init_port_3 {
                    label = "13"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "objDetected"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_3, init_place_3) {
                    label = "23"
                }
                Post_Encapsulated_PetriNet/Place init_place_4 {
                    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 init_port_4 {
                    label = "14"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "no_objDetected"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_4, init_place_4) {
                    label = "24"
                }
                Post_Encapsulated_PetriNet/Place init_place_5 {
                    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 init_port_5 {
                    label = "15"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "up"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_5, init_place_5) {
                    label = "25"
                }
                Post_Encapsulated_PetriNet/Place init_place_6 {
                    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 0!
                        $
                }
                Post_Encapsulated_PetriNet/Port init_port_6 {
                    label = "16"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "neutral"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_6, init_place_6) {
                    label = "26"
                }
                Post_Encapsulated_PetriNet/Place init_place_7 {
                    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 init_port_7 {
                    label = "17"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "down"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_7, init_place_7) {
                    label = "27"
                }

                Post_Encapsulated_PetriNet/Place init_place_8 {
                    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 init_port_8 {
                    label = "18"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return "interrupt"!
                        $
                }
                Post_Encapsulated_PetriNet/PortPlace (init_port_8, init_place_8) {
                    label = "28"
                }
            }
        }
        {Contains} ForAll create_states {
            LHS {
                Pre_Control_PW/State {
                    label = "0"
                }
            }
            RHS {
                Post_Control_PW/State cs_s {
                    label = "0"
                }
                Post_Encapsulated_PetriNet/Place cs_p {
                    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 (cs_s, cs_p) {
                    label = "2"
                }
            }
        }

        {Contains} ForAll create_transitions {
            LHS {
                Pre_Control_PW/State pre_ct_s1 {
                    label = "0"
                }
                Pre_Control_PW/State pre_ct_s2 {
                    label = "1"
                }
                Pre_Control_PW/Transition (pre_ct_s1, pre_ct_s2) {
                    label = "2"
                }
                Pre_Encapsulated_PetriNet/Place pre_ct_p1 {
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_ct_p2 {
                    label = "4"
                }
                Pre_CTRL2EPN_link (pre_ct_s1, pre_ct_p1) {
                    label = "5"
                }
                Pre_CTRL2EPN_link (pre_ct_s2, pre_ct_p2) {
                    label = "6"
                }
                Pre_Encapsulated_PetriNet/Place pre_ps1 {
                    label = "7"
                }
                Pre_Encapsulated_PetriNet/Place pre_ps2 {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/Port pre_pp1 {
                    label = "9"
                    constraint_name = $
                        Boolean constraint(host_model : Element, name : String):
                            String t
                            t = read_attribute(host_model, name, "name")
                            if (bool_or(bool_or(t == "up", t == "neutral"), t == "down")):
                                return True:
                        $
                }
                Pre_Encapsulated_PetriNet/Port pre_pp2 {
                    label = "10"
                    constraint_name = $
                        Boolean constraint(host_model : Element, name : String):
                            String t
                            t = read_attribute(host_model, name, "name")
                            if (bool_or(bool_or(t == "up", t == "neutral"), t == "down")):
                                return True:
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_pp1, pre_ps1) {
                    label = "11"
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_pp2, pre_ps2) {
                    label = "12"
                }

                constraint = $
                    Boolean constraint (host_model : Element, mapping : Element):
                        // Check whether the bound primary places match with the state
                        String s1_type
                        String s2_type
                        String ps1_type
                        String ps2_type
                        s1_type = read_type(host_model, mapping["0"])
                        s2_type = read_type(host_model, mapping["1"])
                        ps1_type = read_attribute(host_model, mapping["9"], "name")
                        ps2_type = read_attribute(host_model, mapping["10"], "name")

                        if (s1_type == "Up"):
                            if (ps1_type != "up"):
                                return False!
                        elif (s1_type == "Down"):
                            if (ps1_type != "down"):
                                return False!
                        elif (s1_type == "Neutral"):
                            if (ps1_type != "neutral"):
                                return False!

                        if (s2_type == "Up"):
                            if (ps2_type != "up"):
                                return False!
                        elif (s2_type == "Down"):
                            if (ps2_type != "down"):
                                return False!
                        elif (s2_type == "Neutral"):
                            if (ps2_type != "neutral"):
                                return False!

                        return True!
                    $
            }
            RHS {
                Post_Control_PW/State post_ct_s1 {
                    label = "0"
                }
                Post_Control_PW/State post_ct_s2 {
                    label = "1"
                }
                Post_Control_PW/Transition (post_ct_s1, post_ct_s2) {
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_ct_p1 {
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_ct_p2 {
                    label = "4"
                }
                Post_CTRL2EPN_link (post_ct_s1, post_ct_p1) {
                    label = "5"
                }
                Post_CTRL2EPN_link (post_ct_s2, post_ct_p2) {
                    label = "6"
                }
                Post_Encapsulated_PetriNet/Place post_ps1 {
                    label = "7"
                }
                Post_Encapsulated_PetriNet/Place post_ps2 {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/Port post_pp1 {
                    label = "9"
                }
                Post_Encapsulated_PetriNet/Port post_pp2 {
                    label = "10"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_pp1, post_ps1) {
                    label = "11"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_pp2, post_ps2) {
                    label = "12"
                }
                Post_Encapsulated_PetriNet/Transition post_ct_t {
                    label = "13"
                }
                Post_Encapsulated_PetriNet/P2T (post_ps1, post_ct_t) {
                    label = "14"
                }
                Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ps2) {
                    label = "15"
                }
                Post_Encapsulated_PetriNet/P2T (post_ct_p1, post_ct_t) {
                    label = "16"
                }
                Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ct_p2) {
                    label = "17"
                }
            }
        }

        {Contains} ForAll check_object {
            LHS {
                Pre_Control_PW/State pre_cop_s1 {
                    label = "0"
                }
                Pre_Control_PW/State pre_cop_s2 {
                    label = "1"
                }
                Pre_Control_PW/Transition (pre_cop_s1, pre_cop_s2) {
                    label = "2"
                    constraint_objDetected = $
                        Boolean constraint(host_model : Element, name : String):
                            String t
                            t = read_attribute(host_model, name, "objDetected")
                            if (bool_or(t == "Y", t == "N")):
                                return True!
                            else:
                                return False!
                        $
                }
                Pre_Encapsulated_PetriNet/Place pre_cop_p1 {
                    label = "3"
                }
                Pre_Encapsulated_PetriNet/Place pre_cop_p2 {
                    label = "4"
                }
                Pre_CTRL2EPN_link (pre_cop_s1, pre_cop_p1) {
                    label = "5"
                }
                Pre_CTRL2EPN_link (pre_cop_s2, pre_cop_p2) {
                    label = "6"
                }
                Pre_Encapsulated_PetriNet/Place pre_cop_ps1 {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/Port pre_pp1 {
                    label = "11"
                    constraint_name = $
                        Boolean constraint(host_model : Element, name : String):
                            String t
                            t = read_attribute(host_model, name, "name")
                            if (bool_or(t == "objDetected", t == "no_objDetected")):
                                return True!
                            else:
                                return False!
                        $
                }
                Pre_Encapsulated_PetriNet/PortPlace (pre_pp1, pre_ps1) {
                    label = "12"
                }
                Pre_Encapsulated_PetriNet/Transition pre_cop_t {
                    label = "15"
                }
                Pre_Encapsulated_PetriNet/P2T (pre_ps1, pre_cop_t) {
                    label = "16"
                }
                Pre_Encapsulated_PetriNet/T2P (pre_cop_t, pre_ps2) {
                    label = "17"
                }

                constraint = $
                    Boolean 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"):
                            if (ps1_type == "objDetected"):
                                return True!
                        elif (s1_value == "N"):
                            if (ps1_type != "no_objDetected"):
                                return True!

                        return False!
                    $
            }
            RHS {
                Post_Control_PW/State post_ct_s1 {
                    label = "0"
                }
                Post_Control_PW/State post_ct_s2 {
                    label = "1"
                }
                Post_Control_PW/Transition (post_ct_s1, post_ct_s2) {
                    label = "2"
                }
                Post_Encapsulated_PetriNet/Place post_ct_p1 {
                    label = "3"
                }
                Post_Encapsulated_PetriNet/Place post_ct_p2 {
                    label = "4"
                }
                Post_CTRL2EPN_link (post_ct_s1, post_ct_p1) {
                    label = "5"
                }
                Post_CTRL2EPN_link (post_ct_s2, post_ct_p2) {
                    label = "6"
                }
                Post_Encapsulated_PetriNet/Place post_ps1 {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/Port post_pp1 {
                    label = "11"
                }
                Post_Encapsulated_PetriNet/PortPlace (post_pp1, post_ps1) {
                    label = "12"
                }
                Post_Encapsulated_PetriNet/Transition post_ct_t {
                    label = "15"
                }
                Post_Encapsulated_PetriNet/P2T (post_ps1, post_ct_t) {
                    label = "16"
                }
                Post_Encapsulated_PetriNet/T2P (post_ct_t, post_ps2) {
                    label = "17"
                }
                Post_Encapsulated_PetriNet/P2T (post_cop_obj, post_cop_t) {
                    label = "9"
                }
                Post_Encapsulated_PetriNet/T2P (post_cop_t, post_cop_obj) {
                    label = "10"
                }
            }
        }
    }
    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, check_input) {}
    OnSuccess (check_input, success) {}

    OnFailure (init_ports, create_states) {}
    OnFailure (create_states, create_transitions) {}
    OnFailure (create_transitions, check_object) {}
    OnFailure (check_object, fix_interrupt) {}
    OnFailure (fix_interrupt, check_input) {}
    OnFailure (check_input, success) {}
}

export annotate to models/pn_annotate