What is Tina ?

Tina is a toolbox for the edition and analysis of Petri Nets and Time Petri Nets, developed in the OLC group of LAAS/CNRS. General Petri nets information can be found on the Petri Nets World site.

The Tina toolbox includes the tools:

nd (NetDraw): An editor for graphically or textually described Petri nets, Time Petri net and Automata. Interfaced with analysis tools below and drawing facilities.

tina: Construction of reachability graphs. Inputs nets in textual or graphical format. Outputs graphs in human readable form or in various formats for available model checkers and equivalence checkers.
This tool is described in [4] and [9]. Depending on options retained, it builds:

• The coverability graph of a Petri net, by the Karp and Miller technique.
• The marking graph of a bounded Petri net, checking boundedness on the fly.
• Partial marking graphs of a Petri net, by the covering steps methods of [6][7], the method of persistent sets, or several combinations of them explained 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 (preliminary).

• Computes generator sets for semi-flows or flows on places and/or transitions of a Petri net. Also determines the invariance and consistence properties.

plan: Path analysis of Time Petri nets (from 2.8.0, preliminary).

• Computes all, or a single, timed firing sequence (schedule) over some given firing sequence. May also computes the fastest and slowest paths.

selt: A State/Event LTL model checker (from 2.8.0).

• Operates in batch or interactive mode. Model checks the kripke transition systems built by the tina tool above against S/E LTL formula. Accepts a rich language allowing notably to declare new operators or redefine existing operators (so that available libraries can be loaded with virtually no changes). The counter examples generated can be saved in a format loadable into the nd simulator, for replay. For conversion of formula to Buchi automata, selt relies on ltl2ba.

ndrio: Conversion tool for Time Petri nets (from 2.8.0).

• Converts between Tina formats .net, .ndr and .tpn, and .pnml format.

ktzio: Conversion tool for Kripke transition systems.

• Converts between Tina .ktz format and .aut, .bcg (CADP formats), and .mec (MEC4 format).