Last update: March 22, 2005
Teachers: J.F. Groote and J.C. van de Pol.
A Linux/MacOs/Unix version of this toolset can be obtained at the mcrl home page. This tool also runs on window machines under Cygwin (see mCRL for Windows). Installation of the toolset goes by following the instructions in the INSTALL file. In case of problems contact Bert Lisser (bertl@cwi.nl) with a clear and concise description of the problem.
The most important commands are mcrl, that checks the syntax and typing of a mcrl specification. With the flag -tbf, -regular or -regular2 a linear specification is generated into a compressed .tbf format. A known bug in mcrl is that it cannot deal with terminating processes. In case of non explainable crashes termination is often the problem.
The tool pp can be used to transform a .tbf file to readable text. The tool msim can simulate a specification. Instantiator can generate a statespace. Tools as constelm, parelm, structelm, invelm, confelm reachelm and others can be used to reduce the complexity of .tbf files.
It is also possible to use the Ceasar/Aldebaran toolset. This tool is also available on the svstud.win.tue.nl. In order to use the tool, the following commands must be executed when logging in. For bash:
export CADP=~jfg/CADP
export CADP_LANGUAGE=english
CADP_ARCH=`$CADP/com/arch`
PATH=$CADP/bin.$CADP_ARCH:$CADP/com:$PATH
For csh:
setenv CADP ~jfg/CADP
setenv CADP_LANGUAGE english
set CADP_ARCH=`$CADP/com/arch`
set path=($path $CADP/bin.$CADP_ARCH $CADP/com)
The home page of the Ceasar/Aldebaran toolset provides lots of information, including the possibility to download the tool. For this a separate (free) license must be acquired, which is a hairy procedure, generally taking several weeks. A compiled and ready to run version of this toolset can be found in ~jfg/CADP/com.
The second way is by generating a .svc file, using the flag -svc in the instantiator. Using lts2dot, and subsequently dot -Tps file.dot > file.ps a picture in postscript format can be generated. The dot program can be found in the directory /home/jfg/bin.
The third way is by using the FSM visualizer of Frank van Ham. This gives by far the most spectacular results. This visualiser can be used by strating the program startfsm in the directory /home/jfg/bin. The program svc2fsm can be used to translate a svc file to a file readable for start fsm. If the -svc-term flag is used in the instantiator, svc2fsm file.svc file.tbf generates on stdout a .fsm file, from which in the tool values of variables can be inspected. The FSM visualiser is available for windows and linux machines and requires a decent graphics card. This program is also freely available. It can be found in the directories of Frank van Ham. Here also many visualised transition systems of various applications can be found.