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 [Gar19] 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 (where <element>? denotes zero or one ocurrences of <element>, where <element>* denotes zero or many occurrences of <element>, and where "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
   <label-description>?

<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<trans-nb> 
   #<nb-of-input-places> <input-place-list>
   #<nb-of-output-places> <output-place-list>\n

<label-description> ::=
   labels <place-flag> <trans-flag> <unit-flag> <label-length>\n
   <place-label>*
   <trans-label>*
   <unit-label>*

<place-label> ::= p<place-nb> <label>\n
<trans-label> ::= t<trans-nb> <label>\n
<unit-label>  ::= u<unit-nb> <label>\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>
<trans-nb>             ::= <unsigned-integer>
<nb-of-input-places>   ::= <unsigned-integer>
<nb-of-output-places>  ::= <unsigned-integer>
<label-length>         ::= <unsigned-integer>

<place-flag>           ::= 0 | 1
<trans-flag>           ::= 0 | 1
<unit-flag>            ::= 0 | 1

<label>                ::= <character-string>

<unsigned-integer> denotes a non-empty sequence of decimal digits representing an integer value smaller than 2^31.

<character-string> denotes a non-empty sequence of printable characters.

In order to keep the NUPN format simple and easy to process using script languages (such as Awk), the rules for spacing are strict: tabulations are prohibited; multiple spaces are not allowed where a single space is; spaces are not permitted at the beginning or end of a line; empty or blank lines are forbidden.

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 only consider the second form.

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

In <label-description>:
 37. if <place-flag> = 0, there are no occurrences of <place-label>
     -- places are not labelled
 38. if <place-flag> = 1, there are <nb-of-places> occurrences of
     <place-label> -- all places are labelled
 39. if <trans-flag> = 0, there are no occurrences of <trans-label>
     -- transitions are not labelled
 40. if <trans-flag> = 1, there are <nb-of-trans> occurrences of
     <trans-label> -- all transitions are labelled
 41. <nb-of-trans> = 0 => <trans-flag> = 0
 42. if <unit-flag> = 0, there are no occurrences of <unit-label>
     -- units are not labelled
 43. if <unit-flag> = 1, there are <nb-of-units> occurrences of
     <unit-label> -- all units are labelled

In each <place-label>:
 44. <min-place-nb> <= <place-nb> <= <max-place-nb>

Globally to all <place-label>s:
 45. each <place-nb> occurs once and only once after a "p"
     -- thus all <place-nb>s are pairwise distinct, but it is not
     -- required that all <character-string>s are pairwise distinct

In each <trans-label>:
 46. <min-trans-nb> <= <trans-nb> <= <max-trans-nb>

Globally to all <trans-label>s:
 47. each <trans-nb> occurs once and only once after a "t"
     -- thus all <trans-nb>s are pairwise distinct, but it is not
     -- required that all <character-string>s are pairwise distinct

In each <unit-label>:
 48. <min-unit-nb> <= <unit-nb> <= <max-unit-nb>

Globally to all <unit-label>s:
 49. each <unit-nb> occurs once and only once after a "u"
     -- thus all <unit-nb>s are pairwise distinct, but it is not
     -- required that all <character-string>s are pairwise distinct

In each <label>:
 50. strlen (<character-string>) <= <label-length>

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).

Note 3: as stated in rules 45, 47, and 49, the labelling of places, transitions, and units is not necessarily injective. For instance, several transitions may share the same label (e.g., the label "i" used to denote internal transitions in concurrent languages such as LOTOS and LNT).

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>

where <nb-places> denotes an <unsigned-integer> defined above, and where <nb-tokens>, <min>, and <max> are unsigned integers that may be greater than 2^31 but must be smaller than 2^63.

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 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:

In a valid NUPN file, this pragma should satisfy the following constraints, where <nb-of-initial-places> denotes the number of initial places given in the <initial-marking-description>: 

  51.  1 <= <nb-places> <= <nb-of-initial-places>
  52.  1 < <min> <= <max>
  53.  <nb-places> = 1 => <min> = <max>
  54.  <nb-tokens> >= (<nb-of-initial-places> - <nb-places>) +
                      ((<nb-places> - 1) * <min>) + <max>
  55.  <nb-tokens> <= (<nb-of-initial-places> - <nb-places>) +
                      <min> + ((<nb-places> - 1) * <max>)

A consequence of rule 51 is that, if there are zero initial places, the pragma multiple_initial_tokens should be absent. Said differently, the pragma "!multiple_initial_tokens #0 #0 0...0" is not allowed.

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>

where <nb-trans-in>, <nb-trans-out>, and <nb-trans-inout> are <unsigned-integer>s defined above, where <min-in>, <max-in>, <min-out>, and <max-out> are unsigned integers that may be greater than 2^31 but must be smaller than 2^63, and where <min-diff> and <max-diff> are signed integers on 64 bits.

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 that is not ordinary, i.e., 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, there are no multiple arcs.

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

If the net has no transition, this pragma may not be present.

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

In a valid NUPN file, this pragma should satisfy the following constraints, where <nb-of-trans> denotes the number of transitions given in the <nested-unit-petri-net> description: 

  56.  0 <= <nb-trans-in> <= <nb-of-trans>
  57.  0 <= <nb-trans-out> <= <nb-of-trans>
  58.  0 <= <nb-trans-inout> <= <nb-of-trans>
  59.  0 < <nb-trans-in> + <nb-trans-out> + <nb-trans-inout>
       <= <nb-of-trans>
  60.  <nb-trans-in> + <nb-trans-inout> = 0 =>
                             <min-in> = 1 and <max-in> = 0
  61.  <nb-trans-in> + <nb-trans-inout> = 1 =>
                             1 < <min-in> = <max-in>
  62.  <nb-trans-in> + <nb-trans-inout> > 1 =>
                             1 < <min-in> <= <max-in>
  63.  <nb-trans-out> + <nb-trans-inout> = 0 =>
                             <min-out> = 1 and <max-out> = 0
  64.  <nb-trans-out> + <nb-trans-inout> = 1 =>
                             1 < <min-out> = <max-out>
  65.  <nb-trans-out> + <nb-trans-inout> > 1 =>
                             1 < <min-out> <= <max-out>
  66.  <min-diff> <= <max-diff>

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 three 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

[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 [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

See Also

caesar.bdd , caesar , nupn_info

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 [email protected]

Table of Contents