Last update: March 14, 2005.
Teacher: J.F. Groote.
setenv CLASSPATH .:/home/amathijs/bin/grappa1_2.jar
This is also necessary to let the `Graph' button in msim work. For using graphical programs from a windows machine or a macOs based machine, a X-server must be installed. Logging at the svstud can be done using a secure shell.
All the programs reside in the directory /home/jfg/bin. Example files are in /home/jfg/share/mCRL/examples. In case of problems contact J.F.Groote@tue.nl. Most tools have a -help flag that gives a concise description of the tool and its use. All tools, except the simulator (msim) are command line driven. Many tools print their output to stdout, such that their results can be piped into other tools.
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 manual pages for the mCRL toolset are online. See the new manpages for the mCRL toolset.
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 Caesar/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 Caesar/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 Caesar Aldebaran is particularly useful for verifying modal formulas, using the evaluator tool. There are several helpful webpages describing this tool. Expecially useful is this page on patterns of modal formulas, which helps in formulating the modal formulas. There is also an overview of all tools.
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.