TorX Tutorial

In this section we give a tutorial about two TorX Examples. The first example is about coffee machines. We present a small, easy to understand, model of a coffee machine. You will get comfortable with the xtorx user-interface. The second example is about a chat-box protocol implementation called the conference protocol. This example is more complex but the example itself is straight forward.

For this tutorial we assume that the TorX tool and its examples are installed propperly. If not fix this first! See the section about installing TorX and TorX Examples.

NOTE!: With the abbreviation $TE we refer to the (root) directory where the TorX Examples are installed.

Coffee machines

Consider the labelled transition system, given in Figure 2, specifying a coffee machine. The label button is an input; coffee, espresso and cappuccino are outputs. (L_I = { button }, L_U = { coffee, espresso, cappuccino }).

Figure 2: Coffee machine as labelled transition system

The coffee machine specified in Figure 2 is a labelled transition system. This coffee machine delivers coffee, espresso or cappuccino depending on how many times the button is pressed. If the button is pressed only once (and the system was in its initial state) the machine may decide to deliver espresso or coffee. Both are possible because the system is either in state 1 or in state 3. You can check this by following all outgoing arrows labelled button in state 0. When the button is pressed again and neither coffee nor espresso was delivered it may decide to produce espresso, coffee or cappuccino. When the button is pressed more then twice (and no output was delivered) the machine deliveres coffee, espresso or cappuccino, eventually.

A textual version of labelled transition system in Figure 2 can be found in the TorX Example distribution ($TE/coffee/SPEC/SOURCE/spec1.aut). The .aut files are expressed in the so-called Aldebaran format. A labelled transition system in .aut-format is simply a list of transitions with source state - transition label - destination state. The first line of an .aut-file specifies (from left to right) the initial state, the number of transitions, and the number of states. Below we give the .aut-file content representing Figure 2:

des (0, 8, 4)
(0,      button,  1)
(0,      button,  3)
(1,      button,  2)
(2,  cappuccino,  0)
(3,      button,  2)
(3,      button,  3)
(3,    espresso,  0)
(3,      coffee,  0)

To experiment with this example you'll need the Caesar/Aldebaran Development Package (CADP). This package is required to compile the Aldebaran source into a TorX Primer. The Eucalyptus tool is part of the CADP package. With it you can view an .aut-file by calling xeuca &. Click with the left mouse button on the .aut-file you would like to see and select Visualize->Edit. Subsequently you may have to move the objects a little bit in order to obtain a readable transition system.

One of the TorX tool components is the simulator. With the simulator we can imitate a real implementation given a Aldebaran file. In the same directory $TE/coffee/SPEC/SOURCE/ you can find five files: impl1 to impl5. These files are just Aldebaran files but are interpreted by the simulator as coffee machine implementations. The simulator makes the approach to compair and relate the specification and the implementation very easy because both are expressed in the same Aldebaran modeling language. As a consequence we can test each Aldebaran against itself.

To be able to play with the coffee example you should have installed the TorX distribution and also the TorX Example distribution. The latter is a collection of several examples. For the coffee example you should also need Caesar Aldebaran Development Package (CADP) otherwise you are not able to generate the TorX Primers. Ofcourse, for this example you need only the coffee example from the TorX Example distribution. When everything is working properly you can start xtorx & at the commandline. Note that the bin directory of the TorX distribution is in your default search path. You should get something like:

Here you see the GUI of TorX called xtorx. It is an optional component of the Test Tool TorX. It optional because its also possible to use a commandline interface which is more flexible (and simple) for interoperability reasons.

In the titel of xtorx you'll see the name of TorX and its version number. Directly below there is a menu bar. The most interesting entries are File, Primers and Mutants. As we will see in a moment the File menu is used to select the desired configuration file. The other two Primers and Mutants are used between different specification and implementations, respectively. Alternatively you can view the source of the specification (Primer) or implementation (Mutants) by using the View menu.

The first step is loading the configuration of the coffee example into xtorx. Select and open the coffee configuration file with the File->Open Configuration... option. The coffee example configuration file is located at the TorX Example distribution ($TE/coffee/coffee.if). Note the changes in the titel bar of the GUI. This is the place where to look if you want to know which configuration, primer and/or mutants is selected.

The second step is selecting the Primer spec1 from the Primer menu and the Mutant impl1 from the Mutant menu. Now it is a good time to view the source (View->Primer source or View->Mutant source). You should get something what you see below:

The implementation is missing one state and two transitions with respect to the specification. Does this influence the intended behaviour? With TorX we can check (test) the ioco relation. So, press the start button and TorX activates the initial steps. This is what you'll see:

Xtorx starts always in manual mode. To activate the automatic mode you must click the Auto checkbox and Torx will start immediatly. After a while you are getting tired and want to stop the testing proces. By clicking the stop button the test process is stopped. If you want to go to manual mode you have to click the Manual checkbox. You have to stop the testing process if you want to change Primer or Implementation and you probably see something like:

The part of the GUI, below the verdict bar, displays a lot of messages. These messages are more or less used for debugging purposes and less interesting for this case study in specific. When something goes wrong you usually can find here some messages about the error.

The part of the GUI, below the menu bar and above the 'current state offers' you see the executed trace. The trace is 27265 steps long.

The midsection of the GUI is used for steering the test process manually. You can choose input- or an output action. An output action does an observation from the implementation. The observed event should be listed in the output menu (otherwise something went wrong!). An input action which chosen from the input menu is send (stimulated) to the implementation. There are also some random buttons to let the system make the decides what to do next.

This is already the end of this coffee example. You can ofcourse still play a little bit with it. For example, select one of the other implementations (impl2..impl5). Which of them are according to the TorX Test Tool incorrect, if you test them against the specfication spec1?

Chat boxes (conference protocol)

This section presents a tutorial of the conference protocol which is a chat-box program where user can join a named conference and exchange messages with each other. In the first part we demonstrate a chat session with three conference protocol users talking together.

The second part we show how to test one entity (read:user) of the conference protocol in a test context with two other users.

Short 'live' chat demo...

With the conference protocol example (confprot) a script confprot-demo.sh which start up three conference protocol entities (cpe) (including user-cpe interface). Below you see the initial screens of the three users. The titel in of the console tells you which user the console represents.

The lines of text in each console say something about the configuration of the implementation. One of the options says that we are using the USER_INTERFACE. This means that on top of the conference prtogram entity (cpe) there is a small piece of software that forms the interface between the cpe and the user.

Lets assume the user ONE starts a conference named chatbox and immediately after that she/he send a message to the chatbox conference "Hello, anybody alive?". This is what all users observe:

Ofcourse none of the two other users see the message which was send by user ONE because user TWO and user THREE are not participants of the chatbox conference.

The next step the user TWO joins the same conference and sends the message "Hello, somebody there?". This is what we observe from the user consoles:

User ONE receives the messages and replies with the following message "Yes, I'm here!" which is also received by TWO. Then user THREE is also joining the conference chatbox but he/she is not sending a message. User TWO is replying on the message of user ONE and sends the message "Well, that's nice, then I'm not alone...". And as you can see below the message is also received by user THREE.

You may noticed that user THREE used the letter 'j' instead of 'join'. The first letter is enough to discriminate the command. In fact it has the 'send' command as the default one. So any other command starting with character except 'j', 'l', 'q' (and 'r') will be interpreted as 's'.

Then user ONE replies with "It is always nice to chat with others!" and the message is transmitted to all three users. User THREE replies with "I agree, that it is nice to chat". Also this message is received by all three users.

Then something urgent happened and user TWO has to leave this conference and joins into another conference called 'coffee' where he sends a message "hello". And, ofcourse the other users do not receive this message because its a different conference. We can observe the following consoles:

Then says user ONE hello to user THREE and sends the message "Hello THREE, how are you?". This is ofcourse received by user THREE but not by user TWO because he/she's in a different conference. At this time user THREE is leaving the chatbox conference as well and joins the coffee conference and inquires "Anybody here?" This message is received by user TWO who replies with "Yes, but I'm going back to chatbox, cu."

The user TWO leaves the coffee conference and join the old chatbox conference but with a different username "2". After that he sends a messages "Hello, I'm back!". The user THREE is leaving the conference and he/she stops chatting. At this time the status of the three consoles is:

User ONE is happily surprised and welcomes him/her "Welcome back 2, or shoud I say TWO?". User 2 does not reply and leaves the conference. And after some time user ONE leaves as well.

(to be continued...)

Prev	Table of Contents	Next
Chapter 7: TorX examples		Chapter 9: Conference Protocol Case Study