Development Tools for Critical Reactive Systems
using the Synchronous Approach
The Verimag Reactive Tool Box

Author Erwan Jahier
Date 2021-03-18 10:08

1 Introduction

Several development tools targeting the design of reactive programs (typically, for critical embedded systems) are made available by the synchronous team of the Verimag laboratory.

The objective of this document is to describe briefly how to install and to use them. This tools set contains tools to


2 Install

There are 4 different tools suites containing Verimag Synchronous tools.

  1. docker: based on a docker image. It requires docker.
  2. V4 binaries : made of pre-compiled binaries gathered in a tarball. It requires to change your environment variables (PATH, LUSTRE_INSTALL, etc.)
  3. V6 binaries: ditto
  4. V6 via opam: integrated in the opam (ocaml) package manager. It requires opam 2.
  5. From sources. The gitlab projects hosting the different tools are accessible from:

    Not all suites contain all tools, as outlined in the table below:

tools \ distributions 2 docker 2 2 V4 binaries 2 2 V6 binaries 2 2 V6 via opam/sources 2
V4 essentials (*) X X X  
V4 full (*) X X    
lv6 X   X X
lutin X   X X
sim2chro X X X  
gnuplot-rif X   X X
luciole-rif X   X  
lurette X   X X
rdbg X     X
lesar X X X  

(*) "V4 essentials" is a sub-set of "V4 full", containing the V4 tools that are really useful to use the V6 tool-set (luciole, gnuplot-rif, sim2chro, etc.).

Hence, to get the complete set of tools, you need to use the docker distribution, or both the "V4 binaries"+the "V6 via opam" ones. As far as OSes are concerned:

OS \ distributions 2 docker 2 2 V4 binaries 2 2 V6 binaries 2 2 V6 via opam 2
linux X X X X
mac os (**) X     X
windows (*) X (via a VM)      

(**) For mac users, to be able to use X11-based tools (luciole, gnuplot-rif, sim2chro, etc.) it is necessary to

  • install xquartz: brew cask install xquartz
  • start it (click in Finder -> Applications)
  • open XQuartz -> Preferences from the menu bar. Go to the last tab, Security, and enable both "Allow connections from network clients" and "Authenticate connections" checkboxes and restart XQuartz.

(*) for windows users, in order to use the docker version via wsl, you still need to install an X server, for instance using mobaxterm.

2.1 The V4 and V6 tools suite via docker

One way to install those tools is via docker. Once docker is installed with X display properly settled (which can sometimes be cumbersome. For mac users using a recent distribution (2018), having X windows working correctly is a bit painful. Here a useful link:, installing the distribution is super easy.

You first need to launch docker with the jahierwan/verimag-reactive-toolbox image, that is available on the docker hub:

docker run -it jahierwan/verimag-reactive-toolbox -e USR_ID=`id -u` -e GRP_ID=`id -g`

The first time, it will download the verimag-reactive-toolbox docker image on the docker hub. Then you will be logged onto a docker machine where all tools are available from the path.

It is very handy to mount your current (host) directory onto some /workdir in the docker image adding something that looks like: -v "$PWD":/workdir -w /workdir to the docker call.

Also, if you want to use tools that make use of graphics (sim2chro, gnuplot-rif, luciole-rif), one can use the following option: -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix. All together, you can therefore use the following command:

docker run -v "$PWD":/workdir -w /workdir  -e USR_ID=`id -u` -e GRP_ID=`id -g` \
  -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
  -it jahierwan/verimag-reactive-toolbox

It is might be easier to have a sh/dockver script accessible from your path and defined as follows:

unameOut="$(uname -s)"
case "${unameOut}" in
    Darwin*) DISPLAY=host.docker.internal:0 ;;

docker run   -e USR_ID=`id -u` -e GRP_ID=`id -g` -v "$PWD":/workdir -w /workdir \
   -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix  \
   -it jahierwan/verimag-reactive-toolbox $@

Such a script can be used like that:

chmod u+x dockver # to do once

to open an interactive session.

Once can also use the binaries provided in this image directly like that:

./dockver lutin -l 10 some_file.lut -o some_trace.rif
./dockver gnuplot-rif some_trace.rif

to remain into your CLI context.

nb: this image embeds an emacs with Lustre and Lutin mode installed:

./dockver emacs somefile.lus

Putting this script somewhere accessible from your PATH migth be convenient too.

2.2 The V4 tools suite via pre-compiled binaries

The V6 tool suite actually (partly) depends on the Lustre V4 tool suite, that therefore needs to be installed too. Binary distributions of the The Lustre V4 for Linux and Mac can be found here:

The Lustre V4 tool set is described in the Lustre V4 Documentation.

2.3 The V6 tools suite via pre-compiled binaries

One can install the V6 distribution via Pre-compiled binaries can be found there :

tar xvfz `arch`-`uname`-lv6-bin-dist.tgz
export LV6_PATH=`pwd`/lv6-bin-dist/
. ./ 

nb: if you need to

  • use the rdbg debugger
  • call lutin or lustre from ocaml

You need to go via the docker or the opam way.

2.4 The V6 tools suite via opam 2

One way to install the V6 distribution is via opam, a package manager for ocaml programs. It should work out of the box with most Linux distributions and OSX (mac). It ougth to work on windows too (follow this link for instructions).

For instance, on ubuntu, installing opam just requires (intructions for other arch):

apt-get update 
apt-get install -y m4 make ocaml ocaml-native-compilers camlp4-extra wget patch unzip bubblewrap git g++ wget opam
opam init -y --jobs=1 --disable-sandboxing
eval $(opam env)
opam switch create 4.11.1 ; eval $(opam env) # optional, just to have a recent ocaml
cp /usr/bin/opam opam/4.11.1/bin/
apt install libgmp-dev m4 perl
opam install -y opam-depext 

In order to obtain the very last version, one can add the verimag opam repo.

# optional
opam repo add verimag-sync-repo ""
opam update -y

And then to install the necessary packages:

opam depext -y lustre-v6  lutin
opam install -y lustre-v6 lutin 

Afterwards, upgrading to the last version of the tools is as simple as:

opam update
opam upgrade

3 Lustre V6

The Lustre V6 language is described in the Lustre V6 Reference Manual. Here we focus on tools.

Sorry, your browser does not support SVG.

Some programs can be found in a dedicated github repo:

3.1 Compiling Lustre V6 programs

The Lustre V6 compiler is named lv6. By default, lv6 produces lic code out of a .lus file (hence its name). lic stands for "Lustre Internal Code". Basically, lic is Lustre V6 with all genericity and syntactic suggar removed.

Consider the content of the edge.lus file:

node edge (X: bool) returns (Y: bool);
 Y = r_edge(X) or r_edge(not(X));
node r_edge (X: bool) returns (Y: bool);
 Y = false -> X and not pre(X);

It is a Lustre program that detects (rising or falling) edges of a Boolean stream. If one wants to generate lic out of this Lustre program, one just need to invoke:

 lv6 edge.lus -lic -n edge 

Note that the -node option (or -n for short), that sets the top-level node, is now mandatory.

lv6 edge.lus -node edge
lv6 edge.lus -n r_edge

Generate lic code is not very useful; generate C code can be done using -2c:

lv6 edge.lus -n edge -2c

3.2 Executing Lustre V6 programs

The call to lv6 edge.lus -node edge -2c not only generates C files: it also generetes a script that can be used to generate a edge.exec binary file. The edge.exec file can be generated directly via the -cc (--compile-generated-c) option.

lv6 edge.lus -node edge -2c -cc 

It is also possible to use the interpreter that is embedded in lv6 via the -exec option.

rm -f edge.rif
lv6 edge.lus -node edge -exec -o edge.rif

In both cases, input data needs to be provided via the keyboard. It is also possible to use a tcl/tk based GUI via luciole-rif:

luciole-rif lv6 edge.lus -node edge -exec
lv6 edge.lus -node edge -2c -cc; luciole-rif ./edge.exec

nb: luciole-rif

3.3 Using the V4 tool set

It is often possible to use the V4 tool set to execute and compile V6 programs, using -lv4 or -ec:

lv6 edge.lus -node edge -lv4 -o edge_v4.lus
lv6 edge.lus -node edge -ec -o

And then you should be able to use the V4 tools set: lus2ec, ecexe, ec2c, ecverif, etc.

4 Lutin

Consider the lutin/range.lut Lutin program:

node range(i:int) returns (y:int) = 
   loop 0 <= y and y <= i

In order to simulate this program, on can use one of the following commands:

lutin range.lut 
lutin range.lut -n range
luciole-rif lutin range.lut 

Here again, the focus is on the basic use of tools, not on the language. More information can be found in this Lutin Tutorial.

More on Lutin


RIF stands for Reactive Input Format. It is the format used between the V4 and the V6 distributions tools to read inputs and write outputs. If you simulate a Lustre (V4 or V6), a Lutin program, or if you use lurette or rdbg, all tools will produce .rif files which follows the RIF conventions.

RIF Data files, that can be visualised with sim2chro or gnuplot-rif.

5.1 Exemple

A RIF file looks like this:

# This is lutin Version 2.26 ("1af0fb6")
# The random engine was initialized with the seed 300035711
#inputs "x":int 
#outputs "y":int 
#step 1
4 #outs 5 
#step 2
5 #outs 6 
#step 3
64 #outs 65 
#step 4
5 #outs 6 
#step 5
4 #outs 5 

It basically contains:

  • comments (preceeded with #)
  • pragmas (particular kinds of comments: '#inputs', '#outputs', '#outs', '#outs', etc.)
  • data (int, bool, float)

5.2 The RIF convention (useful for tool providers)

5.2.1 Data

A RIF file is a sequence of data values separated by spaces, newlines, horizontal tabulations, carriage returns, line feed and form feeds. A data value can be either an integer, a floating-point or a Boolean (t, T, or 1 stands for true ; f, F or 0 stands for false).


Single line comments are introduced by the two character # and terminated by a new line. Multi-line comments are introduced by the two characters #, and terminated by the two characters #@.

5.2.3 Pragmas

Pragmas are special kinds of comments, that migth (or not) be taken into account by tools that reads RIF data. One-line pragmas have the form #pragma_ident, and multi-line pragmas the form #pragma_ident ... #@.

The most common pragmas used by verimag tools are (using BNF notation):

  • #@inputs (<var name> : <var type>)+ #@ or
  • #inputs (<var name> : <var type>)+

to declare the list of input variable names and types;

  • #@outputs (<var name> : <var type>)+ #@ or
  • #outputs (<var name> : <var type>)+

    to declare the list of output variable names and types;

  • #@locals (<var name> : <var type>)+ #@ or
  • #locs

to indicate that the following data correspond to local variables; to declare the list of local variable names and types;

  • #outs, to indicate that the following data correspond to output variables;
  • #step <int>, to indicate that a new step is starting, and that the following data correspond to input variables.

Note that those pragmas are necessary for RIF file viewers such as sim2chro and gnuplot-rif to work properly. Here is another exemple:

#seed = 97040004
#program "lurette chronogram (degradable-sensors.lut) "
#step 1
7.00 7.00 7.00 7.00 #outs T 
#locs 0 0.08 -0.05 -0.05 0.10 
#step 2
7.13 7.20 7.16 7.18 #outs T 
#locs 1 0.13 0.07 0.03 0.05 
#step 3
7.27 7.37 7.27 7.18 #outs T 
#locs 2 0.14 0.10 -0.00 -0.09 
#step 4
7.45 7.47 7.38 7.36 #outs T 
#locs 3 0.18 0.02 -0.07 -0.09 
#step 5
7.59 7.68 7.61 7.56 #outs T 
#locs 4 0.14 0.09 0.02 -0.03 
#step 6
7.65 7.58 7.64 7.55 #outs T 
#locs 5 0.06 -0.06 -0.01 -0.09 
#step 7
7.84 7.91 7.94 7.90 #outs T 
#locs 6 0.20 0.07 0.10 0.06 
#step 8
8.00 8.07 8.00 8.09 #outs T 
#locs 7 0.15 0.07 0.00 0.09 
#step 9
8.12 8.09 8.17 8.16 #outs T 
#locs 8 0.13 -0.03 0.05 0.04 
#step 10
8.26 8.29 8.30 8.20 #outs T

6 sim2chro

In order to graphically display RIF data files via chronograms, you can use sim2chro or sim2chrogtk

sim2chro    -ecran -in edge.rif > /dev/null
sim2chrogtk -ecran -in edge.rif > /dev/null

For more information: sim2chro -help

sim2chro -help

nb : sim2chro and sim2chrogtk are part of the V4 tool set distribution

7 gnuplot-rif

In order or graphically display RIF data files, one can also used gnuplot-rif, that basically pre-process RIF to feed gnuplot:

gnuplot-rif edge.rif

It is possible to hide the display of some variables, using command-line options, or using the .gnuplot-rif resource file.

For more information:

gnuplot-rif -h

8 luciole-rif

luciole-rif generates little TK-based GUIs. Such GUIs allow one to provide input and visualize outputs graphically. luciole-rif can be used with all tools that follows the RIF conventions, such as the Lustre V6 interpreter:

luciole-rif lv6 edge.lus -node edge -exec

The executable produced via C also speaks RIF:

lv6 edge.lus -node edge -2c -cc -o edge
luciole-rif ./edge.exec --debug-me

The Lutin interpreter too:

luciole-rif lutin range.lut 

Try luciole-rif -h more information.

luciole-rif is a wrapper around luciole, which is part of V4 tool set distribution.

9 lurette

-- f.lus
node a_node (X: bool) returns (RE: bool);
 RE = false -> X and not pre(X);
node some_prop(X,RE:bool) returns (res:bool);
  res = true -> (pre(RE) => not(RE)) and (RE => not(pre(RE)));
-- env.lut
node an_env () returns (X: bool) = loop true 

In order to test (during 100 steps) a Lustre node defined in file f.lus (called hereafter the sut, for system under test), against properties defined in the Lustre node some_prop (called hereafter the oracle), and using an environment for N defined by the Lutin node an_env defined in file env.lut (called the environment), one can use lurette as follows:

lurette -sut "lv6 f.lus -n a_node" -env "lutin env.lut -n an_env" \
     -oracle "lv6 f.lus -n some_prop" -l 100

Before running the test, lurette will check that:

  • The set of sut inputs names is included in the set of env outputs names
  • The set of env inputs names is included in the set of sut outputs names
  • The set of oracle inputs names is included in the set of sut and env outputs names

Note that several sut/env/oracle can be used. Any system call that follows the RIF conventions can be used as arguments of -sut, -env, and -oracle.

lurette is actually (now) an alias for rdbg -lurette ; more information can therefore be obtained via rdbg -h.

More on Lurette and automatic testing of Reactive Programs

10 rdbg

If you want to debug the Lustre node N of file f.lus, you can try to do:

rdbg -sut "lv6 f.lus -n a_node"

If an environnement exists for this node on the form of a Lutin program env.lut with node N_env, you can try:

rdbg -sut "lv6 f.lus -n a_node" -env "lutin env.lut -n an_env"

If you want rdbg to skip what occurs in the Lutin program, you can use -env-nd instead -env (-nd stands for no debug):

rdbg -sut "lv6 f.lus -n a_node" -env-nd "lutin env.lut -n an_env"

If you have found a bug using Lurette, you can call the rdbg debugger just like you called Lurette: just replace lurette by rdbg. Note that the oracle can be debugged too. In the following call, only the oracle will be stepped into:

rdbg -sut-nd "lv6 f.lus -n a_node" \
     -env-nd "lutin env.lut -n an_env" \
     -oracle "lv6 f.lus -n some_prop"

More information on rdbg

11 lesar

Lesar is a model-checker of temporal program properties written in Lustre. It is distributed with the V4 tool set (it is also part of the V6 pre-compiled distribution and the docker image). In order to model-check Lustre V6 programs properties, one first needs to translate it into ec or Lustre V4.

-- f.lus
node a_node_satisfy_some_prop (x: bool) returns (res: bool);
var y : bool;
   y = a_node(x);
   res = some_prop(x,y);
node some_prop_on_inputs(x: bool) returns (res: bool);
  res = x -> true; -- true at the first instant
lv6 f.lus -n a_node_satisfy_some_prop -lv4 -o prove_me.lus
lesar  prove_me.lus f__a_node_satisfy_some_prop

lesar actually uses the V4 compiler under the hood to generate an .ec file, which is given to ecverif, which performs the real work.

A different path consists of generating an .ec file with lv6 -ec, and to give the resulting file to ecverif:

lv6 f.lus -n a_node_satisfy_some_prop -ec -o

nb: if you want to prove properties that involve programs with enums, you might want to try the experimental -eeb (–expand-enums-as-bool) option of lv6.

More information on Lesar is available Here.

Note that the kind2 SMT-based model-checker, which works on most Lustre V4 and V6 programs, is worth giving a try if your property involves numeric variables.