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) {} }