Learning an Alternating Bit Protocol with Smyle

Suppose we are concerned with learning the Alternating Bit Protocol (ABP). We suppose two processes, say p, the producer, and c, the consumer. The producer sends data to the consumer along with a bit that alternates with any acknowledgment that p receives from c. A typical scenario of the ABP is depicted on the left. Here, p starts sending data (from which we abstract here) along with the bit 0 to c until it receives an acknowledgment in terms of a message a. As the data is not corrupted (c is assumed to be able to distinguish between correct and corrupted data), c immediately sends an acknowledgment to p and ignores any further sendings that carry the bit 0. Having received the acknowledgment, p changes the bit and sends new data along with the new bit 1. Again, process c acknowledges the first correct message transfer sending an a back to process p, and so on.

We start Smyle and choose an existential bound 1:

Next, we provide Smyle with some simple example scenarios that we have in mind as positive examples:

ABP0.msc	ABP1.msc	ABP2.msc	ABP3.msc

Then, Smyle starts asking membership queries. We list here some queries that have to be answered negatively by clicking on . Note that this list is incomplete:

To be classified as negative:
We would like to see at least one message exchange.	There is an acknowledgment without having received a message from p.	Process c receives a message without acknowledging it.	Again, process c receives a message (with bit 1) without acknowledging it.	The second acknowledgment is preceded by receiving 0, which had already been acknowledged.

Process p changes the bit without having received an acknowledgment.	Again, process p changes the bit without having received an acknowledgment.	We would like to start with 0.	Process c sends two acknowledgments in a row.

It follows a complete list of scenarios that have to be classified as positive by clicking on :

To be classified as positive:

After 41 user queries and 5333 membership queries, Smyle eventually computes a design model consistent with our classification and asks if we want to test and simulate it, which we confirm by clicking on :

We obtain an automata model that recognizes the 1-bounded linearizations of a represented MSC language and, thus, corresponds to a distributed implementation:

But is this what we really have in mind? Actually, when simulating the automaton, we detect that no linearization is accepted that corresponds to the following MSC, which, however, shall be part of our system and will thus be added:

ABP4.msc

In the following, we will be asked further membership queries, of which we list those that have to be answered positively:

To be classified as positive:

Finally, after 105 user queries and 19276 membership queries, Smyle proposes a refined design model:

Indeed, this model corresponds to what we intended to specify. The automaton recognizes the set of 1-bounded linearizations of the MSC language we had in mind.