.\" 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 "LESAR 1"
.TH LESAR 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"
lesar, ecverif \- formal verification
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
\&\fBlesar\fR \fIfile\fR\fB.lus\fR \fInode\fR [\fBoptions\fR]
.PP
\&\fBecverif\fR \fIfile\fR\fB.ec\fR [\fBoptions\fR]
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
The \fBlesar\fR command first calls \fBlus2ec\fR, then \fBecverif\fR.
The \fBecverif\fR tool takes a program whose first output is
Boolean, and try to prove that this Boolean output remains true,
for any execution of the program (i.e. whatever is 
the infinite sequence of input values received by the program).
Moreover, the tool supposes that every assertion 
(\fBassert\fR statements) appearing in the program denotes an hypothesis
on the program environement, so the goal of the tool is at last to
prove that:
.PP
\&\fIWhatever the sequence of inputs, as long as the
assertions (the hypothesis) are satisfied, the first output (the property)
always remains true.\fR
.PP
The input program, often called the \fIverification program\fR, is
generally built as a combination of the program to validate (the implementation)
together with another program (the observer) expressing the safety property.
The user may read the \fILustre Tutorial\fR which explains
how to build verification programs suitable for 
\&\fBlesar/ecverif\fR.
.PP
\&\fBecverif\fR is a \fImodel-checker\fR: it
explores a finite model (an automaton) of the program. This model
is an abstraction that represents an upper-approximation of all the possible
executions of the program. The abstraction made on the 
program is conservative: if the verification
suceeds on the model, the property \fIis also satisfied\fR by the
program. In this case the tool answer \fITrue Property\fR.
If the verification fails on the model, the result is
inconclusive: either the property is not satisfied by the program,
or the property is too complex for the tool.
So when the tool answer \fIFalse Property\fR, it simply means
\&\fII don't know\fR!
.PP
More precisely, the Boolean part of the program is completly reflected in
the model, but everything else is abstracted (numerical variables,
external types and functions ...). Note that, as a consequence of this, the
model-checking is complete for purely Boolean programs (e.g. logical
circuits).
.PP
Nevertheless, some knowledge on numerical properties has been added
to the model checker. A library based on \fIpolyhedra manipulation\fR can be
used to check whether linear constraints are feasible or not.
For instance, using the polyhedra library, the tool will realise that 
the condition "\f(CW\*(C`(y < x) and (0 < e) and (x + 2*e < y)\*(C'\fR" cannot
be satisfied by any numerical values.
This information is then taken into account to obtain a more precise
model, but note that the verification still remains partial in general.
.PP
The successive stages of the computation are involving complex
algorithms that may take (a lot of) time. It is recomended to use
the verbose mode: in this case \fBecverif\fR outputs information
on the current stage, that allows the user to \*(L"guess\*(R" if the
computation has a chance to end in a reasonable delay.
The stages are:
.IP "Static analysis" 4
.IX Item "Static analysis"
The source code is optimized for the proof: this stage
performs dependence checking,
syntactic minimisation, and other optimization at the source level.
The complexity here is reasonable (linear or quadratic).
.IP "Bdds construction" 4
.IX Item "Bdds construction"
The Boolean part of the program is identified
and transformed in a set of logical functions, represented by bdds (Binary
Decision Diagrams). The result is an implicit representation of
the model to check. This stage may be exponential in the worst case.
.IP "Exploration of the model" 4
.IX Item "Exploration of the model"
Several algorithms can be selected.
In all cases, the time necessary for the traversal of the model
can be exponential in the worst case.
.SH "OPTIONS"
.IX Header "OPTIONS"
.SS "Miscellaneous"
.IX Subsection "Miscellaneous"
.IP "\fB\-v\fR" 4
.IX Item "-v"
set the verbose mode. Since the algorithms used in the tool
are very expensive, it is strongly recomended to use this option
in order to have a feed-back on the verification progress.
.IP "\fB\-help\fR" 4
.IX Item "-help"
print available options.
.SS "Static analysis"
.IX Subsection "Static analysis"
.IP "\fB\-nomin\fR" 2
.IX Item "-nomin"
Normally, the first stage of the verification consists
in minimizing the source program, according to syntactic equivalence
of expressions. This checking also takes into account equivalence of
\&\fIrecursive definitions\fR. The result is much more precise than
a simple \*(L"common sub-expression checking\*(R", but indeed   more
expensive, so the user can disable it with this option.
.IP "\fB\-split\fR" 2
.IX Item "-split"
split the property into several smaller ones (if possible).
.IP "\fB\-optb\fR" 2
.IX Item "-optb"
force static Boolean optimization of the source program.
This option was supported by older versions, but it is (almost) obsolete
since the bdds construction stage is now optimized.
.SS "Model checking"
.IX Subsection "Model checking"
The main stage of the model checker consists in exploring the
underlying automaton (the model). The user may choose between several
algorithms for this exploration.
.PP
Assertions are taken into account during the exploration to throw away
unfeasible transitions. A state whose all outgoing transitions have all
been discarded is said to be a \fIsink state\fR. Assertions that can produce 
sink states are said to be \fInon-causal\fR.
.IP "\fB\-enum\fR" 4
.IX Item "-enum"
(default) use the \fIenumerative algorithm\fR.
The automaton is checked state by state, starting from the initial one.
The verification fails as soon as a state violating the property is reached.
An error occurs if the assertions are found to be non-causal.
.IP "\fB\-states\fR \fIn\fR" 4
.IX Item "-states n"
only works in enumerative mode. The exploration
stops after \fIn\fR states are visited.
.IP "\fB\-forward\fR" 4
.IX Item "-forward"
use the \fIsymbolic forward\fR algorithm.
The set of reachable states is build as a Boolean formula over the 
state variables. The verification fails if this set 
contains states violating the property.
.IP "\fB\-backward\fR" 4
.IX Item "-backward"
use the \fIsymbolic backward\fR algorithm.
This algorithm builds a symbolic representation of the 
\&\fIbad states\fR, i.e. states that can lead to the violation
of the property. The verification fails if the initial state 
belongs to this set.
.IP "\fB\-causal\fR" 4
.IX Item "-causal"
compute a causal assertion equivalent to the initial one,
before starting the model-checking. This computing is expensive, so it
is recommended to use it only when needed (when a first attempt
have failed because of non-causal assertions). Moreover, this 
option must not be used with the \fIforward algorithm\fR, which
implements its own treatment for non-causal assertions.
.IP "\fB\-poly\fR" 4
.IX Item "-poly"
force the model checker to use the \fIpolyhedra library\fR
to check wether linear constraints on numerical values are feasible.
Without this option, semantics of numerical values is completly ignored,
and any condition is supposed to be feasible as soon as integers or reals
are involved.
.SS "Diagnosis"
.IX Subsection "Diagnosis"
.IP "\fB\-diag\fR" 2
.IX Item "-diag"
print a diagnosis when verification fails. The diagnosis
is a sequence of input values that may leads to a state violating
the property.
.IP "\fB\-lurettediag\fR \fIn filename\fR" 2
.IX Item "-lurettediag n filename"
Due to abstractions applied to non-boolean programs, the counter-examples
produced by the \fB\-diag\fR option are not always very useful, mainly because
(1) new inputs are created to the model to take into account the (now
unpredicatable) non-boolean elements of the program, and (2) as already
explained, abstraction may lead to false negatives: counter-examples,
which have no counterpart in the concrete model. In general, associating
a long and complex abstract counter-example with a concrete one is a long
and tedious exercise. This option generates richer output to the file called
\&\fIfilename\fR, which, in turn, can be fed into the tool \fBlurette\fR to try
and produce concrete counter-examples automatically.
.Sp
The \fBlurette\fR file contains three Lustre nodes \fInode_main\fR, \fInode_assertion\fR
and \fInode_oracle\fR (where \fInode\fR is the name of the main node in the 
verified program), which are to be given to \fBlurette\fR as the main, 
assertion and oracle node respectively. The length of the counter-example
produced is reported by \fBlesar\fR. The first (numeric) parameter specifies
the minimum length counter-example to produce. Typically, this is set to
0, for the shortest counter-examples, but sometimes the user may wish to 
force \fBlesar\fR to produce longer counter-examples.
.Sp
This option automatically enforces \fB\-forward\fR.
.SS "Bdds"
.IX Subsection "Bdds"
.IP "\fB\-merge\fR" 4
.IX Item "-merge"
perform a \*(L"clever\*(R" variable ordering before building bdds;
this option is sometimes useful when the state generation pahse cannot even
start.
.IP "\fB\-bddpage\fR \fIn\fR" 4
.IX Item "-bddpage n"
the space devoted to bdds is allocated
by pages. Before allocating new pages, the program first performs
garbage collection; for big programs, frequent garbage collection may
dramatically slow down the model-checking, so the user may increase
the size of pages, expressed in kilo-unit (default 10).
.SH "NOTES"
.IX Header "NOTES"
Building verification programs to \*(L"feed\*(R" \fBlesar\fR is quite hard.
The graphical proof manager \fBxlesar\fR can be a simpler way
for starting with formal verification.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
lustre, lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg,
ec2c, poc, lux, lesar, ecverif, xlesar