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

Author Erwan Jahier
Date 2018-07-11 10:11

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

lustre.png

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.

    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 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, sim2chro).

2.1 The V4 and V6 tools suite via docker

The simplest way to install those tools is via docker. You first need (of course) to install docker and then launch it in your CLI using the jahierwan/verimag-sync-tools image available in the docker hub:

docker run -it jahierwan/verimag-sync-tools

The first time it will download the verimag-sync-tools 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 --user `id -u`. 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 DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
  -it jahierwan/verimag-sync-tools

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

docker run  --user `id -u` -v "$PWD":/workdir -w /workdir \
   -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix  \
   -it jahierwan/verimag-sync-tools $@

Such a script can be used like that:

dockver

to open an interactive session, or 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: the image embeds an emacs with Lustre and Lutin mode installed.

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 :

http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html

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 : http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/pre-compiled/

wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/pre-compiled/`arch`-lv6-bin-dist.tgz
tar xvfz `arch`-lv6-bin-dist.tgz
export LV6_PATH=`pwd`/lv6-bin-dist
. ./v6-tools.sh

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 (preferred method for ocaml users)

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 (all ?) 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 ocaml ocaml-native-compilers camlp4-extra opam
opam init 
eval `opam config env`
opam switch 4.06.1 ; eval `opam config env` # optional

[optional] In order to obtain the very last version, one can add the verimag opam repo. But tools versions in the official opam repo should be recent enough.

# optional
opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update

And then to install the necessary packages:

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

Once is is done, 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.

patate.svg

Some programs can be found in a dedicated github repo: https://github.com/jahierwan/lustre-examples

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);
let
 Y = r_edge(X) or r_edge(not(X));
tel
node r_edge (X: bool) returns (Y: bool);
let
 Y = false -> X and not pre(X);
tel

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

If one wants to generate only the code necessary for a specific node, one has to use the -node option (or -n for short).

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 edge.sh 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 
./edge.exec

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 edge.ec

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

5 RIF

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).

5.2.2 Comments

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) "
#@inputs
"T":real
"T1":real
"T2":real
"T3":real
@#
#@locals
"degradable-sensors__cpt":int
"degradable-sensors__eps":real
"degradable-sensors__eps1":real
"degradable-sensors__eps2":real
"degradable-sensors__eps3":real
@#
#@outputs
"Heat_on":bool
@#
#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);
let
 RE = false -> X and not pre(X);
tel;
node some_prop(X,RE:bool) returns (res:bool);
let
  res = true -> (pre(RE) => not(RE)) and (RE => not(pre(RE)));
tel
-- 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 environnement 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). 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;
let
   y = a_node(x);
   res = some_prop(x,y);
tel;
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 prop.ec
ecverif prop.ec

More information on Lesar is available Here.