| [ Home | What's New | Contents | Overview | Contributors | Distribution | Examples | Documentation | Manual | Publications | Mailing List Archive | Problems ] | This page was last updated by Axel Belinfante on 2006-06-30 | |
| TorX Test Tool Information | ||
| Prev | Next | |
The distribution of TorX consists of a gnuzipped tar archive. It contains all source files to generate the TorX tool set. First you have to obtain the TorX distribution. Unzip the archive and extract the tar archive. Read the READMEs and the INSTALL text files in the distribution for the latest installation details.
The test tool TorX is an academic prototype research tool and as it is now not ready for commercial use but can be usefull to test small to medium sized programs automatically. However, it may require some time to develop the specification and the Test Context before you can actually start testing.
The TorX Test Tool runs on unix/linux based machines. We ourselves have worked with Sun Solaris and Linux. Recently we have made things work on Mac OS X (Darwin) too. During one of the case studies we noticed that HP unix machine had some limitations. We have tried to port the distribution to Windows in (for example) a Cygwin environment.
Last time we tried is a while ago. To our experience, TorX 3.2.0 can be run on windows, if a (recent?) Cygwin enviroment is available there. We tried cygwin version 1.3.22, installed and configured such that we can also use CADP (see below). Note that also the TorX examples distribution needed updates to run (via cygwin) on windows -- you will need torx-examples version 3.2.
If you want to install cygwin for torx, and use it with CADP, then, please note that CADP imposes particular constraints on how you install cygwin, so please read first the CADP Cygwin installation and configuration notes in the CADP Windows Installation page before you start installing cygwin.
On windows (with cygwin) have a look at Tcldot for Windows which hopefully makes it easier to get the animation working.
To install the TorX Test Tool you need the following software. The numbers list the version(s) we used. Other versions may work as well. The configure script (that you have to run as part of the installation procedure) will check for the presence of these on your system (as far as they are needed during the installation process)
Tk is only required for the grafical user interface (xtorx). Although it is very well possible to use the command line interface (torx), we mostly use it in shell scripts, and use the gui for interactive work. Note that TorX versions prior to 3.2.0 used expectk for xtorx; from 3.2.0 on we just need tcl/tk (wish).
The CADP package is needed to compile LOTOS and ``binary coded graph'' specifications (.lot and .bcg) to the CADP primer/explorers. (It might be required to flatten certain LOTOS specifications (i.e.their ADT's) with a conversion utility, that we hope to distribute soon as part of an updated version of (Mini)Lite). Note that TorX versions prior to 3.5.0 needed CADP also for Aldebaran (.aut) files; from 3.5.0 on we instead use our own autexp(1) explorer, which allows us to animate the automaton during testing using anifsm.
The mcrl and mcrl2 packages are needed to create primer/explorers for mCRL (.mcrl) and mCRL2 (.mcrl2) files. For mCRL2 (.mcrl2) files only the mcrl2 package is needed (from which we use tools mcrl22lpe and lpe2torx) -- for mCRL (.mcrl) we need both packages (because we use tool mcrl from the mcrl package to generate .tbf, and translate that .tbf to .lpe with tool tbf2lpe from the mcrl2 package, after which we use tool lpe2torx to explore the .lpe). This is still rather new, in particular lpe2torx, so, even though things work, it may need your feedback to helpt it to stabilize.
The (Mini)Lite package is needed to run the CONFPROTSYMBOLIC example. This component is more efficient with memory at some expense of computer power. Unfortunately, the example needs a newer version of (Mini)Lite than the one that is currently available to the public; we hope to update the (Mini)Lite distribution ``sometime soon''.
The LTSA package is needed for the FSP examples.
The lts (FSP) explorer in TorX uses the LTSA package to do the work. The java and javac package is needed for LTSA.
Some of the TorX tool components are implemented using Kimwitu. This means that only when you change these tools, you need kimwitu to regenerate the (source) code.
GraphViz, or to be more concrete, its editor component dotty, and its Tcldot Tcl package are used by TorX components jararacy resp. anifsm to visualize (animate) the exploration of automatons. For example, the automaton generated from test purposes by jararaca or the automaton in the Aldebaran (.aut) files, as is demonstrated in the conference protocol resp. the coffee machines example in the examples distribution. Nowadays anifsm (and thus Tcldot) is preferred over jararacy (which needed dotty). Recently anifsm was extended with graphical editing and writing of the automaton to file in Aldebaran (.aut) format, which effectively turns anifsm into a simple graphical editor to create automata in Aldebaran (.aut) format.
GNU plot is used to visualize the implementation code coverage measurement results for the conference protocol implementation in the examples distribution.
The installation procedure is the (common) three step process:
In the first step ``configure'' prepares the generation fase (step 2). It determines the hardware and software that you have installed and it creates all intermediate scripts and makefiles. In the second step everything is compiled that needs to be compiled. Now your distribution contains also all compiled executables, etc. In the last step, the third step, these are copied to the installation location specified as a configure parameter at step 1. After you have installed TorX you should add the ``bin'' sub-directory of the installation directory to your PATH environment. For detailed info about the parameters see the README in the distribution.
| Prev | Table of Contents | Next |
| Chapter 4: Downloading TorX |
|
Chapter 6: Using TorX |