|
@@ -0,0 +1,293 @@
|
|
|
+include "primitives.alh"
|
|
|
+include "modelling.alh"
|
|
|
+include "object_oeprations.alh"
|
|
|
+
|
|
|
+Composite schedule {
|
|
|
+ {Contains} Success success {}
|
|
|
+ {Contains} Failure failure {}
|
|
|
+
|
|
|
+ {Contains} Atomic add_resource_handler {
|
|
|
+ LHS {}
|
|
|
+ RHS {
|
|
|
+ Post_CDEVS/DEVSInstance post_resource_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "resource_handler"!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "ResourceHandler"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Post_CDEVS/InputPort post_resource_2 {
|
|
|
+ name = "resource_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_resource_1, post_resource_2) {}
|
|
|
+ Post_CDEVS/OutputPort post_resource_3 {
|
|
|
+ name = "resource_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_resource_1, post_resource_3) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll initial {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_init_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_init_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_init_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "Initial"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_init_0, post_init_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_init_2 {
|
|
|
+ name = "control_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_init_1, post_init_2) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll finish {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_finish_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_finish_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_finish_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "Finish"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_finish_0, post_finish_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_finish_2 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_finish_1, post_finish_2) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll activity {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_activity_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_activity_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_activity_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "Activity"!
|
|
|
+ $
|
|
|
+ value_parameters = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "[" + cast_value(read_attribute(model, mapping["0"], "name")) + ", " + cast_string(read_attribute(model, mapping["0"], "distribution")) + "]"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_activity_0, post_activity_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_activity_2 {
|
|
|
+ name = "resource_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_activity_1, post_activity_2) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_activity_3 {
|
|
|
+ name = "resource_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_activity_1, post_activity_3) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_activity_4 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_activity_1, post_activity_4) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_activity_5 {
|
|
|
+ name = "control_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_activity_1, post_activity_5) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll parallelsplit {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_split_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_split_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_split_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "ParallelSplit"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_split_0, post_split_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_split_2 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_split_1, post_split_2) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_split_3 {
|
|
|
+ name = "control_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_split_1, post_split_3) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll synchronization {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_sync_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_sync_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_sync_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "Synchronization"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_sync_0, post_sync_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_sync_2 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_sync_1, post_sync_2) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_sync_3 {
|
|
|
+ name = "control_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_sync_1, post_sync_3) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll xor {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_xor_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_xor_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_xor_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "ExclusiveChoice"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_xor_0, post_xor_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_xor_2 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_xor_1, post_xor_2) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_xor_3 {
|
|
|
+ name = "control_out1"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_xor_1, post_xor_3) {}
|
|
|
+ Post_CDEVS/OutputPort post_xor_4 {
|
|
|
+ name = "control_out2"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_xor_1, post_xor_4) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ {Contains} ForAll merge {
|
|
|
+ LHS {
|
|
|
+ Pre_PM/Initial pre_merge_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
+ RHS {
|
|
|
+ Post_PM/Initial post_merge_0 {
|
|
|
+ label = "0"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstance post_merge_1 {
|
|
|
+ label = "1"
|
|
|
+ value_name = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return read_attribute(model, mapping["0"], "name")!
|
|
|
+ $
|
|
|
+ value_type = $
|
|
|
+ String function value(model : Element, name : String, mapping : Element):
|
|
|
+ return "SimpleMerge"!
|
|
|
+ $
|
|
|
+ }
|
|
|
+ Trace (post_merge_0, post_merge_1) {}
|
|
|
+
|
|
|
+ Post_CDEVS/InputPort post_merge_2 {
|
|
|
+ name = "control_in"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_merge_1, post_merge_2) {}
|
|
|
+
|
|
|
+ Post_CDEVS/OutputPort post_merge_3 {
|
|
|
+ name = "control_out"
|
|
|
+ }
|
|
|
+ Post_CDEVS/DEVSInstanceToPort (post_merge_1, post_merge_3) {}
|
|
|
+ }
|
|
|
+ }
|
|
|
+}
|