
NAME
     tina - state space generation tool

     Part of Tina Toolbox for analysis of  Petri  nets  and  Time
     Petri nets (see also nd, plan, struct, ndrio, ktzio, selt).


SYNOPSIS
     tina [-help]
          [-C(|k|b) | -R |
           -V | -Vq | -V(o|f|l) tlist | -P | -Q(p|b|h) |
           -M(|m) | -E(|a) | -W(|m) | -S(|a) | -A | -U]
          [-s n] [-c n] [-b n] [-t s] [-m n] [-df | -bf] [-g |-p]
          [-NET | -NDR | -PNML | -TPN]
          [-v | -q | -aut | -mec | -bcg | -ktz]
          [-ls] [-lt] [-sp n] [-tp n] [-wp n]
          [infile] [outfile]


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


OPTIONS
     -help Recalls options.

     Operating mode options:

     -C |  -Ck |  -Cb
          Build the Coverability Graph of a Petri  net  (untimed,
          or  with temporal information discarded). Three heuris-
          tics are proposed:  -Cb is as fast as -R below  if  the
          net  is actually bounded, but may be very slow if it is
          not; -Ck  implements a  heuristic closer  to  the  ori-
          ginal  Karp and Miller method, it may be very  slow  if
          the net  is  actually  bounded,  but  unbounded  places
          are detected as early as possible; -C behaves like  -Cb
          until an unbounded marking  is found,  after  which  it
          behaves  like -Ck,  detecting further unbounded  places
          as  soon as possible.

     -R   Builds the marking reachability graph of  a  Petri  net
          (untimed, or with temporal information discarded).

     -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.  -Vq  stops  as     soon    as
          all    transitions     have    been     fired   (checks
          quasi-liveness).  tlist being  a  list   of  observable
          transitions,   -Vo   tlist    preserves   observational
          equivalence  wrt  transitions   in  tlist,  -Vf   tlist
          preserves   failure    equivalence,    and   -Vl  tlist
          preserves linear  time temporal   properties.  If   all
          transitions  are observable then -V(o|f|l) tlist is eqv
          to -R.

     -P   Builds  the partial marking  graph of   a  Petri   net,
          according    to  the  persistent  sets  technique.  The
          heuristic retained is to minimize local branching.

     -Qp | -Qb | -Qh
          Builds  the  partial   marking   graph   of   a   Petri
          net.  Combine  the persistent  sets  (-P)  and   cover-
          ing  steps   (-V)   methods.   Several  heuristics  are
          available:   -Qp  maximizes  size  of  steps; -Qb steps
          minimizing branching, like -P;  -Qh  largest  conflict-
          free steps, a trade off between -Qp and -Qb.

     -W   Build the linear  state class graph of  a  Time   Petri
          net,     according     to     the     technique      of
          Berthomieu/Menasche.   The linear  state   class  graph
          preserves  reachability properties and linear time tem-
          poral  properties.   If  no   temporal  information  is
          specified,  or if all  transitions bear interval [0,w[,
          then -W is silently replaced by -R.

     -Wm  As -W, except interprets multi-enabledness  of  transi-
          tions.

     -S   Build the strong linear state class  graph  of  a  Time
          Petri net.  If no temporal information is specified, or
          if all transitions bear  interval  [0,w[,  then  -S  is
          silently replaced by -R.

     -Sa  As  -S, except  signals  non atomic  state  classes.

     -M | -Mm
          As -W or -Wm, except only markings are preserved  (fir-
          ing sequences are not).

     -E | -Ea
          As -S or -Sa, except only states are preserved  (firing
          sequences are not).

     -A   Build 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.

     -U   An  alternative for  -A,  generally  slower,   provided
          for    educational   purposes.    Algorithmically,   -A
          partitions/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.

     Exploration strategy flags:

     -df  Depth-first exploration (meaningless for -A)

     -bf  Breadth-first exploration (default for -A)

     Stopping test and limits flags:

     -s n Stopping test for the boundedness property.
          -s 0 : none, use limit option(s) to ensure termination
          -s 1 : Karp and Miller condition (default)
          -s 2 : -s 1 + inclusion of firing domains
          -s 3 : -s 2 + saturation of transitions following
                 places with increasing markings (see documents).
          With -R, conditions -s 2 and -s 3 are equivalent to -s 1
          With -C, no stopping test is necessary.

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

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

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

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

     Output format selection :

     -v : textual output, prints full results

     -q : textual output, prints a summary of results

     -aut  : transition  system output  in .aut  format, as  read by
          Aldebaran.

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

     -ktz: transition system output in .ktz proprietary compact
          format.

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

     -ls : prints labelled state properties

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

     -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.

     -sp n : encoding of state properties for transition system
          outputs:

          -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

          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  proper-
          ties  (labels) are prefixed by  "T.", 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 pro-
          perties.  If  -sp 2 or 3 is specified, weighted proper-
          ties 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  pro-
          perties,  even for infinite weights (unbounded places).
          For .ktz, flag values 1 to 3 yield the same result.


     -tp n : encoding of transition properties for transition system
          outputs:

          -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

          The .aut and .bcg formats expect  a  single  transition
          property  (or  none, represented by "i"). Multiple pro-
          perties 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 multi-
          ple  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.

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

          -wp 0 : no wait state properties
          -wp 1 : emit wait state properties

          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" pro-
          perty 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 hav-
          ing that property.

          Default value: -wp 1 if 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 checkers has a
          flag to restore these properties, if desired.

     Other flags:

     -g   Disables liveness analysis (if not -a or -C).

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

     Input format flags:

     -NET | -NDR | -PNML | -TPN
          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

     Input source:

     infile
          Where the  net is  read. The  input format  is   deter-
          mined  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.

          file extension      input format
          --------------------------------------------------------------
           .net               net format
           .ndr               ndr format
           .tpn               tpn format
           .pnml              pnml format

     Output destination:

     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.

          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)

     Default options:

          tina -W -s 1 -c 0 -t 0 -b 0 -m 0 -v


FILES
     Files net.txt, ndr.txt, tpn.txt,  TPN.rng in directory  for-
     mats  specify  the  syntax of  .net,  .ndr,  .tpn and  .pnml
     net description  files, respectively.


EXAMPLES
     tina -q  < nets/ifip.ndr
     tina -PNML < mynet.xml
     tina -s 2 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


SEE ALSO
     nd, plan, struct, ndrio, ktzio, selt


AUTHORS
     Bernard       Berthomieu,       LAAS/CNRS,        2000-2005,
     Bernard.Berthomieu@laas.fr.
