About Tina
TINA (TIme petri Net Analyzer) is a toolbox for the editing and analysis of Petri Nets, with possibly inhibitor and read arcs, Time Petri Nets, with possibly priorities and stopwatches, and an extension of Time Petri Nets with data handling called Time Transition Systems. TINA has been developed in the OLC, then VerTICS, research groups of LAAS/CNRS. General Petri nets information can be found on the Petri Nets World site.
The TINA toolbox includes the tools:
nd (NetDraw): Editor and GUI for Petri nets, Time Petri Nets and Automata.
-
Handles graphically or textually described nets or automata. Interfaced with analysis tools below. Includes drawing facilities for nets and automata and a stepper simulator for nets.
tina: Construction of reachability graphs.
-
From nets described in textual or graphical form, produces transition systems abstracting their behavior 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. |
| 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 discussed in [1][2][3][5]. Depending on the option selected, the construction perserves markings, states, LTL properties, or CTL* properties of the concrete state space of the Time Petri net. |
sift: Construction and checking of reachability graphs.
-
Sift is a specialized version of tina supporting in addition on the fly verification
of reachability properties. If offers less options than tina but is typically faster
and requires considerably less space.
struct: Structural analysis of 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.
plan: Path analysis.
-
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.
-
Operates in batch or interactive mode. Model checks the kripke transition systems built by the tina or sift tools
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 spin,
ltl2ba or ltl2tgba (from spot)
at the user's choice.
muse: A modal mu-calculus model checker.
-
Operates in batch or interactive mode. Model checks the kripke transition systems built by the tina or sift tools
above against modal mu-calculus formula. Accepts a rich language allowing notably to declare new operators or redefine
existing operators. Muse computes the set of states obeying some formula. A path to some state can then be
computed using the pathto and plan tools, and that path replayed on the model using tool play or the
nd stepper.
play: Stepper simulator.
-
Allows to simulate interactively and step by step net descriptions in all formats accepted by tina.
Its capabilities are similar to those of the nd stepper except that it is faster and may also simulate
Time Transition Systems.
pathto: Path finder.
-
A utility tool computing the path to some state in a kripke transition system.
ndrio: Conversion tool for Time Petri nets.
-
Converts between Tina formats .net, .ndr, .tpn and the .pnml exchange format.
Also export to other formats of Petri nets or Time Petri nets.
ktzio: Conversion tool for Kripke transition systems.
-
Converts Tina .ktz format to/from CADP formats .aut, .bcg and MEC4 format .mec.
tedd: Construction of symbolic reachability graphs.
-
Plays a role similar to the above sift tool but relies of decision diagram based methods rather than explicit
methods. Allow to check absence of deadlocks or of dead transitions, and, in the short future, arbitrary
reachability properties.
reduce: State space preserving reductions of Place/Transition nets.
-
Implements the reduction rule sets introduced in [20], [21]. Given a reduction rules specification,
it produces a reduced net together with reduction traces, in the form of equations, allowing to reconstruct the state space
of the original net from that of the reduced net.
walk: Constrained ramdon walker.
-
Given a reachability property, tool walk attempts to find a marking falsifying it.
It looks essentially like a non-interactive version of tool play, plus some exploration directives.
Much faster and space efficient, as simulation history is not recorded.
frac: Fiacre to tina tts compiler.
-
Fiacre is a high level description language for real time systems; frac compiles Fiacre
descriptions into the Time Transition Systems (tts) accepted as input by most TINA tools.
Because it moves at a different pace than Tina, frac is not distributed with the
toolbox but made available on a dedicated Fiacre site.