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" } Exec print_plant_EPN { name = "epn_print" } Exec print_control_EPN { name = "epn_print" } Exec print_environment_EPN { name = "epn_print" } ForkJoin forkjoin2 {} Exec combine_EPN { name = "combine_EPN" } Exec print_pn { name = "pn_print" } Exec EPN_to_PN { name = "EPN_to_PN" } Exec analyse { name = "reachability" } Exec print_reachability { name = "print_reachability" } ForkJoin forkjoin3 {} Exec matches { name = "matches" } 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, print_plant_EPN) {} Next (environment_to_EPN, print_environment_EPN) {} Next (control_to_EPN, print_control_EPN) {} Next (print_plant_EPN, forkjoin2) {} Next (print_environment_EPN, forkjoin2) {} Next (print_control_EPN, forkjoin2) {} Next (forkjoin2, combine_EPN) {} Next (combine_EPN, print_pn) {} Next (print_pn, analyse) {} Next (analyse, print_reachability) {} Next (print_reachability, 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 (refine_plant, req) { name = "requirements" } Consumes (refine_environment, req) { name = "requirements" } Consumes (refine_control, req) { name = "requirements" } Consumes (refine_query, req) { name = "requirements" } Consumes (refine_plant, plant_model) { name = "plant" } Consumes (refine_environment, environment_model) { name = "environment" } Consumes (refine_control, control_model) { name = "control" } Consumes (refine_query, query) { name = "query" } Produces (refine_plant, plant_model) { } Produces (refine_control, control_model) { } Produces (refine_environment, environment_model) { } Produces (refine_query, query) { } Consumes (plant_to_EPN, plant_model) { name = "plant_model" } Produces (plant_to_EPN, plant_EPN) { } Consumes (environment_to_EPN, environment_model) { name = "environment_model" } Produces (environment_to_EPN, environment_EPN) { } Consumes (control_to_EPN, control_model) { name = "control_model" } Produces (control_to_EPN, control_EPN) { } Consumes (combine_EPN, plant_EPN) { name = "epn_1" } Consumes (combine_EPN, environment_EPN) { name = "epn_2" } Consumes (combine_EPN, control_EPN) { name = "epn_3" } Produces (combine_EPN, pn) { } Consumes (analyse, pn) { name = "pn" } Produces (analyse, reachability_graph) { } Consumes (print_reachability, reachability_graph) { name = "reachability_graph" } Consumes (matches, reachability_graph) { name = "reachability_graph" } Consumes (matches, query) { name = "query" } Consumes (print_plant_EPN, plant_EPN) { name = "epn" } Consumes (print_environment_EPN, environment_EPN) { name = "epn" } Consumes (print_control_EPN, control_EPN) { name = "epn" } Consumes (print_pn, pn) { name = "pn" } }