.\" 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 "XLESAR 1"
.TH XLESAR 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"
xlesar \- graphical proof manager for lustre
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
xlesar
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
This tool is a graphical interface to the lustre verification tool
\&\fBecverif\fR.
.PP
More precisely, this tool allows the user to manage a set of properties
for a given lustre program. Each property can be edited, annotated, completed 
with local assumptions. A window allows the user to select the desired
options and to launch the prover \fBecexe\fR.
.SS "Main window"
.IX Subsection "Main window"
The main window allows the user to select a main program and a main node
within this program. Once selected, the lists of inputs and outputs are
displayed and the user can define properties involving those variables.
.PP
The property manager is part of the main window: the user can create,
delete and edit properties.
.SS "Property editor"
.IX Subsection "Property editor"
In the main window, one must select a property (by clicking in the
properties list) and launch a property editor by clicking \fBEdit\fR.
In the property editor window, the user can:
.IP "\(bu" 4
edit the property name
.IP "\(bu" 4
define the property, by typing a correct Lutre Boolean expression 
(see below for details).
.IP "\(bu" 4
declare a local input (menu \fBEdit\fR, field \fBNew input\fR).
A local input behaves as a \*(L"random\*(R" value in the proofs.
.IP "\(bu" 4
declare and define a local variable (menu \fBEdit\fR, field 
\&\fBNew variable\fR).
.IP "\(bu" 4
define a local assertion (menu \fBEdit\fR, field \fBNew assertion\fR).
The assertion must be a correct Boolean lustre expression.
.IP "\(bu" 4
write a description of the property. The command \fBShow description\fR
from the \fBEdit\fR menu opens a text editor where the user can type his
description.
.SS "Correct lustre expressions"
.IX Subsection "Correct lustre expressions"
Each lustre expression entered in \fBxlesar\fR is checked for consistency
before the prover is launched.
Such an expression must be syntactically correct, but \fBxlesar\fR also
checks type and the identifier consistency.
Every identifier appearing in the expression must exists in the current
context. A valid identifier is:
.IP "\(bu" 4
any global input or output (those from the main node, if it exists).
.IP "\(bu" 4
any local input or variable that is currently enabled.
.SS "Imported nodes"
.IX Subsection "Imported nodes"
The tool does not allow the user to define complex objects like nodes.
In order to use a node call in the definition of a property (resp.
assertion, local variable), the user must \fIimport\fR its definition
(main window menu \fBImport\fR, menu \fBFiles\fR, command \fBLoad file\fR).
Once loaded, the imported file is parsed by xlesar to find and display
all the nodes declaration. From this moment on, the user will be able
to use those nodes in the property (resp. assertion or variable)  
definitions.
.SS "Prover launcher"
.IX Subsection "Prover launcher"
A prover launcher is displayed in the property editor window.
This launcher allows the user to select the options and run the proof.
It also display the current status of the property (checked, not checked or
unknown). When the prover is running, all messages are \*(L"echoed\*(R" in
the window, and the user may kill the proof process by pushing the 
\&\fBStop\fR button.
.SS "Saving and loading the session"
.IX Subsection "Saving and loading the session"
A xlesar session is called a \fIproject\fR (extension \fB.lesar\fR).
The user may save, load or restart a project via the \fBFiles\fR menu
in the main window.
.SH "ENVIRONMENT"
.IX Header "ENVIRONMENT"
The environement variable \fB\s-1LUSTRE_INSTALL\s0\fR must exist and hold
the path of the lustre v4 distribution.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
lustre, lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg,
ec2c, poc, lux, lesar, ecverif, xlesar