Alternating Bit Protocol
Problem
specification:
The
fault-intolerant program consists of two processes: a sender and a receiver. The
sender reads from an infinite input stream of data packets and sends the newly
read packet to the receiver. The receiver copies each received packet into an
infinite output stream. When the sender sends a data packet, it waits for an
acknowledgement from the receiver before it sends the next packet. Also, when
the receiver receives a new data packet, it sends an acknowledgment bit back to
the sender. A one-bit message header suffices to identify the data packet
currently being sent since at every moment there exists at most one
unacknowledged data packet. Using this identifier bit, the sender (respectively,
the receiver) does not need count the total number of packets sent
(respectively, received).
The input text file to our synthesis framework.
The description of the example.