|
@@ -0,0 +1,288 @@
|
|
|
+Start start {}
|
|
|
+Finish finish {}
|
|
|
+
|
|
|
+Exec revise_req {
|
|
|
+ name = "models/revise_req"
|
|
|
+}
|
|
|
+Exec make_initial_models {
|
|
|
+ name = "models/make_initial_models"
|
|
|
+}
|
|
|
+
|
|
|
+Fork fork1 {}
|
|
|
+
|
|
|
+Exec revise_plant {
|
|
|
+ name = "models/revise_plant"
|
|
|
+}
|
|
|
+Exec revise_environment {
|
|
|
+ name = "models/revise_environment"
|
|
|
+}
|
|
|
+Exec revise_control {
|
|
|
+ name = "models/revise_control"
|
|
|
+}
|
|
|
+Exec revise_query {
|
|
|
+ name = "models/revise_query"
|
|
|
+}
|
|
|
+Exec revise_architecture {
|
|
|
+ name = "models/revise_architecture"
|
|
|
+}
|
|
|
+
|
|
|
+Exec plant_to_EPN {
|
|
|
+ name = "models/plant_to_EPN"
|
|
|
+}
|
|
|
+Exec environment_to_EPN {
|
|
|
+ name = "models/environment_to_EPN"
|
|
|
+}
|
|
|
+
|
|
|
+Exec control_to_EPN {
|
|
|
+ name = "models/control_to_EPN"
|
|
|
+}
|
|
|
+
|
|
|
+Join join2 {}
|
|
|
+
|
|
|
+Exec merge_EPN {
|
|
|
+ name = "models/merge_EPN"
|
|
|
+}
|
|
|
+
|
|
|
+Exec combine_EPN {
|
|
|
+ name = "models/combine_EPN"
|
|
|
+}
|
|
|
+
|
|
|
+Exec EPN_to_PN {
|
|
|
+ name = "models/EPN_to_PN"
|
|
|
+}
|
|
|
+
|
|
|
+Exec analyse {
|
|
|
+ name = "models/reachability"
|
|
|
+}
|
|
|
+
|
|
|
+Join join3 {}
|
|
|
+
|
|
|
+Exec match {
|
|
|
+ name = "models/match"
|
|
|
+}
|
|
|
+
|
|
|
+Exec bfs {
|
|
|
+ name = "models/bfs"
|
|
|
+}
|
|
|
+
|
|
|
+Exec reachability_print {
|
|
|
+ name = "models/reachability_graph_print"
|
|
|
+}
|
|
|
+
|
|
|
+Decision found {}
|
|
|
+
|
|
|
+Data req {
|
|
|
+ name = "requirements"
|
|
|
+ type = "formalisms/Requirements"
|
|
|
+}
|
|
|
+Data plant_model {
|
|
|
+ name = "plant_model"
|
|
|
+ type = "formalisms/PW_Plant"
|
|
|
+}
|
|
|
+Data environment_model {
|
|
|
+ name = "environment_model"
|
|
|
+ type = "formalisms/PW_Environment"
|
|
|
+}
|
|
|
+Data control_model {
|
|
|
+ name = "control_model"
|
|
|
+ type = "formalisms/PW_Control"
|
|
|
+}
|
|
|
+Data plant_EPN {
|
|
|
+ name = "plant_EPN"
|
|
|
+ type = "formalisms/Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Data control_EPN {
|
|
|
+ name = "control_EPN"
|
|
|
+ type = "formalisms/Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Data environment_EPN {
|
|
|
+ name = "environment_EPN"
|
|
|
+ type = "formalisms/Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Data pn {
|
|
|
+ name = "pn"
|
|
|
+ type = "formalisms/PetriNet"
|
|
|
+}
|
|
|
+Data reachability_graph {
|
|
|
+ name = "reachability"
|
|
|
+ type = "formalisms/ReachabilityGraph"
|
|
|
+}
|
|
|
+Data query {
|
|
|
+ name = "query"
|
|
|
+ type = "formalisms/Query"
|
|
|
+}
|
|
|
+Data architecture {
|
|
|
+ name = "architecture"
|
|
|
+ type = "formalisms/Architecture"
|
|
|
+}
|
|
|
+Data merged_EPN {
|
|
|
+ name = "merged_EPN"
|
|
|
+ type = "formalisms/Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+
|
|
|
+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, merge_EPN) {}
|
|
|
+Next (merge_EPN, 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, reachability_print) {}
|
|
|
+Next (reachability_print, finish) {}
|
|
|
+
|
|
|
+Consumes (revise_req, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+Produces (revise_req, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+
|
|
|
+Produces (make_initial_models, plant_model) {
|
|
|
+ name = "PW_Plant"
|
|
|
+}
|
|
|
+Produces (make_initial_models, environment_model) {
|
|
|
+ name = "PW_Environment"
|
|
|
+}
|
|
|
+Produces (make_initial_models, control_model) {
|
|
|
+ name = "PW_Control"
|
|
|
+}
|
|
|
+Produces (make_initial_models, query) {
|
|
|
+ name = "Query"
|
|
|
+}
|
|
|
+Produces (make_initial_models, architecture) {
|
|
|
+ name = "Architecture"
|
|
|
+}
|
|
|
+Produces (make_initial_models, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (revise_plant, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+Consumes (revise_environment, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+Consumes (revise_control, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+Consumes (revise_query, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+Consumes (revise_architecture, req) {
|
|
|
+ name = "Requirements"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (revise_plant, plant_model) {
|
|
|
+ name = "PW_Plant"
|
|
|
+}
|
|
|
+Consumes (revise_environment, environment_model) {
|
|
|
+ name = "PW_Environment"
|
|
|
+}
|
|
|
+Consumes (revise_control, control_model) {
|
|
|
+ name = "PW_Control"
|
|
|
+}
|
|
|
+Consumes (revise_query, query) {
|
|
|
+ name = "Query"
|
|
|
+}
|
|
|
+Consumes (revise_architecture, architecture) {
|
|
|
+ name = "Architecture"
|
|
|
+}
|
|
|
+Produces (revise_plant, plant_model) {
|
|
|
+ name = "PW_Plant"
|
|
|
+}
|
|
|
+Produces (revise_control, control_model) {
|
|
|
+ name = "PW_Control"
|
|
|
+}
|
|
|
+Produces (revise_environment, environment_model) {
|
|
|
+ name = "PW_Environment"
|
|
|
+}
|
|
|
+Produces (revise_query, query) {
|
|
|
+ name = "Query"
|
|
|
+}
|
|
|
+Produces (revise_architecture, architecture) {
|
|
|
+ name = "Architecture"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (plant_to_EPN, plant_model) {
|
|
|
+ name = "PW_Plant"
|
|
|
+}
|
|
|
+Produces (plant_to_EPN, plant_EPN) {
|
|
|
+ name = "Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Consumes (environment_to_EPN, environment_model) {
|
|
|
+ name = "PW_Environment"
|
|
|
+}
|
|
|
+Produces (environment_to_EPN, environment_EPN) {
|
|
|
+ name = "Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Consumes (control_to_EPN, control_model) {
|
|
|
+ name = "PW_Control"
|
|
|
+}
|
|
|
+Produces (control_to_EPN, control_EPN) {
|
|
|
+ name = "Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (merge_EPN, environment_EPN) {
|
|
|
+ name = "EPN_Environment"
|
|
|
+}
|
|
|
+Consumes (merge_EPN, control_EPN) {
|
|
|
+ name = "EPN_Control"
|
|
|
+}
|
|
|
+Consumes (merge_EPN, plant_EPN) {
|
|
|
+ name = "EPN_Plant"
|
|
|
+}
|
|
|
+Produces (merge_EPN, merged_EPN) {
|
|
|
+ name = "Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (combine_EPN, merged_EPN) {
|
|
|
+ name = "Encapsulated_PetriNet"
|
|
|
+}
|
|
|
+Consumes (combine_EPN, architecture) {
|
|
|
+ name = "Architecture"
|
|
|
+}
|
|
|
+Produces (combine_EPN, pn) {
|
|
|
+ name = "PetriNet"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (analyse, pn) {
|
|
|
+ name = "PetriNet"
|
|
|
+}
|
|
|
+Produces (analyse, reachability_graph) {
|
|
|
+ name = "ReachabilityGraph"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (match, reachability_graph) {
|
|
|
+ name = "ReachabilityGraph"
|
|
|
+}
|
|
|
+Consumes (match, query) {
|
|
|
+ name = "Query"
|
|
|
+}
|
|
|
+Produces (match, reachability_graph) {
|
|
|
+ name = "ReachabilityGraph"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (bfs, reachability_graph) {
|
|
|
+ name = "ReachabilityGraph"
|
|
|
+}
|
|
|
+
|
|
|
+Consumes (reachability_print, reachability_graph) {
|
|
|
+ name = "ReachabilityGraph"
|
|
|
+}
|