next up previous contents index
Next: Preface Up: Lehrstuhl für Automaten und Systemtheorie Previous: Version 2.1

INA
Integrated Net Analyzer

INA


Name of tool:
Integrated Net Analyzer INA
Version number:
2.2
Year of completion:
First shipped 1992, current version 1999
Language of tool:
English
Language of documentation:
English and German
Environment:
Computer system:
SUN-Workstation with Sun-OS or Solaris
IBM-PC and compatibles with Windows 95/98/NT or Linux
Open/closed system:
Open
Source program language:
MODULA-2
Extensibility:
Communication with the programm and between its parts is done by ASCII-files, the user may interfere with own programs.
Availability:
Prices:
Executable program: free.
Consulting services, source code: to be negotiated.
Documentation:
Manual

Functionality:
INA is a tool package supporting the analysis of Place/Transition Nets (Petri Nets) and Coloured Petri nets.

INA combines the following:

The editor gives the possibility to construct and to edit nets. One can use any graphical editor, too, if one knows the structure of its database file, by writing a program which converts to the INA-file format.

The by-hand simulation part allows starting at a given marking to forward fire either single transitions or maximal steps; the user can thus traverse parts of the reachability graph.

The reduction part can be used to reduce the size of a net (and of its reachability graph) whilst preserving liveness and boundedness.

The analysis can be carried out under different transition rules (normal, safe, under capacities), with or without priorities or time restrictions (three types), and under firing of single transitions or maximal sets of concurrently enabled transitions.

The analysis part contains a small expert system which infers - from the known ones - further properties of the given net.

The structural informations computed include:

For certain subclasses of nets, these properties can be used to deduce dynamic properties.

Invariant analysis can be done by computing generator sets of all place/transition invariants and of all non negative invariants. Vectors can be tested for invariance properties.

For checking boundedness and coverability, the coverability graph of the actual net can be computed using either the Karp-Miller algorithm or Finkel's method.

For bounded nets, the reachability graph can be computed and analysed for liveness, reversability, dynamic conflicts, realisable transition invariants, livelocks etc. The symmetries of the given net can be computed and used to reduce the size of the reachability graph. It is also possible to apply stubborn reduction. Formulas expressed in the Computational Tree Logic (CTL) - built using state predicates - can be checked.

Furthermore, minimal paths can be computed, and the nonreachability of a marking can be decided.

No restrictions are imposed on the size of the net, except, of course, the RAM-capacity of the computer used. During a session, all commands and options are saved to a command file, so that the session can be repeated automatically with a different net.

Download:
The official anonymous FTP site is: ftp.informatik.hu-berlin.de, directory /pub/local/petritool

The official Web site is: www.informatik.hu-berlin.de/lehrstuehle/automaten/ina/

The program and the documentation come without any warranty and are free for any non-commercial use. The MODULA-2 source code is available; for terms and conditions (to be negotiated), contact us.

Registration:
There is no need for registration. However, please fill out this form. The data will be sent by mail to us for statistical and support purposes only. We thank you for your time and cooperation.
Institution:
Location:
Name:
Email Address:
Operating system: Sun-OS 4 Solaris Linux Windows 95/98/NT DOS

Contact:
Prof. Dr. Peter. H. Starke

Humboldt-Universität zu Berlin
Institut für Informatik
Lehrstuhl für Automaten- und Systemtheorie

Unter den Linden 6
D-10099 Berlin

Telefon: (+49) (30) 2093 3078
Fax: (+49) (30) 2093 3081

Email: starke@informatik.hu-berlin.de


INA
Integrated Net Analyzer
Version 2.2

Manual

Stephan Roch
Prof. Peter H. Starke

Humboldt-Universität zu Berlin
Institut für Informatik
Lehrstuhl für Automaten- und Systemtheorie
Unter den Linden 6
10099 Berlin


Full-text search in this manual


The following formats can be downloaded here:

Example nets of the manual (zip/pkzip packed) [5 kB]

Manual of version 1.7 [only in german]

Manual of version 2.1 [only in german]

Top of this page



next up previous contents index
Next: Preface Up: Lehrstuhl für Automaten und Systemtheorie Previous: Version 2.1

© 1996-99 Prof. Peter H. Starke (starke@informatik.hu-berlin.de) und Stephan Roch (roch@...)

INA Manual Version 2.2 (last changed 1999-11-17)