An extensive example

Learning an Alternating Bit Protocol with Smyle

example run





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:

msc0 msc1 msc2 msc3
abp0 abp1 abp2 abp3
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 minus. Note that this list is incomplete:

To be classified as negative:
neg1 neg1 neg2 neg3 neg4
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.
neg5 neg6 neg7 neg8
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 plus:

To be classified as positive:
pos0 pos1 pos2
pos3 pos4 pos5

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 test_model:


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:

msc4 abp4 opencounter

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:
nextpos0 nextpos1 nextpos2 nextpos3
nextpos4 nextpos5 nextpos6 nextpos7

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.