NUPN manual page
Table of Contents

Name

nupn, NUPN - Nested-Unit Petri Nets

Description

Nested-Unit Petri Nets (NUPN, for short) are a theoretical model of concurrency. Technically, they extend ordinary, one-safe Petri Nets with structure and locality, by grouping sets of places into hierarchically nested "units". This semantic model is particularly suitable when translating specifications written in high-level concurrent languages (such as process calculi), as structural information can be preserved to make later analyses more efficient and scalable. For further details, refer to the [Gar15] paper listed below in the BIBLIOGRAPHY section.

In practice, the theoretical NUPN model is implemented in two different ways:

The remainder of this manual page defines the latter format, which is referred to as the "NUPN format".

Conversion from PNML to NUPN can be done using the PNML2NUPN tool (see below), whereas conversion from NUPN to PNML (with NUPN-specific extension) can be achieved by invoking the caesar.bdd tool with its -pnml option.

Syntax of the NUPN Format

The format of filename.nupn is defined by the following BNF grammar (in which "nb" stands for "number"):
<nested-unit-petri-net> ::= 
   <pragma-description>*
   places #<nb-of-places> <min-place-nb>...<max-place-nb>\n
   <initial-marking-description>
   units #<nb-of-units> <min-unit-nb>...<max-unit-nb>\n
   root unit <root-unit-nb>\n
   <unit-description>*\n
   transitions #<nb-of-trans> <min-trans-nb>...<max-trans-nb>\n
   <trans-description>*\n
<pragma-description> ::= !<character-string>\n
<initial-marking-description> ::=
   initial place <init-place-nb>\n
 | initial places #<nb-of-initial-places> <initial-place-list>\n
<unit-description> ::=
   U<unit-nb>
   #<nb-of-subplaces> <min-subplace-nb>...<max-subplace-nb>
   #<nb-of-subunits> <subunit-list>\n
<trans-description> ::=
   T<transition-nb> 
   #<nb-of-input-places> <input-place-list>
   #<nb-of-output-places> <output-place-list>\n
<initial-place-list>   ::= <place-nb>*
<input-place-list>     ::= <place-nb>*
<output-place-list>    ::= <place-nb>*
<subunit-list>         ::= <unit-nb>*
<nb-of-places>         ::= <unsigned-integer>
<min-place-nb>         ::= <unsigned-integer>
<max-place-nb>         ::= <unsigned-integer>
<init-place-nb>        ::= <unsigned-integer>
<place-nb>             ::= <unsigned-integer>
<nb-of-units>          ::= <unsigned-integer>
<min-unit-nb>          ::= <unsigned-integer>
<max-unit-nb>          ::= <unsigned-integer>
<root-unit-nb>         ::= <unsigned-integer>
<unit-nb>              ::= <unsigned-integer>
<nb-of-trans>          ::= <unsigned-integer>
<min-trans-nb>         ::= <unsigned-integer>
<max-trans-nb>         ::= <unsigned-integer>
<nb-of-subplaces>      ::= <unsigned-integer>
<min-subplace-nb>      ::= <unsigned-integer>
<max-subplace-nb>      ::= <unsigned-integer>
<nb-of-subunits>       ::= <unsigned-integer>
<transition-nb>        ::= <unsigned-integer>
<nb-of-input-places>   ::= <unsigned-integer>
<nb-of-output-places>  ::= <unsigned-integer>

Note 1: inserting spaces just after "!" and "#", or around "..." is not permitted by the syntax.

Note 2: in <initial-marking-description>, the first form:

   initial place <init-place-nb>\n
is a shorthand for the second form and, namely, is equivalent to:
   initial places #1 <init-place-nb>\n
The first form is an early syntax, kept for backward compatibility reasons. In the sequel, we may only consider the second form.

Note 3: unless otherwise stated, all <unsigned-integer> values are assumed to be smaller than 2^31.

Static Semantics of the NUPN Format

A few preliminary definitions are needed:

A valid NUPN file should satisfy the following constraints:

In <nested-unit-petri-net>:
  1.  <nb-of-places> > 0     -- a net has at least one place
  2.  <max-place-nb> - <min-place-nb> + 1 = <nb-of-places>
  3.  <nb-of-units> > 0     -- a net has at least one unit
  4.  <max-unit-nb> - <min-unit-nb> + 1 = <nb-of-units>
  5.  <min-unit-nb> <= <root-unit-nb> <= <max-unit-nb>
  6.  <nb-of-trans> >= 0    -- a net may have zero transition
  7.  <nb-of-trans> = 0 => <min-trans-nb> = 1 and <max-trans-nb> = 0
      -- the empty interval of transitions is canonically noted 1...0
  8.  <max-trans-nb> - <min-trans-nb> + 1 = <nb-of-trans>
In <initial-marking-description>:
  9.  <min-place-nb> <= <init-place-nb> <= <max-place-nb>
 10.  0 <= <nb-of-initial-places> <= <nb-of-places>
 11.  Length (<initial-place-list>) = <nb-of-initial-places>
 12.  for each pair <place-nb> and <place-nb>' in <initial-place-list>
      one must have: Disjoint (Unit (<place-nb>), Unit (<place-nb>'))
      -- the initial places must belong to disjoint units (and are
      -- thus pairwise distinct); see discussion below about this rule
In each <unit-description>:
 13.  <min-unit-nb> <= <unit-nb> <= <max-unit-nb>
 14.  0 <= <nb-of-subplaces> <= <nb-of-places>
 15.  <nb-of-subplaces> = 0 => <min-subplace-nb> = 1
                           and <max-subplace-nb> = 0
      -- the empty interval of places is canonically noted 1...0
 16.  <min-place-nb> <= <min-subplace-nb> <= <max-place-nb>
 17.  <min-place-nb> <= <max-subplace-nb> <= <max-place-nb>
 18.  <max-subplace-nb> - <min-sublace-nb> + 1 = <nb-of-subplaces>
 19.  0 <= <nb-of-subunits> <= <nb-of-units>
 20.  Length (<subunit-list>) = <nb-of-subunits>
Globally to all <unit-description>s:
 21.  each <unit-nb> occurs once and only once after a "U"
 22.  the sum of all <nb-of-subplaces> is equal to <nb-of-places>
 23.  all intervals <min-subplace-nb>...<max-subplace-nb> form
      a partition of <min-place-nb>...<max-place-nb>
 24.  the sum of all <nb-of-subunits> is equal to <nb-of-units> - 1
 25.  <root-unit-number> and all non-empty <subunit-list>s form
      a partition of <min-unit-nb>...<max-unit-nb>
In each <subunit-list>:
 26.  <min-unit-nb> <= <unit-nb> <= <max-unit-nb>
 27.  <unit-nb> != <root-unit-nb> -- the root unit is not a
                                  -- sub-unit of any other unit
In each <trans-description>:
 28.  <min-trans-nb> <= <trans-nb> <= <max-trans-nb>
 29.  0 <= <nb-of-input-places> <= <nb-of-places>
 30.  Length (<input-place-list>) = <nb-of-input-places>
 31.  0 <= <nb-of-output-places> <= <nb-of-places>
 32.  Length (<output-place-list>) = <nb-of-output-places>
 33.  <input-place-list> is included in <output-place-list>
      => <input-place-list> is equal to <output-place-list>
      -- see discussion below about this rule
Globally to all <trans-description>s:
 34.  each <trans-nb> occurs once and only once after a "T"
In each <input-place-list> and each <output-place-list>
 35.  <min-place-nb> <= <place-nb> <= <max-place-nb>
 36.  for each pair <place-nb> and <place-nb>' in the list, one
      must have: Disjoint (Unit (<place-nb>), Unit (<place-nb>'))
      -- the input (resp. output) places of each transition must
      -- belong to disjoint units (and are thus pairwise distinct);
      -- see discussion below about this rule

Note 1: It is possible that:

   <nb-of-units> <= <nb-of-places>
in the case, e.g., where all places are contained in one single unit. Conversely, it is also possible that:
   <nb-of-places> <= <nb-of-units>
in the case, e.g., where each place is contained in a specific unit.

Note 2: when there is a single initial place, it is often in the root unit, but this is not mandatory (this would be even impossible when the root unit has no local place).

Dynamic Semantics of the NUPN Format

The dynamic semantics of Nested-Unit Petri Nets follows the same rules as Petri Nets that are ordinary (i.e., all arcs have multiplicity one) and safe (i.e., each place contains at most one token):

Additionally, each reachable marking M should satisfy the "unit safe" property, which is defined as follows:

  1. If M has a token in some place P, then M has no token in any other place P' local to the same unit as P, i.e., Unit (P) = Unit (P'). The particular case where P=P' prohibits having two tokens in the same place, thus implying that the net is one-safe.
  2. If M has a token in some place P local to U = Unit (P), there is no token in any place local to any other unit U' that transitively contains U or is transitively contained in U, i.e., Sub* (U, U') or Sub* (U', U). Said differently, if a unit is active, all its ancestor units and descendent units are inactive.

Conditions (1) and (2) can be summarized as follows: a marking M is unit safe iff for each pair of places P and P' marked in M, P <> P' => Disjoint (Unit (P), Unit (P')).

Deciding whether all reachable markings of a NUPN model are unit safe requires, in general, to build the graph of reachable markings. However, some structural checks allow to detect, on the basis of sufficient conditions, certain NUPN models that are likely not to be unit safe. This is the case of three aforementioned rules of the static semantics:

Note: it is neither required that a NUPN is connected, nor that all places can be reachable from the initial marking, nor that all transitions are quasi-live (i.e., can be fired from at least one reachable marking). However, caesar.bdd invoked with option -check warns about such situations.

Supported Pragmas of the NUPN Format

Pragmas provide optional information about a NUPN model. If present, pragmas occur at the very beginning of a NUPN file; they always start with the "!" character and terminate with the end of the line. The following pragmas are currently supported:

Pragma "creator"

The syntax of this pragma is:
   !creator <character-string>

<character-string> should contain the name of the tool that produced the NUPN file, possibly followed by the version number of this tool and (if relevant) the command-line options given to this tool when it was invoked. This pragma is mostly intended for traceability.

Pragma "unit_safe"

The syntax of this pragma is either:
   !unit_safe
or:
   !unit_safe <character-string>

If present, this pragma certifies that all reachable markings of the NUPN model are unit safe. In the first form, unit safeness is certified by the creator tool (if the "!creator" pragma is present). In the second form, unit safeness has been certified by another tool, the name, version number, and (if relevant) command-line options are given in <character-string>.

Pragma "multiple_initial_tokens"

The syntax of this pragma is:
   !multiple_initial_tokens #<nb-tokens>
   #<nb-places> <min>...<max>
As for all pragmas, these syntactic elements must appear on one single line.

<nb-tokens>, <min>, and <max> are unsigned integers that may be greater than 2^31 but must be smaller than 2^63.

By inserting this pragma, the creator tool indicates that the NUPN model has been derived from a original Petri Net, in the initial marking of which certain places contain more than one token. In the NUPN model, the initial number of tokens in such places is implicitly reduced to one.

Thus, this pragma and the unit_safe pragma are mutually exclusive.

The arguments of this pragma are computed, on the original Petri Net, as follows:

The following constraints should hold, where <nb-of-initial-places> denotes the number of initial places given in the <initial-marking-description>:

   <nb-of-initial-places> + <nb-places> * (<min> - 1)
   <= <nb-tokens> <=
   <nb-of-initial-places> + <nb-places> * (<max> - 1)

Pragma "multiple_arcs"

The syntax of this pragma is:
   !multiple_arcs
   #<nb-trans-in> #<nb-trans-out> #<nb-trans-inout>
   <min-in>...<max-in> <min-out>...<max-out>
   <min-diff>...<max-diff>
As for all pragmas, these syntactic elements must appear on one single line.

By inserting this pragma, the creator tool indicates that the NUPN model has been derived from a original Petri Net, in which certain input arcs (i.e., from a place to a transition) and/or output arcs (i.e., from a transition to a place) have a valuation (or "inscription", in PNML terminology) greater than one. Such arcs are called "multiple input arcs" and "multiple output arcs", respectively. In the NUPN model, the valuation of all arcs is implicitly reduced to one.

Thus, this pragma and the unit_safe pragma are mutually exclusive.

The arguments of this pragma are computed, on the original Petri Net, as follows:

Example of a NUPN File

This is an example of a valid NUPN file:
   !creator caesar
   !unit_safe
   places #7 0...6
   initial place 0
   units #3 0...2
   root unit 0
   U1 #4 1...4 #0 
   U2 #2 5...6 #0 
   U0 #1 0...0 #2 1 2 
   transitions #5 0...4
   T0 #1 0 #2 1 5 
   T1 #2 3 6 #2 2 5 
   T2 #2 1 5 #2 4 6 
   T3 #1 2 #1 1 
   T4 #1 4 #1 3 

How to Create a NUPN File

At present, there are two ways of producing NUPN models:

How to Read a NUPN File

At present, there is one single CADP tool, caesar.bdd , that reads and processes NUPN files. This tool, when invoked with its -check option, is the reference parser and semantic checker for the NUPN format.

Bibliography

[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. Related slideshow available from http://cadp.inria.fr/publications/Garavel-15-a.html

See Also

caesar.bdd , caesar

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.

Bugs

Please report bugs to cadp@inria.fr


Table of Contents