## An extensive example

# Learning an Alternating Bit Protocol with Smyle

Suppose we are concerned with learning the Alternating Bit Protocol (ABP). We suppose two processes, say |

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.