|
@@ -0,0 +1,251 @@
|
|
|
+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"
|
|
|
+ }
|
|
|
+}
|