modelverse/models/pm_req_analyse.mvc

Start start {}
Finish finish {}

Exec revise_req {
    name = "revise_req"
}
Exec make_initial_models {
    name = "make_initial_models"
}

Fork fork1 {}

Exec revise_plant {
    name = "revise_plant"
}
Exec revise_environment {
    name = "revise_environment"
}
Exec revise_control {
    name = "revise_control"
}
Exec revise_query {
    name = "revise_query"
}
Exec revise_architecture {
    name = "revise_architecture"
}

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

Exec control_to_EPN {
    name = "control_to_EPN"
}

Join join2 {}

Exec combine_EPN {
    name = "combine_EPN"
}

Exec EPN_to_PN {
    name = "EPN_to_PN"
}

Exec analyse {
    name = "reachability"
}

Join join3 {}

Exec match {
    name = "match"
}

Exec bfs {
    name = "bfs"
}

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"
}
Data architecture {
    name = "architecture"
    type = "Architecture"
}

Next (start, make_initial_models) {}
Next (make_initial_models, revise_req) {}
Next (revise_req, fork1) {}
Next (fork1, revise_plant) {}
Next (fork1, revise_environment) {}
Next (fork1, revise_control) {}
Next (fork1, revise_query) {}
Next (fork1, revise_architecture) {}
Next (revise_plant, plant_to_EPN) {}
Next (revise_environment, environment_to_EPN) {}
Next (revise_control, control_to_EPN) {}
Next (plant_to_EPN, join2) {}
Next (environment_to_EPN, join2) {}
Next (control_to_EPN, join2) {}
Next (revise_architecture, join2) {}
Next (join2, combine_EPN) {}
Next (combine_EPN, analyse) {}
Next (analyse, join3) {}
Next (revise_query, join3) {}
Next (join3, match) {}
Next (match, found) {}
Then (found, bfs) {}
Next (bfs, fork1) {}
Else (found, finish) {}

Consumes (revise_req, req) {
}
Produces (revise_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) {
}
Produces (make_initial_models, architecture) {
}
Produces (make_initial_models, req) {
}

Consumes (revise_plant, req) {
}
Consumes (revise_environment, req) {
}
Consumes (revise_control, req) {
}
Consumes (revise_query, req) {
}
Consumes (revise_architecture, req) {
}

Consumes (revise_plant, plant_model) {
}
Consumes (revise_environment, environment_model) {
}
Consumes (revise_control, control_model) {
}
Consumes (revise_query, query) {
}
Consumes (revise_architecture, architecture) {
}
Produces (revise_plant, plant_model) {
}
Produces (revise_control, control_model) {
}
Produces (revise_environment, environment_model) {
}
Produces (revise_query, query) {
}
Produces (revise_architecture, architecture) {
}

Consumes (plant_to_EPN, plant_model) {
}
Produces (plant_to_EPN, plant_EPN) {
}
Consumes (environment_to_EPN, environment_model) {
}
Produces (environment_to_EPN, environment_EPN) {
}
Consumes (control_to_EPN, control_model) {
}
Produces (control_to_EPN, control_EPN) {
}

Consumes (combine_EPN, plant_EPN) {
}
Consumes (combine_EPN, environment_EPN) {
}
Consumes (combine_EPN, control_EPN) {
}
Consumes (combine_EPN, architecture) {
}
Produces (combine_EPN, pn) {
}

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

Consumes (match, reachability_graph) {
}
Consumes (match, query) {
}
Produces (match, reachability_graph) {
}

Consumes (bfs, reachability_graph) {
}