Softwares that import or export into tina formats (.net or .ndr):
exp.open, a tool part of the CADP toolset from the VASY/CONVECS groups 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.
Contributions:
-
(In progress) This section gathers TINA related material, including use cases, models in the TINA
formats, etc contributed by users.
Contributed by Dmitry Zaitsev (home page):
Models of networking protocols TCP, IOTP, BGP; square grids and hypercube; arithmetic operationsGenerators of Petri net models of a square grid with the following edge conditions: open edges, plugs on edges, truncated devices on edges
Generator of hypertorus Petri net models
Generators of canvas for Petri net models of hypertorus (hypercube) grid with Moore's, von-Neumann's, and generalized neighborhoods
Generator of Petri nets which count double exponent 2^2^k after R.J.Lipton & J.Esparza constructs
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/CONVECS groups.
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 spin, but other options are supported, including ltl2ba, a tool developped by Denis Oddoux and Paul Gastin and ltl2tgba, part of the spot toolset, developped by Alexandre Duret-Lutz. Some local LTL resources are available here.
Implementation:
The tina graphic editor (nd) is written in Tcl/Tk and deployed using EQUI4 or KitCreator tclkits, or ActiveState basekits, depending on platform.
The tina tools (tina, struct, plan, selt, ndrio, ktzio) are written in Standard ML for Poly/ML and MLton, and deployed using MLton. Some local resources are available here.