.\" Automatically generated by Pod::Man 4.10 (Pod::Simple 3.35)
.\"
.\" Standard preamble:
.\" ========================================================================
.de Sp \" Vertical space (when we can't use .PP)
.if t .sp .5v
.if n .sp
..
.de Vb \" Begin verbatim text
.ft CW
.nf
.ne \\$1
..
.de Ve \" End verbatim text
.ft R
.fi
..
.\" Set up some character translations and predefined strings.  \*(-- will
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
.\" double quote, and \*(R" will give a right double quote.  \*(C+ will
.\" give a nicer C++.  Capital omega is used to do unbreakable dashes and
.\" therefore won't be available.  \*(C` and \*(C' expand to `' in nroff,
.\" nothing in troff, for use with C<>.
.tr \(*W-
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
.ie n \{\
.    ds -- \(*W-
.    ds PI pi
.    if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
.    if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\"  diablo 12 pitch
.    ds L" ""
.    ds R" ""
.    ds C` ""
.    ds C' ""
'br\}
.el\{\
.    ds -- \|\(em\|
.    ds PI \(*p
.    ds L" ``
.    ds R" ''
.    ds C`
.    ds C'
'br\}
.\"
.\" Escape single quotes in literal strings from groff's Unicode transform.
.ie \n(.g .ds Aq \(aq
.el       .ds Aq '
.\"
.\" If the F register is >0, we'll generate index entries on stderr for
.\" titles (.TH), headers (.SH), subsections (.SS), items (.Ip), and index
.\" entries marked with X<> in POD.  Of course, you'll have to process the
.\" output yourself in some meaningful fashion.
.\"
.\" Avoid warning from groff about undefined register 'F'.
.de IX
..
.nr rF 0
.if \n(.g .if rF .nr rF 1
.if (\n(rF:(\n(.g==0)) \{\
.    if \nF \{\
.        de IX
.        tm Index:\\$1\t\\n%\t"\\$2"
..
.        if !\nF==2 \{\
.            nr % 0
.            nr F 2
.        \}
.    \}
.\}
.rr rF
.\"
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
.\" Fear.  Run.  Save yourself.  No user-serviceable parts.
.    \" fudge factors for nroff and troff
.if n \{\
.    ds #H 0
.    ds #V .8m
.    ds #F .3m
.    ds #[ \f1
.    ds #] \fP
.\}
.if t \{\
.    ds #H ((1u-(\\\\n(.fu%2u))*.13m)
.    ds #V .6m
.    ds #F 0
.    ds #[ \&
.    ds #] \&
.\}
.    \" simple accents for nroff and troff
.if n \{\
.    ds ' \&
.    ds ` \&
.    ds ^ \&
.    ds , \&
.    ds ~ ~
.    ds /
.\}
.if t \{\
.    ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
.    ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
.    ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
.    ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
.    ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
.    ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
.\}
.    \" troff and (daisy-wheel) nroff accents
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
.ds ae a\h'-(\w'a'u*4/10)'e
.ds Ae A\h'-(\w'A'u*4/10)'E
.    \" corrections for vroff
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
.    \" for low resolution devices (crt and lpr)
.if \n(.H>23 .if \n(.V>19 \
\{\
.    ds : e
.    ds 8 ss
.    ds o a
.    ds d- d\h'-1'\(ga
.    ds D- D\h'-1'\(hy
.    ds th \o'bp'
.    ds Th \o'LP'
.    ds ae ae
.    ds Ae AE
.\}
.rm #[ #] #H #V #F C
.\" ========================================================================
.\"
.IX Title "LUSTRE 1"
.TH LUSTRE 1 "2020-02-06" "lustre v4, release III.a" "Lustre V4 Distribution"
.\" For nroff, turn off justification.  Always turn off hyphenation; it makes
.\" way too many mistakes in technical documents.
.if n .ad l
.nh
.SH "NAME"
lustre
.PP
lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg, ec2c, poc, lux, lesar, ecverif, xlesar \- lustre v4 tools
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
.SS "Lustre and ec"
.IX Subsection "Lustre and ec"
The front-end for Lustre\-V4 tools is the pre-processor \fBlus2ec\fR
.PP
This compiler transforms a Lustre\-V4 program (\fB.lus\fR file,
with modularity, arrays, recursion) into a Lustre-expended-code program
(\fB.ec\fR file, with a single node, no arrays, no recursion).
.PP
All other tools (compilers, simulators ...) are actually running 
on the \fB.ec\fR format, but the distribution provides (in general)
shell scripts combining the front-end (\fBlus2ec\fR) with
the various back-ends (compilers and simulators).
.SS "Simulation"
.IX Subsection "Simulation"
The Lustre\-V4 distribution provides simulation tools that
interpret \fBec\fR code. They only run on \fIbasic programs\fR,
that do not require external types, constants or functions;
however, some classical functions are supported,
corresponding to the \fImath\fR C library.
All those tools are based on the same interpreter, and only differ
on the user interface:
.IP "\fBFile to file simulation:\fR" 4
.IX Item "File to file simulation:"
\&\fBecexe\fR is a \fIunix-filter like\fR tool,
reading on standard input and writing to standard output.
.IP "\fBGraphical simulation:\fR" 4
.IX Item "Graphical simulation:"
\&\fBxecexe\fR (script \fBxsimlus\fR) provides a graphical interface
to the \fBec\fR interpreter; this tool, based on X\-intrinsics 
and Athena widgets is quite old and no longer maintained.
.Sp
\&\fBsimec\fR (script \fBluciole\fR) provides a more friendly interface,
based on \fItcl-tk widgets\fR. Moreover, it allows the user to
(slightly) customize the graphical interfaces.
.SS "Automata generation"
.IX Subsection "Automata generation"
Originally, the lustre compiler was designed to use an intermediate
format, called \fBoc\fR (for object code). This format was initiated by
a collaboration with the Esterel team, and several releases 
where defined. The main characteristic
of this format is that the control structure consists of a finite
state automaton. The tool \fBec2oc\fR (script \fBlus2ec\fR or \fBlustre\fR)
supports \fBoc\fR version 2 ( \fBoc2\fR) and 5 (\fBoc5\fR).
It also provides lot of options that allow the user to choose the
automaton stucture of the generated code.
.PP
Some tools based on the \fBoc\fR format are provided by the Esterel team,
in particular C and Ada code generators (\fBocc\fR, \fBocada\fR).
An alternative Ansi-C code generator, \fBpoc\fR, is provided within
the lustre distribution.
.PP
The distribution also provides a tool that performs minimization
of oc automata (\fBocmin\fR) and a translator to the
\&\fIautograph\fR format (\fBoc2atg\fR).
.SS "C code generation"
.IX Subsection "C code generation"
The low-level target format in Lustre\-V4 is Ansi-C. 
This code can be obtained either:
.IP "\(bu" 4
via \fBec2oc\fR, using the \fBpoc\fR compiler,
.IP "\(bu" 4
directly from the \fBec\fR code, using the compiler \fBec2c\fR.
.PP
Note that the code generated by \fBec2c\fR is different from the
one generated by \fBec2oc\fR; in particular
\&\fBec2c\fR does not build any kind of automaton.
On the contrary the generated interface is the same for both compiler,
so one can (normally) easily swap between code generated by \fBpoc\fR
and code generated by \fBec2c\fR.
.PP
By default, those compilers only provide a \fItransition function\fR,
and the user has to write his (her) own input/output and main procedures.
Moreover, the user has to provide the implementation
of all external objects (types, constants and functions) declared in the
Lustre source.
.PP
Nevertheless, both \fBpoc\fR and \fBec2c\fR have an option \fB\-loop\fR
that builds an additional main procedure. This simple
\&\*(L"loop\*(R" works as a unix filter (just like \fBecexe\fR).
In order to obtain an executable, this main program may
be completed by the implementation of the (possible) external objects.
Anyway, it can be used as a pattern for more complex application.
.PP
If the code does not require external objects, the main
generated by the \fB\-loop\fR option  can be linked \*(L"as it is\*(R"
with the transition function, in order to build a stand-alone
application.
This is the case for almost all programs that can be simulated
using \fBecexe\fR; by the way, the execution of such a stand-alone
program is completly similar to a simulation with \fBecexe\fR:
standard input to standard output, interactive when called form
a terminal.
.PP
The script \fBlux\fR is the best way for quickly building a stand-alone
application: it can take either \fBlus\fR, \fBec\fR or \fBoc\fR 
files as input, and uses the most suitable compilers calls
and build, if possible, a sstand-alone application.
Note that C compilation and the link-editing are performed by the
host Ansi-C compiler; by default, \fBlux\fR calls the \s-1GNU C\s0 compiler
\&\fBgcc\fR, but one may customize this script.
.SS "Formal verification"
.IX Subsection "Formal verification"
The Lustre model-checker is \fBecverif\fR (shell \fBlesar\fR).
It provides several algorithms to check the validity of safety
properties on Lustre programs.
\&\fBlesar\fR (resp. \fBecverif\fR) takes as input
special \fBlustre\fR (resp. \fBec\fR) programs,
called \fIverification programs\fR. Roughly speaking, such a program
must be the parallel product of a program to validate, a program
\&\fIobserving\fR that the desired property is satisfied, and another one
\&\fIobserving\fR that the hypothesis on the environment are satisfied.
The user may build this product himself, and at last, 
\&\fBlesar\fR only checks that its input has a single Boolean output,
wich is supposed to be the property to check; the hypothesis are
supposed to be the conjunction
of all the assertions appearing in the verification program.
.PP
\&\fBxlesar\fR is a graphical interface to \fBlesar\fR/\fBecverif\fR.
This tool is particularly suitable for managing a set of verifications on
the same Lustre programs.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
lustre, lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg,
ec2c, poc, lux, lesar, ecverif, xlesar