Softwares that import or export into tina formats (.net or .ndr):

exp.open, a tool part of the CADP toolset from the VASY group exports networks of automata described in the EXP 2.0 language (.exp files) into Tina .tpn format.

Deborah, by Dmitry Zaitsev decomposes Petri nets described in .net or .ndr formats into Functional subnets, for a faster computation of invariants. The Deborah distribution includes ready to use plugins for nd.

Helena, by Sami Evangelista is a tool for modelchecking Colored Petri nets. Helena can also unfold Colored Petri nets and save them into .net files readable by tina.

Romeo, by Olivier H. Roux and colleagues is a tool for analysis of Scheduling Time Petri nets. Romeo imports and exports nets in tina formats.

The PEP tool may invoke tina for reachability analysis of Time Petri nets. The tool suite includes a converter from PEP format to tina .net format.

The SNOOPY editor exports to Tina formats.

Companion tools:

The tina state space construction tool can produce results in several formats:

The .aut and .bcg formats are the input formats of the Aldebaran and Bcg tools for transformation and analysis of transition systems. Both are part of the CADP toolset, from the VASY group.


The .mec format is the input format of Mec-4, a modelchecker for the propositional mu-calculus developped in the Altarica project at Labri.

For drawing petri nets or automata, nd and ndrio rely on dot and neato, part of the AT&T graph drawing package Graphviz.

For building Buchi automata from LTL formula, selt relies on ltl2ba, a tool developped by Denis Oddoux and maintained by Paul Gastin.

Implementation:

The tina graphic editor (nd) is written in Tcl/Tk and deployed using Tclkit.

The tina tools (tina, struct, plan, selt, ndrio, ktzio) are written in Standard ML for Poly/ML and MLton, and deployed using MLton.