Fix specification of message_out_bs
The specification of the basic machine does not match its implementation, at least for the operations:
- message_out_bs__alloc_req_msg
- message_out_bs__alloc_resp_msg
In the case of the memory allocation failure, the specification promises more than is actually implemented in the C code.