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

Author Erwan Jahier
Date 2022-10-17 14:31

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

  • Execute Lustre V6 programs
  • Execute Lutin programs
  • Luciole-rif eases the simulation of programs that reads/writes RIF using TK GUIs
  • Lurette is a tool that automate the black-box testing of Reactive programs (e.g., written in Lustre)
  • rdbg can help to debug Lustre V6 or Lutin programs
  • Lustre, Lutin, lurette, rdbg, and others produce RIF Data files, that can be visualised with
  • Lesar (a BDD-based model-checker) can formally verify temporal program properties written in Lustre.

For more information, some tutorials are available here

lustre.png

2 Install

Different ways of installing those tools are possible. Via

  1. docker
  2. Virtual Machines
  3. V4 binaries (pre-compiled binaries gathered in a tarball)
  4. V6 binaries (ditto)
  5. opam (opam is an ocaml package manager)
  6. git. The gitlab projects hosting the different tools are accessible from: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone

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

tools \ distributions Virtual Machine 2 docker 2 2 V4 binaries 2 2 V6 binaries 2 2 opam 2 2 git 2
V4 essentials (*) X X X X    
V4 full (*) X X X      
lv6 X X   X X X
lutin X X   X X X
sim2chro X X X X    
gnuplot-rif X X   X X X
luciole-rif X X   X    
lurette X X   X X X
rdbg X X     X X
lesar X X X X    
kind2 (**) X X     X  

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

(**) kind2 is not a Verimag software, but it can be used on Lustre V4 and V6 programs and installed via opam.

Hence, to get the complete set of tools, you need to use of the following alternatives:

  • the docker distribution
  • the VM distribution
  • the "V4 binaries" + "V6 binaries" distributions
  • the "V4 binaries" + "opam" distributions

As far as OSes are concerned, here is a compatibility matrix:

OS \ distributions Virtual Machine 2 docker 2 2 V4 binaries 2 2 V6 binaries 2 2 opam 2
linux X X X X X
mac os (**) X X     X
windows (*) X X     ?

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

  • use the -novnc docker image (see below)
  • or :
    • 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. Otherwise, the novnc docker image works fine without any X server (see below).

2.1 The V4 and V6 tools suite via docker

One way to install the verimag reactive tools is via docker – which of course you need to install.

2.1.1 Using the dockver script

The sh/dockver sh script makes its best to set everything automatically (user id, X11 setup, mount your current directory, etc.).

wget https://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/sh/dockver
chmod u+x dockver
mv dockver /somewhere/accessible/from/your/$PATH/
dockver

When you launch dockver (in a terminal), X11 programs (such as xterm) should work fine. The directory /workspace/ is mounted on the directory you run the dockver script from. All the tools mentionned above should be available (lv6, lurette, etc.) as well as emacs, opam, z3, and others.

One can also use the binaries provided in this image directly (i.e., outside docker) 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.

2.1.2 Using dockver -novnc

If the X-based programs don't run, you may try the -novnc option:

dockver -novnc

In this case, the script runs a noVNC based image, where the graphics is handled (in javascript) inside your browser at http://localhost:6080/

2.1.3 Using dockver -x11docker

An other alternative consists in using x11docker:

dockver -x11docker

In any case, you can have a look at the content of the sh/dockver script.

2.2 The V4 and V6 tools suite via a Virtual Machine

You can use a Virtual Machine (e.g., VirtualBox or VmWare) via an ova file that you can download here:

http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/pre-compiled/verimag-reactive-toolbox.ova

This virtual machine has been built out of the docker image described above - same login (verimag) no password.

nb: a useful command if you have an azerty keyboard:

setxkbmap fr   

2.3 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.4 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/

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

2.5 The V6 tools suite via opam (2 or higher)

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

set -x
sudo apt-get update 
sudo apt-get install -y make wget
wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
yes '' | sudo sh install.sh || echo "ignore failure"
opam init \
           --disable-sandboxing  # only necessary when run from docker 
opam switch create 4.12.0 # optional
eval $(opam env)

In order to obtain an up-to-date version, it is better to use the verimag opam repository:

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

In any case, to install the V6 related packages:

opam install lustre-v6 lutin sasa

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.

Sorry, your browser does not support SVG.

In the following, 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

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 check that this Lustre program is syntactically correct, one just need to invoke:

 lv6 edge.lus -n edge 

Note that the -node option (or -n for short), that sets the top-level node, is mandatory (contrary to the lustre v4 compiler).

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

In order to generate C code, one can use -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 

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 (everything that appears between a '#' and a end-of-line)
  • pragmas, that are particular kinds of comments ('#inputs', '#outputs', '#outs', '#outs', etc.)
  • data (int, bool, float)

5.2 The RIF convention (in more details)

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

Available options be obtained via lurette -h and lurette -more.

More on Lurette and automatic testing of Reactive Programs

10 rdbg

rdbg have the same command-line set of options as lurette.

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;
let
   assert(some_prop_on_inputs(x));
   y = a_node(x);
   res = some_prop(x,y);
tel;
node some_prop_on_inputs(x: bool) returns (res: bool);
let
  res = x -> true; -- true at the first instant
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

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.

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. It is easy to install via opam (opam install kind2) and is part of the docker and Virtual machines distributions (cf 2 section).