.\" 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 "LUS2ATG 1"
.TH LUS2ATG 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"
lus2atg, oc2atg \- automata visualisation
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
\&\fBlus2atg\fR \fIfile\fR\fB.lus\fR \fInode\fR [\fBoptions\fR]
.PP
\&\fBoc2atg\fR \fIfile\fR\fB.oc\fR [\fBoptions\fR]
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
\&\fBoc2atg\fR extracts basic information
about the underlying automaton in the source file,
and outputs this information
in the \fBatg\fR format, suitable for the tool \fIautograph\fR;
See \f(CWhttp://www-sop.inria.fr/meije/verification\fR
.PP
Most of the information is lost: the \fBatg\fR file
only contains the skeleton of the program. This skeleton
consists of a set of states and transitions labelled by 
\&\*(L"input/output\*(R" presence conditions.
.PP
It is quite hard to compile a lustre program in such a way 
that the resulting \fBoc\fR program produces a meaningful 
\&\fBatg\fR automaton, so it is recommended to use
the script \fBlus2atg\fR.  Using this script, the Boolean part of
the source program will be exactly reflected in the resulting
automaton.
.SH "OPTIONS"
.IX Header "OPTIONS"
.SS "Miscellaneous"
.IX Subsection "Miscellaneous"
.IP "\fB\-v\fR set the verbose mode." 4
.IX Item "-v set the verbose mode."
.PD 0
.IP "\fB\-help\fR print available options." 4
.IX Item "-help print available options."
.IP "\fB\-o\fR \fIfile\fR define the output file (default is \fImodule-name\fR\fB.atg\fR)" 4
.IX Item "-o file define the output file (default is module-name.atg)"
.PD
.SS "Labels style"
.IX Subsection "Labels style"
.RS 4
Labels are representing the input/output presence on a transition.
Note that this information is relevant only if the oc program
uses \fIpure signals\fR (see \fBec2oc\fR). The \fIlus2atg\fR script automatically 
produces such a program.
There are actually two styles for the labels: reactive machine style,
and Boolean function style.
.RE
.IP "\fBdefault\fR (reactive machine style)" 4
.IX Item "default (reactive machine style)"
For the inputs, the default is to write \fB+inname\fR if the input is present,
\&\fB\-inname\fR if it is absent and \fB~inname\fR for it is don't care.
.Sp
For the output, only presence is represented by writing \fB!outname\fR (which means that
the output is emited during the transition).
.Sp
Exemple: \fB+x+y\-z~t/!a!b\fR means that, for the transition to be taken,
inputs \fBx\fR and \fBy\fR have to be true (i.e. present),
\&\fBz\fR has to be false (i.e. absent), \fBt\fR and any other input (if it exist) can either true or false
(don't care); as a consequence outputs \fBa\fR and \fBb\fR are true (emited), and any other output
is false.
.IP "\fB\-bf\fR (Boolean function style)" 4
.IX Item "-bf (Boolean function style)"
The label is made of the list of the input values (0 or 1) and the list of the
corresponding outpt values, separated by a \fB/\fR. For instance, if the program
has 2 inputs \fBx\fR, \fBy\fR and 1 output \fBs\fR, \fB10/1\fR means that the transition is taken 
when \fBx\fR is true, \fBy\fR is false, and that the output \fBs\fR is true.
.SS "Partial labels"
.IX Subsection "Partial labels"
.RS 4
Parts of the labels can be hiden.
.RE
.IP "\fB\-ht\fR hides the don't care inputs" 4
.IX Item "-ht hides the don't care inputs"
.PD 0
.IP "\fB\-hp\fR hides the true inputs" 4
.IX Item "-hp hides the true inputs"
.IP "\fB\-hm\fR hides the false inputs" 4
.IX Item "-hm hides the false inputs"
.IP "\fB\-hi\fR hides all the input part" 4
.IX Item "-hi hides all the input part"
.IP "\fB\-ho\fR hides all the output part" 4
.IX Item "-ho hides all the output part"
.IP "\fB\-h\fR hides the \fB/\fR separator between inputs and outputs" 4
.IX Item "-h hides the / separator between inputs and outputs"
.PD
.SH "SEE ALSO"
.IX Header "SEE ALSO"
lustre, lus2ec, ecexe, luciole, simec, lus2oc, ec2oc, ocmin, lus2atg, oc2atg,
ec2c, poc, lux, lesar, ecverif, xlesar