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

Table of Contents

Author Erwan Jahier
Date 2017-05-24 18:04

Table of Contents

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

2.1 The V6 tools suite

The V6 distribution is based on 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 Debian-like distributions, installing opam just requires:

sudo apt-get install opam
opam init

Then, one just need to add the Verimag repository to opam as follows:

opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update
opam install lustre-v6 lutin rdbg

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

opam update
opam upgrade

If you install opam for this purpose, by default its uses the "system" ocaml, i.e., the one installed by your package manager. If, for some reasons (e.g., the debian package camlp4-extra is missing), the previous commands does not work (and if apt-get install camlp4-extra is not enough), try to install a local version of ocaml as follows:

opam switch 4.04.0

2.2 The V4 tools suite

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.

3 Lustre V6

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

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 (poorly) named lus2lic. By default, lus2lic 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.

patate.svg

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:

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

lus2lic edge.lus -node edge
lus2lic edge.lus -n r_edge

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

lus2lic edge.lus -n edge -2c

3.2 Executing Lustre V6 programs

The call to lus2lic 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.

lus2lic edge.lus -node edge -2c -cc
./edge.exec

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

lus2lic edge.lus -node edge -exec

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 lus2lic edge.lus -node edge -exec
lus2lic 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:

lus2lic edge.lus -node edge -lv4 -o edge_v4.lus
lus2lic 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 or graphically display RIF data files via chronograms, can use sim2chro or sim2chrogtk

sim2chro -ecran xxx.rif > /dev/null
sim2chrogtk xxx.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 xxx.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 lus2lic edge.lus -node edge -exec

The executable produced via C also speaks RIF:

lus2lic edge.lus -node edge -2c -cc -o edge
luciole-rif ./edge.exec

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 Test

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

lurette -sut "lus2lic f.lus -n N" -env "lutin env.lut -n N_env" \
     -oracle "lus2lic f.lus -n N_prop" -l 100

Before running the test, lurette will check that:

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

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 Debug

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

rdbg -sut "lus2lic f.lus -n N"

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 "lus2lic f.lus -n N" -env "lutin env.lut -n N_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 "lus2lic f.lus -n N" -env "lutin env.lut -n N_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 "lus2lic f.lus -n N" \
     -env-nd "lutin env.lut -n M_env" \
     -oracle "lus2lic f.lus -n N_prop"

More information on rdbg

11 Proove

Lesar is a model-checker of temporal program properties written in Lustre. It is distributed with the V4 tool set. In order to model-check Lustre V6 programs properties, one first needs to translate it into one of the Lustre V4 dialects.

lus2lic some_file.lus -n some_prop -lv4 -o v4_prop.lus
lesar v4_prop.lus some_file__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 more direct approach consists of generating an .ec file with lus2lic -ec, and to give the resulting file to ecverif:

lus2lic some_file.lus -n some_prop -ec -o prop.ec
ecverif prop.ec

More information on Lesar is available Here.