.TH tina n "Version 4.0.0" "Tina Tools"

.SH NAME
tina - state space generation tool

Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.

.SH SYNOPSIS

.B tina
[\-\f2h\f1elp] [-p]
     [-C | -Cw l | -Cm n | -R |
      -V | -Vq | -V(o|f|l) tlist | -P | -Q(|p|b) | -Z(v|i|vi) |
      -D | -F(|1) |
      -M(|m) | -E | -W(|m) | -S | -A | -U | -incl | -equal]
     [-s n] [-c n] [-b n] [-t s] [-m n] [-en n]
     [-df | -bf ] [-inh] [-tc] [-pr] [-dt] [-sw]
     [-NET | -NDR | -TPN | -PNML | -TTS]
     [-v | -q | -aut | -mec | -bcg | -ktz] 
     [-sp n] [-tp n] [-ls] [-lt] [-wp n] [-g] [-d] [-stats] 
     [infile] [outfile] [digestfile] [errorfile]


.SH DESCRIPTION

tina builds various  state space abstractions for Petri  nets and Time
Petri nets.  It  takes as input descriptions of  a Priority Time Petri
net  in textual  form (\&.net,  \&.pnml, \&.tpn  formats) or  graphical form
(.\&ndr format of files produced by  nd, \&.pnml with graphics), or a Time
Transition System description in .\&tts format.

.SH OPTIONS

.TP
\-\f2h\f1elp
Recalls options.

.TP
.B Operating mode options:

.PP
Note: stopwatches are only supported in modes -W and -S, they are omitted in all other modes.

.TP
\-C | -Cw l | -Cm n
Build the Coverability Graph of a Petri net (untimed, or with temporal
information discarded).
.br
-C  implements  a  method  close  to  the  original  Karp  and  Miller
algorithm;
.br
-Cw  l  behaves like -C,  except that it specifies  a list l of places
with initially unbounded markings;
.br
-Cm  n  behaves like -C,  except that  it  specifies  a threshold  for
unbounded places  (-C eqv.  -Cm  0). With -Cm  k, a place  p becomes
marked with w in  marking m' if some ancestor marking m  of m' is such
that: (for any q)(m'(q) >= m(q)) and  m'(p) > m(p) >= k.
.br
These options remove time constraints, inhibitor arcs, read arcs and priorities,
they set flags -tc -inh -pr.

.TP
\-R
Builds the marking reachability graph of a Petri net (untimed, or with
temporal information discarded). 
This option removes time constraints, it sets flag -tc.

.TP
\-V | -Vq | -Vo tlist | -Vf tlist | -Vl tlist

Builds  the Covering  Step  Graph of  a Petri  net,  according to  the
technique of Vernadat/Azema/Michel.  -V preserves deadlocks.
.br
-Vq stops
as soon  as all transitions  have been fired  or all states  have been
enumerated;  it   checks  quasi-liveness.   tlist  being   a  list  of
observable transitions,
.br
-Vo  tlist preserves observational equivalence
wrt transitions in tlist,
.br
-Vf tlist preserves failure equivalence, and
.br
-Vl  tlist   preserves  linear   time  temporal  properties.
.br
If  all
transitions are observable  then -V(o|f|l) tlist is eqv  to -R.  These
options remove  time constraints  and priorities,  they set  flags -tc
-pr.

.TP
\-P
Builds  the partial marking  graph of  a Petri  net, according  to the
persistent sets technique. The heuristic retained is to minimize local
branching.
These options remove time constraints and priorities, they set flags -tc and -pr.

.TP
\-Q | -Qp | -Qb
Builds  the  partial  marking  graph  of  a  Petri  net.  Combine  the
persistent  sets  (-P)  and   covering  steps  (-V)  methods.  Several
heuristics are available:
.br
-Qp maximizes size of steps;
.br
-Qb minimizes branching, like -P;
.br
-Q (recommended) implemnents a trade off between -Qp and -Qb.
.br
These options remove time constraints and priorities, they set flags -tc -pr.

.TP
\-Zv | -Zi | -Zvi
Builds marking graphs for three "maximal steps" firing rules:
.br
-Zv, or -sleptsov: a step at marking m is an enabled transition t fired at its maximum enabledness multiplicity at m; that is a bag t*k, where k is the largest integer such that t is firable k times simultaneously at m;
.br
-Zi, or -salwicki: a step at m is a maximal set of transitions simultenaously firable at m;
.br
-Zvi, or -slepsalw: a combination of -Zv and -Zi. A step at m is a maximal bag of transitions simultenaously firable at m;
.br
These options remove time constraints. In addition, options -Zi and -Zvi
remove priorities.

.TP
\-D
Builds the essential state graph of a Time Petri net, according to the
technique of Popova. This graph preserves reachability and linear time
temporal properties. Static intervals  must be closed or unbounded and
left-closed.   If no  temporal  information is  specified,  or if  all
transitions bear interval [0,w[, then -D is silently replaced by -R.

.TP
\-F | -F1
Builds  the subgraph  of the  state graph  obtained by  firing integer
delay transitions (unit delays if -F1) and discrete transitions.  This
graph strictly includes that obtained by -D  and  preserves  the  same
properties. Static intervals must be closed  or  unbounded  and  left-
closed. If no temporal information is specified, or if all transitions
bear interval [0,w[, then -F/-F1 is silently replaced by -R.

.TP
\-W
Builds the linear state class graph  of a Time Petri net, according to
the technique  of Berthomieu/Menasche.   The linear state  class graph
preserves  marking reachability  properties and  linear  time temporal
properties.   If  no temporal  information  is  specified,  or if  all
transitions bear interval [0,w[, then -W is silently replaced by -R.
This option removes priorities, it sets flag -pr.

.TP
\-Wm
As   \-W,  except   interprets  multi   enabledness   of  transitions.
Multi-enabled transitions are associated with several delay variables,
ordered by their creation dates.

.TP
\-M | -Mm
As -W or -Wm, except only markings are preserved (firing sequences are not).

.TP
\-S
Builds the  strong state class graph  (also called zone  graph by some
authors) of a Time Petri net.  That graph preserves state reachability
properties  and  linear  time  temporal properties.   If  no  temporal
information is  specified, or if all transitions  bear interval [0,w[,
then -S is silently replaced by -R.

.TP
\-E
As -S, except only states are preserved (firing sequences are not).

.TP
\-A
Builds the arborescent,  or atomic, state class graph  of a Time Petri
net.  The arborescent state  class graph preserves liveness properties
and branching time temporal properties.  If no temporal information is
specified,  or if  all transitions  bear  interval [0,w[,  then -A  is
silently replaced by -R.
This option currently removes priorities, it sets flag -pr.

.TP
\-U
An  alternative for  -A,  generally slower,  provided for  pedagogical
purposes.   Algorithmically,   -A  partition/refines  the   result  of
construction  -E, while -U  proceeds from  the typically  larger graph
obtained by -S. The graphs obtained by -A and -U should be bisimilar.
This option currently removes priorities, it sets flag -pr.

.TP
\-incl
Identify two state classes when one is included in the other.
This flag avoids to specify mode -M or -E when analyzing timed models.
It is silently ignored if the net is untimed or if some operating mode is
simultaneously set, otherwise it has the effects of -M if no priorities are
specified, or of -E otherwise.

.TP
\-equal
Identify two state classes when they are equal (default).
This flag undoes the effects of any preceding -incl flag.

.TP
.B Exploration strategy flags:

.TP
\-df
Depth-first exploration (when meaningful)

.TP
\-bf
Breadth-first exploration (default)

.TP
\-inh
Removes inhibitor and read arcs from the input net.

.TP
\-pr
Removes priority constraints from the input net.

.TP
\-tc
Removes time constraints  from the input net.

.TP
\-dt
Forgets data processing when reading a tts description.

.TP
\-sw
Forgets stopwatch and stopwatch-inhibitor arcs from input net.

.TP
.B Stopping test and limits flags:

.TP
\-s n
Stopping test for the boundedness property.
.nf
\-s 0 : None, use limit option(s) to ensure termination
\-s 1 : Checks a sufficient condition for unboundedness
        of the underlying untimed net (Fast but small risk
        of undetection).
With \-C, no stopping test is necessary.

With time constaints, inhibitor arcs, stopwatch arcs,
boundedness is undecidable.
.fi

.TP
\-c n 
Bound on the number of markings to enumerate (none if n=0).

.TP
\-b n 
Bound on the marking of each place (none if n=0).

.TP
\-t n
Bound on duration of enumeration (none if n=0).

.TP
\-m n
Bound on multi-enabledness of transitions (none if n=0).

.TP
\-en n
Lower bound on number of enabled transitions (none if n=0). E.g. absence
of deadlocks is checked on the fly with "-en 1".

.TP
.B Output format selection :

.TP
\-v
textual output, prints full results

.TP
\-q
textual output, prints a summary of results

.TP
\-\f2a\f1ut
transition  system output  in .aut  format, as  read by Aldebaran.

.TP
\-mec
transition system output in .mec format, as read by Mec 4.

.TP
\-\f2k\f1tz
transition system output in \.ktz proprietary compact format.

.TP
\-bcg
transition system output in .bcg compact format, as read by bcg tools.


.TP
\-ls
prints labelled state properties

Without option -ls, atomic state properties are bijectively mapped to the net's place names. 
With -ls, they are mapped to place labels.

.TP
\-lt
prints labelled transition properties

Without option -lt, atomic transition properties are bijectively mapped to the net's transition names. 
With -lt, they are mapped to transition labels.


.TP
\-sp n
encoding of state properties for transition system outputs:
.nf
-sp 0 : no state properties (default for .aut, .bcg)
-sp 1 : boolean state properties (default for .mec)
-sp 2 : weighted state properties (default for .ktz)
-sp 3 : weighted state properties for all weights
.fi

The \&.aut and \&.bcg formats do not natively support state properties. With -sp n,  where n>0, tina encodes them as additional transitions: regular transition properties (labels) are prefixed by  "E.", state  properties (markings) are  introduced as loops on states labelled by the places marked, prefixed by "S.". In  addition, when n>1, place names are suffixed by their marking, separated by "*".  E.g.  if place p3 has 3 tokens in state s, than -sp 1 adds transition (s,"S.`p3`",s), -sp 2 adds  (s,"S.`p3`*3",s), and -sp 3 adds  (s,"S.`p3` S.`p3`*2 S.`p3`*3",s).

The \&.mec format natively supports unweighted state properties. If -sp 2 or 3 is specified, weighted properties are encoded into boolean properties: e.g. marking  p*3  is represented by state property  p with -sp 1, p_3 with  -sp 2, and properties p, p_2, and p_3, with -sp 3.

The .ktz format natively supports weighted state properties, even for infinite weights (unbounded places). For \&.ktz, flag values 1 to 3 yield the same result.

.TP
\-tp n
encoding of transition properties for transition system outputs:
.nf
-tp 0 : no transition properties
-tp 1 : boolean transition properties (default for \&.aut, \&.bcg, \&.mec)
-tp 2 : weighted transition properties (default for \&.ktz)
-tp 3 : weighted transition properties for all weights
.fi

The \&.aut and \&.bcg formats expect a single transition property (or none, represented by "i"). Multiple properties are encoded into a single one, built from the concatenation of their representations.

The .\&mec format supports unweighted multiple transition properties.
Weights are appended to the  properties  as explained above for weighted  state  properties.

The \&.ktz format natively supports weighted transition properties (even for infinite weights). For \&.ktz, flag values 1 to 3 yield the same result.

Note: All tina constructions except -V  produce  single transition  properties; construction -V produces multiple  transition  properties. No construction  currently produces weighted  transition properties,  but  options -tp 2 and -tp 3 are still  useful  when  combined  with option -lt and transition labelling is surjective.

.TP
\-wp n
encoding of wait states for transition system outputs:

.nf
-wp 0 : no wait state properties
-wp 1 : emit wait state properties
.fi

In Time Petri nets, it may happen that no transition firable from some state has a finite firing deadline. Knowledge of such "wait" states is important for e.g. LTL model checkers. With -wp 1, an extra "wait" property is emitted for all wait states (thus for all states if the net is untimed or all transitions have interval [0,w[). In all formats, it is represented by an extra transition labelled "*" looping on states having that property.

Default value: -wp 1 if ktz output and at least one transition has an interval different from [0,w[, otherwise -wp 0. This treatment avoids to associate a wait property for all behavior states in untimed nets, for which LTL model checking typically assumes a fairness hypothesis for transition firing. The tina LTL model checker has a flag to restore these properties, if desired.

.TP
.B Other flags:

.TP
\-stats
Prints progress information on the fly.

.TP
\-g
Disables liveness analysis (if applicable).

.TP
\-p
Disables reachability and liveness analysis (just parses).

.TP
\-d
As of 2.9.4, tina prints a five lines digest in digestfile (see below)
after construction of the specified abstraction.
Flag -d disables printing and computation of digest (if applicable).

The digest information includes status information for the properties
of the net (boundedness, liveness, reversibility) and some information
about the contents of the transition system (ts) built:

.nf
count: the number of states/transitions in the ts
props: the number of atomic states/transitions propositions
       referred to in the ts. Depending on whether ts is built
       from names or labels, these are:
       - the numbers of places/transitions of the net, or
       - the numbers of distinct place/transition labels
psets: the number of sets of propositions referred to in the
       ts. Depending on whether ts is built from names or
       labels, these are
       - the numbers of markings/transition steps referred
          to in the ts, or
       - the numbers of those distinct after labelling
dead: the numbers of deadlock states and of unfireable transitions
live: the numbers of live states and transitions, where
       - a state is live if it is found in some pending
          strong connected component of the ts
       - a transition is live if it fires in all pending
          strong connected components of the ts
.fi


.TP
.B Input format:

.TP
\-NET | -NDR | -PNML | -TPN | -TTS
Specifies the format of the input net. This flag is necessary when the
input net is read on standard input, or read from a file that does not
bear the expected extension. By default, the net is assumed in \&.net or
\&.ndr format.

.TP
.B Input source:

.TP
infile
Where the  net is  read. The  input format is  determined by  the file
type, according to the table below. If absent or specified by "-", the
net is  read on standard  input in the  format specified by  the input
flag. If  both an  infile and  some input flag  are present,  then the
format defined  by the  input flag supersedes  that determined  by the
infile extension.

.nf
file extension		input format
--------------------------------------------------------------
\&.net			net format
\&.ndr			ndr format
\&.tpn			tpn format
\&.pnml			pnml format
\&.tts			tts format
.fi

.TP
.B Output destination:

.TP
outfile
Where results are written. The output format is determined by the file
type, according  to the  table below. If  absent or specified  by "-",
then the net is written on standard output in the format specified by
the output flag. If both an  outfile and some output flag are present,
then the format defined by  the output flag supersedes that determined
by the outfile extension.

.nf
file extension		output format
--------------------------------------------------------------
\&.ktz			tina binary ktz format
\&.bcg			bcg tools bcg format
\&.aut			aldebaran aut format
\&.mec			mec4 mec format
any other		textual output (default -v style)
.fi

.TP
.B Digest destination:

.TP
digestfile

As of 2.9.4, tina prints a five lines digest in digestfile (default stdout) 
after construction of the specified abstraction. 

.TP
.B Errors destination:

.TP
errorfile
Where error messages are written. By default, errors are printed on standard error.


.TP
.B Default options:

Depend upon the features of the input net:
.nf
If no time constraint:     tina -R -s 1 -c 0 -t 0 -b 0 -m 0 -v
Else, if no priorities:    tina -W -s 1 -c 0 -t 0 -b 0 -m 0 -v
Otherwise:                 tina -S -s 1 -c 0 -t 0 -b 0 -m 0 -v
.fi


.SH EXAMPLES

.nf
tina -q  < nets/ifip.ndr
tina -PNML < mynet.xml
tina -s 0 nets/abp.net abp.txt
tina -R -q < nets/ifip.ndr > ifip.log-R
tina -a nets/ifip.ndr > ifip.aut
tina -C ../nets/hp.ndr hp.ktz
tina -R ../nets/ifip.ndr ifip.ktz ifip.digest ifip.error
.fi


.SH SEE ALSO

nd(n), plan(n), struct(n), ktzio(n), ndrio(n), tedd(n), selt(n), sift(n), muse(n), pathto(n), scan(n), play(n), walk(n), reduce(n), formats(n), stan(n)


.SH AUTHORS
Bernard Berthomieu, with contributions by Francois Vernadat,
Pierre-Olivier Ribet, Florent  Peres,  LAAS/CNRS,  2000-2026,
{Bernard.Berthomieu|Francois.Vernadat}@laas.fr.

