Fiacre: Working with a Fiacre Model

In this tutorial, we explain how to generate the state space of a model defined using the Fiacre language and perform model-checking using the selt model-checker provided with Tina.

1. Generating a TTS directory from a Fiacre file using frac

The first step is to compile the Fiacre specification into a Time Transition System (TTS) suitable for analysis by the Tina tools. We assume that the Fiacre program is in a file named <infile>.fcr.

        frac [options] <infile>.fcr <outfile>.tts

The frac compiler offers several options that can be viewed using the -help command flag: frac [-h | -help]. The following options are recognized (more information can be found in the USAGE file provided in the distribution):

-h / -help	a short description of command line flags
-q	in quiet mode [default]
-v	in verbose mode
-o <errfile>	sets the file for error stream (default stderr)
-f	does not compile, but check the validity of the Fiacre source file and pretty-prints the code .

The command frac <infile>.fcr <outfile>.tts, checks the contents of file <infile>.fcr and generates a TTS description in <outfile>.tts. A TTS description is a directory containing two files:

<outfile>.net, containing the description of a Time Petri Net with priority using the .net format (the net can be rendered using the nd editor and simulator tool provided with Tina);
<outfile>.c, containing a description of the data processing actions associated to the net. This is a C file that uses the TTS API required by Tina.

2. Compiling the TTS description

For analysis by Tina, the file <outfile>.tts/<outfile>.c must be compiled into a shared library (extension .so on Linux/Unix, .dylib on Mac, .dll on Windows). The frac distribution provides a Makefile for this task. The code generated requires gcc as C compiler. We assume that there is an environement variable, FIACREPATH, whose value is the directory containing the local Fiacre distribution.

        make -B -f ${FIACREPATH}/Makefile  LIBHOME=${FIACREPATH}/lib/ NAME=<infile>

3. Generating the state space using tina

tina is a command line tool that builds various state space abstractions for Petri nets, Time Petri nets and Time Transition System description in .tts format. It is possible to use tina to generate the state space of a TTS in the ktz format, that is a compressed, binary format for kripke transition system. That compact format is the input format of selt (the tina SE-LTL model checker) and other forthcoming tools.

        tina [options] <infile>.tts <outfile>.ktz

The ktzio tool can be used to convert a ktz file between several formats or to print the result on the standard output. The formats manipulated are the following:

Table 1. Ouput formats for ktzio
name	file ext	description
ktz	.ktz	tina compact binary format
bcg	.bcg	CADP compact binary format
aut	.aut	CADP aldebaran format
mec	.mec	Mec4 model checker format
textual	.txt	textual descriptions

4. Using the selt model-checker on a ktz file

selt is a model-checker for state-event LTL formulas on a kripke transition system given in ktz format. If some formula is specified (by flag -f or by providing a formula in a file), then the result of evaluation of the formula is printed according to the output mode and verbosity flags, and selt exits. If no formulafile is specified, then selt starts an interactive session, evaluating commands entered by the user on standard input (see the selt manpages). For example, to check the absence of deadlocks, we can use the following command:

        selt <infile>.ktz  -f "[] - dead"

Sources

Frac sources are available in licence CECILL-B and precompiled distributions for various targets are available at: http://www.laas.fr/fiacre

The Tina Toolbox homepage: http://www.laas.fr/tina