Title: Model checking a modular-structured nonblocking atomic commitment protocol for asynchronous distributed systems