Tina is a toolbox for the analysis of Petri Nets and Time Petri Nets. At that time, it includes the tools:
Time Petri net editor, and tools gui.
Construction of state class graphs of Time Petri nets according to the techniques introduced in (1), (2), (3).
Construction of marking graphs of Petri nets (time annotations omitted, if any).
Structural analysis of Petri nets. Computes the invariance and consistence properties for a net and the generator sets for semi-flows on places and transitions.
(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.