|
@@ -0,0 +1,41 @@
|
|
|
+include "primitives.alh"
|
|
|
+
|
|
|
+A B {
|
|
|
+ Composite schedule {
|
|
|
+ {Contains} Success success {}
|
|
|
+ {Contains} Failure failure {}
|
|
|
+ {Contains} Atomic init_ports {
|
|
|
+
|
|
|
+ }
|
|
|
+ {Contains} ForAll create_states {
|
|
|
+
|
|
|
+ }
|
|
|
+ {Contains} ForAll command_transition {
|
|
|
+
|
|
|
+ }
|
|
|
+ {Contains} ForAll check_object {
|
|
|
+
|
|
|
+ }
|
|
|
+ {Contains} ForAll detect {
|
|
|
+
|
|
|
+ }
|
|
|
+ {Contains} ForAll remove_detect {
|
|
|
+
|
|
|
+ }
|
|
|
+ }
|
|
|
+ Initial (schedule, init_ports) {}
|
|
|
+
|
|
|
+ OnSuccess (init_ports, create_states) {}
|
|
|
+ OnSuccess (create_states, command_transition) {}
|
|
|
+ OnSuccess (command_transition, check_object) {}
|
|
|
+ OnSuccess (check_object, detect) {}
|
|
|
+ OnSuccess (detect, remove_detect) {}
|
|
|
+ OnSuccess (remove_detect, success) {}
|
|
|
+
|
|
|
+ OnFailure (init_ports, create_states) {}
|
|
|
+ OnFailure (create_states, command_transition) {}
|
|
|
+ OnFailure (command_transition, check_object) {}
|
|
|
+ OnFailure (check_object, detect) {}
|
|
|
+ OnFailure (detect, remove_detect) {}
|
|
|
+ OnFailure (remove_detect, success) {}
|
|
|
+}
|