NUPN_INFO manual page

Table of Contents## Name

nupn_info - query and transformation of Nested-Unit Petri Nets
## Synopsis

**nupn_info**
*option* [ *arguments* ] [ *filename***.nupn** ]
## Description

Taking as input *filename***.nupn**
(or by default the standard input), which contains a Nested-Unit Petri
Net (NUPN) encoded in the **nupn**
format, **nupn_info** performs various
analyses or transformations, depending on the *option* specified on the
command-line, and writes the corresponding results to the standard output.
## Options

## NUPN
(Nested-Unit Petri Net) Format

See the **nupn**
manual page for a detailed
definition of the NUPN file format.
## Permutation Format

The *permutation* files
used by the options **-place-permute**, **-transition-permute**, and **-unit-permute** have
the same text file format. Each line has the form "*x* *y*", which denotes
that the place (resp. transition or unit) *x* is renumbered by the permutation
to the place (resp. transition or unit) *y*. Lines of the following form "*x*
*x*" can be omitted. Checks are made to ensure that the permutation file
defines a bijection.
## Exit Status

The exit status of **nupn_info** is zero if
execution went well; in such case, a valid NUPN file is written to the
standard output. Otherwise, a non-zero exit status is returned and an error
message may be displayed to the standard output.
## Author

Hubert Garavel (INRIA
Rhone-Alpes)
## Files

## Bibliography

[Gar19]
Hubert Garavel. "Nested-Unit Petri Nets". Journal of Logical and Algebraic
Methods in Programming, vol. 104, pages 60-85, April 2019. Available from
http://cadp.inria.fr/publications/Garavel-19.html
## See Also

**caesar.bdd**
,
**nupn**
## Bugs

Please report new
bugs to Hubert.Garavel@inria.fr

**-canonical-nupn**- Transform the input NUPN to put it under a canonical
form by applying the seven options "
**-essential-nupn", "**", "**-normal-nupn****-place-renumber**0", "**-transition-renumber**0", "**-transition-sort**", "**-unit-renumber**0", and "**-unit-sort**" described hereafter. This option can be useful to compare whethertwo NUPNs are "structurally" identical or not. **-essential-nupn**- Remove all pragmas and all (place, transition, and unit) labels, thus retaining only the core semantical part of the input NUPN.
**-normal-nupn**- Simplify (if possible) the
input NUPN to put it under a normal form. The following transformations
are applied: tabulations are replaced with spaces; empty or blank lines
are deleted; extra spaces are removed; the description of units and the
description of transitions are sorted by increasing numbers; the list of
sub-units of each unit is sorted by increasing numbers; the lists of input
and output places of each transition are sorted by increasing numbers;
any line of the following form "
`initial place %d`

" is replaced with "`initial places #1 %d`

"; any line of the following form "`labels 0 0 0 %d`

" is deleted; the maximal length of labels (4th argument of the "`labels`

" line) is recomputed and set to its minimal value. The resulting NUPN is displayed on the standard output. **-place-fusion**- Apply the place-fusion abstraction to the input NUPN, merging in each unit all the places of this unit into a single place. The resulting NUPN has as many places as it has non-void units. Places may be renumbered if merged places are deleted; unit and transition numbers are kept unchanged. The resulting NUPN is displayed on the standard output.
**-place-permute***permutation*- Renumber the places of the input NUPN according to the
*permutation*file. See below for a description of the format of this file. The min-max interval of place numbers is preserved by the permutation. **-place-renumber***N*- Renumber
all places of the input NUPN, setting the lowest place number to
*N*. All place numbers are modified by adding or substracting the same constant number. **-redundant-removal**- Eliminate all redundant units from the input NUPN,
i.e., units containing exactly one (directly nested) sub-unit. Units and places
may be renumbered if redundant units are deleted; transition numbers are
kept unchanged. If the input NUPN has no redundant unit, the only changes
applied are those performed by option
**-normal-nupn**. The resulting NUPN is displayed on the standard output. **-transition-permute***permutation*- Renumber
the transitions of the input NUPN according to the
*permutation*file. See below for a description of the format of this file. The min-max interval of transition numbers is preserved by the permutation. **-transition-renumber***N*- Renumber all transitions of the input NUPN, setting the lowest transition
number to
*N*. All transition numbers are modified by adding or substracting the same constant number. **-transition-sort**- Reorder the list of transitions
of the input NUPN according to the order defined by the
**-transition-order**option of**caesar.bdd**. **-trivial-units**- Erase the existing unit structure of the input NUPN and replace it with the trivial unit structure, in which each unit contains a single place, except the root unit, which has no place and contains all the other units. The resulting NUPN has as many non-void units as it has places. Units may be renumbered if new units are added; place and transition numbers are kept unchanged. The resulting NUPN is displayed on the standard output.
**-unit-permute***permutation*- Renumber the units of the
input NUPN according to the
*permutation*file. See below for a description of the format of this file. The min-max interval of unit numbers is preserved by the permutation. **-unit-renumber***N*- Renumber all units of the input NUPN,
setting the lowest unit number to
*N*. All unit numbers are modified by adding or substracting the same constant number. **-unit-sort**- Reorder the list of units
of the input NUPN according to the order defined by the
**-unit-order**option of**caesar.bdd**. **-void-removal**- Eliminate all void (non-root) units from
the input NUPN, i.e., units containing no local places. Units may be renumbered
if void units are deleted; place and transition numbers are kept unchanged.
If the input NUPN has no void (non-root) unit, the only changes applied
are those performed by option
**-normal-nupn**. The resulting NUPN is displayed on the standard output.

For performance reasons, **nupn_info** assumes that
the contents of the input NUPN are correct. When dealing with an unknown
NUPN, it is therefore advisable to first analyze its contents with the
**-check** option of **caesar.bdd**
. However, certain options (especially **-normal-nupn
and **) may transform an incorrect NUPN into a correct one.

`->`

`->`

*filename***.nupn**- Nested-Unit Petri Net (input)

[Gar15] Hubert Garavel. "Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets". In R. Devillers and A. Valmari, editors, Proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'15), Brussels, Belgium. Lecture Notes in Computer Science, vol. 9115, Springer, 2015. Superseded by [Gar19]. Available from http://cadp.inria.fr/publications/Garavel-15-a.html

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in
files **$CADP/INSTALLATION_*.**

Recent changes and improvements to this software
are reported and commented in file **$CADP/HISTORY.**