WHAT IS TINA :
--------------

Tina (TIme petri Net Analyzer) is  a toolbox for the analysis of Petri
Nets and Time Petri Nets. The latest version of Tina may be downloaded
from the web page http://www.laas.fr/tina

At that time, the toolbox includes:

nd (NetDraw) : Time Petri net and Automata editor.
~~~~~~~~~~~~~~
Allows one to create a {Time} Petri nets, in textual or graphical form.
Interfaced with the above tools.

tina : construction of reachability graphs.
~~~~~~
Depending upon the  option retained, builds (references at  the end of
file):

The coverability graph of a Petri net, by the Karp and Miller technique.

The  markings reachability  graph of  a  Petri net  (untimed, or  with
timing information discarded).

The covering  step graph  of a Petri  net, according to  the technique
introduced in (6,7), preserving various properties.

The partial marking  graph of a Petri net  according to the persistent
sets method,  as well as  three experimental variants of  it combining
persistent sets and covering steps, described in (8).

Various  state space  abstractions for  Time Petri  nets  (state class
graphs),  following the  techniques introduced  in (1,2),  and further
refined  in (3,5).   Depending  on option  selected, the  construction
perserves markings, states, LTL  properties, or CTL* properties of the
concrete state space of the Time Petri net.

struct :  structural analysis of Petri nets.
~~~~~~~
Computes  generator sets  for  semi-flows or  flows  on places  and/or
transitions  of  a Petri  net.   Also  determines  the invariance  and
consistence properties.

path : path analysis if Time Petri nets.
~~~~~~
Given a  firable sequence of  transitions, this tool computes  all, or
one of, depending  on options, firing schedule that  has this sequence
as support.

selt : A State/Event LTL model checker.
~~~~~~
This tool checks a  Kripke transition system against S/E-LTL formulas,
interactively or  in batch mode.  Produce counter  example reusable by
the nd  stepper. For converting  S/E-LTL formula into  Buchi automata,
selt relies  on  ltl2ba  (http://www.liafa.jussieu.fr/~oddoux/ltl2ba).

ndrio : conversion tool for nets.
~~~~~~~
A tool for  converting Petri nets and Time  Petri nets between various
formats, including tina formats .net, .ndr and .tpn, and .pnml.

ktzio : conversion tool for transition systems.
~~~~~~~
A  tool   for  converting  labelled  transition   systems  (or  Kripke
transition  systems) between various  formats, including  formats .ktz,
.aut, .bcg, .mec, and textual formats.



INSTALLATION:
------------

Read:
file INSTALL  for installation notes, 
files doc/txt/*, or the Unix man pages in doc/man/mann, for usage,
files doc/formats/* for details about the concrete formats known to tina.

The binary distributions  of the Tina toolbox may  be freely installed
and  used  for  educational  or  research purposes.  The  software  is
distributes "as is", without warranties or conditions of any kind.

The Tina toolbox is property of LAAS-CNRS, 7, avenue du Colonel Roche,
31077, Toulouse.   For any comments, bug reports  or specific demands,
please contact the author at bernard@laas.fr.


REFERENCES : (check http://www.laas.fr/tina/papers for updates)
------------

(1) B.  Berthomieu, M. Menasche, An Enumerative Approach for Analyzing
    Time Petri Nets, IFIP Congress 1983, Paris, 1983.

(2) B.   Berthomieu,  M.   Diaz,  Modeling and  verification  of  time
    dependent  systems using  time Petri  nets.  IEEE  Transactions on
    Software Engineering, 17(3), 1991.

(3) B. Berthomieu, La mthode des Classes d'tats pour l'Analyse des Rseaux
    Temporels - Mise en Oeuvre, Extension  la multi-sensibilisation.
    Modlisation des Systmes Ractifs, MSR'2001, Hermes, 2001.

(4) B.  Berthomieu,  P.-O.  Ribet,  F.  Vernadat,  The  tool  TINA  --
    Construction  of Abstract  State Spaces  for Petri  Nets  and Time
    Petri Nets, International Journal of Production Research, Vol. 42,
    No 4, July 2004.

(5) B. Berthomieu, F. Vernadat, State class constructions for branching
    analysis of Time Petri nets, TACAS 2003. Springer Verlag LNCS 2619,
    2003.

(6) F. Vernadat, P. Azma, F. Michel, Covering Step Graph, Application
    and Theory of Petri Nets 96, Springer Verlag LNCS 1091, 1996.

(7) F. Vernadat, F. Michel, Covering Step Graph Preserving Failure Semantics,
    Application and Theory of Petri Nets 97, Springer-Verlag LNCS 1248, 1997.

(8) P-O. Ribet, F. Vernadat, B. Berthomieu, On Combining the Persistent Set
    Method with the Covering Step Graph Method, FORTE 2002, Springer Verlag
    LNCS 2529, 2002.

(9) B.  Berthomieu,   P.-O.  Ribet,  F.  Vernadat,   L'outil  TINA  --
    Construction d'espaces d'tats abstraits pour les rseaux de Petri
    et rseaux Temporels, Modlisation des Systmes Ractifs, MSR'2003,
    Hermes, 2003.
