Tool homepage: http://www.laas.fr/tina
Tool availability: Free of charge
nd: An editor for Petri nets, Time Petri nets, and automata, in textual or graphical form, interfaced with drawing tools and the analysis tools below. A stepper/simulator operating both in graphical and textual modes is packed with the editor.
tina: Builds various reachability graphs or state space abstractions for Petri nets and Time Petri nets. For Petri Nets: coverability graphs, markings graphs, and various partial graphs using Covering steps, Stubborn or Persistent sets, or Persistent steps. For Time Petri nets: various state class graph constructions, preserving markings, states, linear time properties, or branching time properties. Results may be produced in several popular formats.
struct: Computes semiflows (invariants) or flows on places and/or transitions, with various options.
LAAS-CNRS 7, avenue du Colonel Roche 31077 Toulouse CEDEX France Phone: +33/(0)5 61 33 63 63 Fax: +33/(0)5 61 33 64 11 E-mail: Bernard.Berthomieu@laas.fr