INA
Integrated Net Analyzer

INA

Name of tool:

Integrated Net Analyzer INA

Version number:

2.2 - final - Jul 31 2003

Year of completion:

First shipped 1992, current version 2003

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/ME/NT/XP/2000/... 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:

a textual editor for nets
a by-hand simulation part
a reduction part for Place/Transition-nets
an analysis part to compute
- structural information
- place invariants, transition invariants
- reachability and coverability graphs.
These are then used to verify properties like boundedness, liveness, reversability, etc.
a model checker for the Computational Tree Logic (CTL)

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:

conflicts (static, dynamic) and their structure (e.g. free choice property),
deadlocks and traps (deadlock-trap-property)
state machine decomposition and covering.

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.

Some external graphical editors and tools can export nets to INA, e.g.

PEP: Programming Environment based on Petri Nets
PED: Hierarchical Petri Net Editor
PNK: Petri Net Kernel (see Java component pnt2pnk and the Phyton application inapilot on the application page)
Visual SimNet: Stochastic Queueing and Petri Net Simulator

and maybe many other tools not mentioned here.

inatcl/TkINA
INA is not directly usable as a computing engine for other applications (it is not possible to invoke algorithms from outside the program) and does not provide a graphical user interface. Therefore inatcl and TkINA were developed.

inatcl is a tcl-based interface to (some) functionality provided by INA. It allows to write simple applications using the interpreted scripting language tcl.

TkINA provides a graphical interface for starting analysis algorithms; some results are displayed in a textual format. It is integrated in the PEP tool (Programming Envorionment based on Petri Nets) and does not provide its own graphical editor. Within the PEP tool it can be used to generate and highlight e.g. invariants, deadlocks, and state machine components. Nevertheless TkINA can also be used as a standalone tool.

Download:

The official anonymous FTP site is not available anymore!

The official Web site is: www2.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.

Last update: Jul 31 2003 (see recent changes and the notes below)

Unix full version for Sun-OS 4 [gzip]
Unix full version for Sparc-Solaris [gzip]
Linux full version (see notes below)) [gzip] full version (statically linked) [gzip]
Windows-95/ME/NT/XP/2000/... full version [exe]
DOS demo version (only 2.1) [exe]
Manual

Note: If gunzip does not work (i.e. it says "not in gzip format") after retrieving a file for Unix or Linux, then (especially if you use Netscape) the file is gunziped on the fly during download. Please rename and change the access permissions for execution! File types can be determined with the standard Unix utility called "file".

New - additional note for Linux version only: The binary depends on some libraries which may not exist in compatible versions on your system. If you encounter an error like "./INAlinux: relocation error: ./INAlinux: symbol errno, version GLIBC_2.0 not defined in file libc.so.6 with link time reference" then try to set the environment variable LD_ASSUME_KERNEL to 2.4.1, i.e. export LD_ASSUME_KERNEL=2.4.1 for bash or setenv LD_ASSUME_KERNEL 2.4.1 for (t)csh. We also provide a statically linked version which does not need this workaround (see above).

Registration: