modelverse/models/environment_to_EPN.mvc

include "primitives.alh"

A B {
    Composite schedule {
        {Contains} Success success {}
        {Contains} Failure failure {}
        {Contains} ForAll create_ports {
            LHS {
                Pre_Environment_PW/Event {
                    label = "1"
                }
            }
            RHS {
                Post_Environment_PW/Event {
                    label = "1"
                }
                Post_Encapsulated_PetriNet/Place cp_place {
                    label = "2"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return read_attribute(model, mapping["0"], "name")!
                        $
                }
                Post_Encapsulated_PetriNet/Port cp_port {
                    label = "3"
                    value_name = $
                        String function value(model : Element, name : String, mapping : Element):
                            return read_attribute(model, mapping["0"], "name")!
                        $
                }
                Post_ENV2EPN_link (cp_evt, cp_place) {
                    label = "4"
                }
                Post_Encapsulated_PetriNet/PortPlace (cp_port, cp_place) {
                    label = "5"
                    value_tokens = $
                        Integer value(model : Element, name : String, mapping : Element):
                            return 0!
                        $
                }
            }
        }
        {Contains} ForAll create_switches {
            LHS {
                Pre_Environment_PW/Group pre_grp {
                    label = "1"
                }
                Pre_Environment_PW/Event pre_evt_a {
                    label = "2"
                }
                Pre_Environment_PW/Event pre_evt_b {
                    label = "3"
                }
                Pre_Environment_PW/Contains (pre_grp, pre_evt_a) {
                    label = "4"
                }
                Pre_Environment_PW/Contains (pre_grp, pre_evt_b) {
                    label = "5"
                }
                Pre_ENV2EPN_link (pre_evt_a, pre_place_a) {
                    label = "6"
                }
                Pre_ENV2EPN_link (pre_evt_b, pre_place_b) {
                    label = "7"
                }
                Pre_Encapsulated_PetriNet/Place pre_place_a {
                    label = "8"
                }
                Pre_Encapsulated_PetriNet/Place pre_place_b {
                    label = "9"
                }
            }
            RHS {
                Post_Environment_PW/Group post_grp {
                    label = "1"
                }
                Post_Environment_PW/Event post_evt_a {
                    label = "2"
                }
                Post_Environment_PW/Event post_evt_b {
                    label = "3"
                }
                Post_Environment_PW/Contains (post_grp, post_evt_a) {
                    label = "4"
                }
                Post_Environment_PW/Contains (post_grp, post_evt_b) {
                    label = "5"
                }
                Post_ENV2EPN_link (post_evt_a, post_place_a) {
                    label = "6"
                }
                Post_ENV2EPN_link (post_evt_b, post_place_b) {
                    label = "7"
                }
                Post_Encapsulated_PetriNet/Place post_place_a {
                    label = "8"
                }
                Post_Encapsulated_PetriNet/Place post_place_b {
                    label = "9"
                }
                Post_Encapsulated_PetriNet/P2T (post_place_a, post_transition) {
                    label = "10"
                }
                Post_Encapsulated_PetriNet/T2P (post_transition, post_place_b) {
                    label = "11"
                }
                Post_Encapsulated_PetriNet/Transition post_transition {
                    label = "12"
                }
            }
        }
    }
    Initial (schedule, create_ports) {}
    OnSuccess (create_ports, create_switches) {}
    OnSuccess (create_switches, success) {}
    OnFailure (create_ports, failure) {}
    OnFailure (create_switches, failure) {}
}