A quick tour


This is a short tutorial on how to learn a design model from examples that are given as message sequence charts (MSCs). Smyle should be started with as much RAM as possible. From the console you can start it via the commands:

./start [ammountOfMemory]M Smyle.jar

or

java -jar -Xmx[ammountOfMemory]M Smyle.jar

(e.g., the command

java -jar -Xmx100M Smyle.jar

would start Smyle with 100 Megabytes memory)


Having started Smyle, its main window will open

welcome

Now suppose we have a simple producer-consumer protocol in mind. We might think of two processes, p and q, that communicate through unbounded FIFO buffers. Hereby, p, the producer, provides the consumer process q with an arbitrary number of messages, say of type a. To start learning such a protocol, click on the button start_button . The following menu asks to specify a channel bound, which might be either universal or existential. As we plan to design a protocol with possibly unbounded channels, we choose an existential bound, and we set it to be 2 (note that we learn finite automata that, however, correspond to distributed implementations with possibly unbounded channels; for more information, please consult the technical report):

properties

Now, Smyle asks for one or several example scenarios that will be part of the desired system behavior. In our case, the simplest possible scenario is that of sending one message from p to q. This scenario is represented by the following MSC:

first_msc

To inform Smyle that we consider this MSC to be a possible behavior of our system, we provide a textual description thereof and save it as .msc-file, say prod_cons.msc:

prod_cons

Then, we can add our example MSC to the system by means of the following dialogue:

choose_msc

As we consider our MSC to be an example that is definitely part of our protocol, we declare it positive:

positive

We will then be asked if the following MSC shall be a scenario of our protocol, too:

query1

Let us decide that we would like to have at least one message exchange, so that we discard the proposed MSC by clicking on minus.
In the sequel, we will be asked for membership of the following MSCs:

query2 query3

As both scenarios correspond to what we would like to specify, any of these queries should be answered positively by clicking on plus.
Then, we will be proposed a first design model:

question

By clicking on test_model, we arrive at a window that allows us to test and simulate the computed system, which is given in terms of a finite automaton, recognizing the set of 2-bounded linearizations of some represented MSC language (so that the automaton actually corresponds to a distributed implementation; again, we refer to the technical-report for details):

test

The automaton can now be simulated by choosing an action to be executed. At the same time, a corresponding MSC is displayed:

simulate

As this actually corresponds to a producer-consumer protocol, we are pleased with the result.