modelverse/models/pm_req_analyse.mvc

ProcessModel analyse_requirements {
    Start start {}
    Finish finish {}

    Exec define_req {
        name = "define_req"
    }
    Exec make_initial_models {
        name = "make_initial_models"
    }

    ForkJoin forkjoin1 {}

    Exec refine_plant {
        name = "refine_plant"
    }
    Exec refine_environment {
        name = "refine_environment"
    }
    Exec refine_control {
        name = "refine_control"
    }
    Exec refine_query {
        name = "refine_query"
    }

    Exec plant_to_EPN {
        name = "plant_to_EPN"
    }
    Exec environment_to_EPN {
        name = "environment_to_EPN"
    }
    Exec control_to_EPN {
        name = "control_to_EPN"
    }

    ForkJoin forkjoin2 {}

    Exec combine_EPN {
        name = "combine_EPN"
    }

    Exec EPN_to_PN {
        name = "EPN_to_PN"
    }

    Exec analyse {
        name = "reachability"
    }

    ForkJoin forkjoin3 {}

    Exec matches {
        name = "query_match"
    }

    Decision found {}

    Data req {
        name = "requirements"
        type = "Requirements"
    }
    Data plant_model {
        name = "plant_model"
        type = "PW_Plant"
    }
    Data environment_model {
        name = "environment_model"
        type = "PW_Environment"
    }
    Data control_model {
        name = "control_model"
        type = "PW_Control"
    }
    Data plant_EPN {
        name = "plant_EPN"
        type = "Encapsulated_PetriNet"
    }
    Data control_EPN {
        name = "control_EPN"
        type = "Encapsulated_PetriNet"
    }
    Data environment_EPN {
        name = "environment_EPN"
        type = "Encapsulated_PetriNet"
    }
    Data merged_EPN {
        name = "merged_EPN"
        type = "Encapsulated_PetriNet"
    }
    Data pn {
        name = "pn"
        type = "PetriNet"
    }
    Data reachability_graph {
        name = "reachability"
        type = "ReachabilityGraph"
    }
    Data query {
        name = "query"
        type = "Query"
    }

    Next (start, define_req) {}
    Next (define_req, make_initial_models) {}
    Next (make_initial_models, forkjoin1) {}
    Next (forkjoin1, refine_plant) {}
    Next (forkjoin1, refine_environment) {}
    Next (forkjoin1, refine_control) {}
    Next (forkjoin1, refine_query) {}
    Next (refine_plant, plant_to_EPN) {}
    Next (refine_environment, environment_to_EPN) {}
    Next (refine_control, control_to_EPN) {}
    Next (plant_to_EPN, forkjoin2) {}
    Next (environment_to_EPN, forkjoin2) {}
    Next (control_to_EPN, forkjoin2) {}
    Next (forkjoin2, combine_EPN) {}
    Next (combine_EPN, EPN_to_PN) {}
    Next (EPN_to_PN, analyse) {}
    Next (analyse, forkjoin3) {}
    Next (refine_query, forkjoin3) {}
    Next (forkjoin3, matches) {}
    Next (matches, found) {}
    Then (found, forkjoin1) {}
    Else (found, finish) {}

    Produces (define_req, req) {}

    Produces (make_initial_models, plant_model) {}
    Produces (make_initial_models, environment_model) {}
    Produces (make_initial_models, control_model) {}
    Produces (make_initial_models, query) {}

    Consumes (req, refine_plant) {}
    Consumes (req, refine_environment) {}
    Consumes (req, refine_control) {}
    Consumes (req, refine_query) {}

    Consumes (plant_model, refine_plant) {}
    Consumes (environment_model, refine_environment) {}
    Consumes (control_model, refine_control) {}
    Consumes (query, refine_query) {}
    Produces (refine_plant, plant_EPN) {}
    Produces (refine_control, control_EPN) {}
    Produces (refine_environment, environment_EPN) {}
    Produces (refine_query, query) {}

    Consumes (plant_EPN, combine_EPN) {}
    Consumes (environment_EPN, combine_EPN) {}
    Consumes (control_EPN, combine_EPN) {}
    Produces (combine_EPN, merged_EPN) {}

    Consumes (merged_EPN, EPN_to_PN) {}
    Produces (EPN_to_PN, pn) {}

    Consumes (pn, analyse) {}
    Produces (analyse, reachability_graph) {}

    Consumes (reachability_graph, matches) {}
    Consumes (query, matches) {}
}