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


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


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


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:


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:


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


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


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


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:


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


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


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