Name of tool: Integrated Net Analyser INA
Version number: 2.1
Year of completion: First shipped 1992, current version 1998
Language of tool: English
Language of documentation: German
Environment:
Computer system: SUN-Workstation with Sun-OS or Solaris
IBM-PC and compatibles with MS-DOS,
MS-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: INA Manual
INA Handbuch
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.
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. Formulas expressed in the Computational Tree
Logic (CTL) - built using state predicates - can be checked.
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.
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.
Hints:
INA reads and writes data from/to ASCII-files with different
file extensions. If INA needs data, a default file name is
proposed. By typing <cr> you can accept the proposed name.
Otherwise you can overwrite the name. In case of misprinting,
do not use the <del>-key but rather <?> to move the cursor
to the left and <space> to move it to the right.
If there is no file of the required type, or if you want to
create new data, reply with <esc> you will then be given
the opportunity to input data from the terminal.
INA will automatically generate the following files:
SESSION.INA: contains all the results of your last session;
overwritten in the following session;
OPTIONS.INA: keeps the options set by the user for the next session;
COMMAND.INA: (created on demand only) contains all your inputs
so that the last session can be repeated without
any typing by answering "Same procedure as last
time?" with <Y>;
INVARI.HLP: contains computed (unformatted) invariants.
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/
INA 2.1: MS-DOS [ina.exe]
INA 2.2: Sun-OS 4 [INAsunos4.gz]
Sparc-Solaris [INAsolaris.gz]
Linux [INAlinux.gz]
MS-Windows 95/98/NT [INAwin32.exe]
Release note: PostScript [relnote.ps]
INA-Handbuch: PostScript [handbuch.ps]
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.
Contact:
Prof. Dr. Peter. H. Starke
Humboldt-Universitaet zu Berlin
Institut fuer Informatik
Lehrstuhl fuer Automaten- und Systemtheorie
Unter den Linden 6
D-10099 Berlin
Phone:(+49)(30) 20 181 - 285
Fax: (+49)(30) 20 181 - 287
Email:starke@informatik.hu-berlin.de
Witzenhauser Strasse 26
D-13053 Berlin-Hohenschoenhausen
Phone: (+49)(30) 982 1441