fond
Model Checking Contest 2019
9th edition, Prague, Czech Republic, April 7, 2019 (TOOLympics)
About the NUPN Format
Last Updated
Apr 15, 2019

1. Motivation

One goal of the Model Checking Contest (MCC) is to progress the capabilities of verification tools for concurrent systems by assessing them on benchmarks of increasing complexity.

In this respect, one must notice that there exist instances of certain MCC benchmarks that have not been successfully handled by any tool so far.

There may be various explanations for this situation. One plausible explanation is based on the following observations:

It is therefore highly desirable to provide the MCC competing tools with information about the concurrent structure of MCC benchmarks when such information is available, which is the case for those models obtained from higher-level specifications.

Clearly, such additional information should remain optional, so that competing tools are free to use it or not. To use a metaphor, the situation would be similar in a matrix-computation contest, where matrices would be provided as the central information, together with additional information on zero blocks, which certain tools may wish to take advantage of to improve their performance and scale to larger problems.

2. Nested-Unit Petri Nets (NUPN)

At present, information about the concurrent structure of MCC benchmarks is only provided for P/T nets that are ordinary (i.e., all arc weights are equal to one) and one-safe. Colored models and non-ordinary or non-safe P/T nets are not concerned.

To represent the concurrent structure, we rely of on the concept of Nested-Unit Petri Nets (NUPN) proposed in [Gar19] (see also [Gar89] [GS90] [GS06] [Gar15]). This approach is an upward-compatible extension of P/T nets and relies on a reduced number of definitions:

3. Definition of the NUPN-toolspecific section

For MCC benchmarks with known information about their concurrent structure, this information is made available in a "toolspecific" section of the PNML file, i.e., an XML element enclosed between:

   <toolspecific tool="nupn" version="1.1">
and:
   </toolspecific>
that is located either inside the "net" element or inside the (supposedly unique) "page" element of the PNML file.

According to the conventions of the PNML format, all "toolspecific" sections (including the NUPN one) are optional, so that tools are free to process or ignore these sections.

To indicate which MCC models provide such additional information, a new structural property has been added to the MCC model forms. This property corresponds to the LaTeX macro \HasModelNestedUnits and is displayed as "nested units" in the PDF model forms. It is set to True if and only if the PNML file(s) of the model instance(s) has(ve) a NUPN-toolspecific section.

Note: there also exists an alternative, non-PNML, text-based format for representing Nested-Unit Petri Nets (see here for a definition of this format). MCC benchmarks for which \HasModelNestedUnits is True could be also provided in this format if some tools, which are not based on Petri net theory and do not embedd a PNML parser, want to participate to MCC.

The reminder of this section concisely defines the syntax and semantic constraints for NUPN-toolspecific sections. This presentation is mostly intended to users interested in quickly grasping how NUPN-toolspecific sections are organized, and to users who want to write or read such sections using hand-written generators or parsers. To also support XML-based automatic code generation, standardized definitions of the NUPN-toolspecific format using XSD (XML Schema Definition), DTD (Document Type Definitions), and RELAX NG are given in Section 5 below.

The contents of a NUPN-toolspecific section can be defined in five main steps, numbered from (a) to (e).

4. Example of a NUPN-toolspecific section

At present (December 2014), the six following benchmarks have a NUPN-toolspecific section: ARMCacheCoherence, EnergyBus, MultiwaySync, ProductionCell, UtahNoC, and Vasy2003. However, this list is expected to grow with the introduction of new "surprise" models and with the addition of NUPN-toolspecific sections for already known benchmarks.

The following fragment taken from the PNML file of the MCC model ARMCacheCoherence (2014) illustrates the syntax of a NUPN-toolspecific section; this model has the typical "communicating automata" structure, as it consists of 12 concurrent units, all nested in a root unit "u0", which has no local places; noticeably, the number of units remains small, even when the numbers of arcs and transitions get large:

   <toolspecific tool="nupn" version="1.1">
      <size places="87" transitions="33676" arcs="246935"/>
      <structure units="13" root="u0" safe="true">
         <unit id="u0">
            <places>p0</places>
            <subunits>u1 u2 u3 u4 u5 u6 u7 u8 u9 u10 u11 u12</subunits>
         </unit>
         <unit id="u1">
            <places>p1 p2 p3 p4 p5</places>
            <subunits/>
         </unit>
         <unit id="u2">
            <places>p6 p7</places>
            <subunits/>
         </unit>
         <unit id="u3">
            <places>p8 p9</places>
            <subunits/>
         </unit>
         <unit id="u4">
            <places>p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24</places>
            <subunits/>
         </unit>
         <unit id="u5">
            <places>p25 p26 p27 p28 p29 p30 p31 p32 p33 p34 p35 p36 p37 p38 p39</places>
            <subunits/>
         </unit>
         <unit id="u6">
            <places>p40 p41 p42 p43 p44 p45 p46 p47 p48 p49 p50 p51 p52 p53 p54</places>
            <subunits/>
         </unit>
         <unit id="u7">
            <places>p55 p56 p57 p58 p59 p60 p61 p62 p63 p64 p65 p66 p67 p68 p69</places>
            <subunits/>
         </unit>
         <unit id="u8">
            <places>p70 p71</places>
            <subunits/>
         </unit>
         <unit id="u9">
            <places>p72 p73 p74</places>
            <subunits/>
         </unit>
         <unit id="u10">
            <places>p75 p76 p77 p78</places>
            <subunits/>
         </unit>
         <unit id="u11">
            <places>p79 p80 p81 p82</places>
            <subunits/>
         </unit>
         <unit id="u12">
            <places>p83 p84 p85 p86</places>
            <subunits/>
         </unit>
      </structure>
   </toolspecific>

5. Grammars for the NUPN-toolspecific section

5.1. XML Schema Definition (XSD)

This is an XSD description of the NUPN-toolspecific section:

   <?xml version="1.0" encoding="utf-8"?>
   <xsd:schema elementFormDefault="qualified" xmlns:xsd="http://www.w3.org/2001/XMLSchema">

   <xsd:element name="toolspecific">
      <xsd:complexType>
         <xsd:sequence>
            <xsd:element name="size" type="sizeType"/>
            <xsd:element name="structure" type="structureType"/>
         </xsd:sequence>
         <xsd:attribute name="tool" type="xsd:string" fixed="nupn"/>
         <xsd:attribute name="version" type="xsd:decimal" fixed="1.1"/>
      </xsd:complexType>
   </xsd:element>

   <xsd:complexType name="sizeType">
      <xsd:attribute name="places" type="xsd:positiveInteger" use="required"/>
      <xsd:attribute name="transitions" type="xsd:nonNegativeInteger" use="required"/>
      <xsd:attribute name="arcs" type="xsd:nonNegativeInteger" use="required"/>
   </xsd:complexType>

   <xsd:complexType name="structureType">
      <xsd:sequence>
         <xsd:element name="unit" type="unitType" maxOccurs="unbounded"/>
      </xsd:sequence>
      <xsd:attribute name="units" type="xsd:positiveInteger" use="required"/>
      <xsd:attribute name="root" type="xsd:IDREF" use="required"/>
      <xsd:attribute name="safe" type="xsd:boolean" use="required"/>
   </xsd:complexType>

   <xsd:complexType name="unitType">
      <xsd:sequence>
         <xsd:element name="places" type="placeList"/>
         <xsd:element name="subunits" type="unitList"/>
      </xsd:sequence>
      <xsd:attribute name="id" type="xsd:ID" use="required"/>
   </xsd:complexType>

   <xsd:simpleType name="placeList">
      <xsd:list itemType="xsd:IDREF"/>
   </xsd:simpleType>

   <xsd:simpleType name="unitList">
      <xsd:list itemType="xsd:IDREF"/>
   </xsd:simpleType>

   </xsd:schema>

There are additional syntactic and semantics constraints that are not captured by this XSD specification:

5.2. Document Type Definition (DTD)

This is a DTD description of the NUPN-toolspecific section:

   <!ELEMENT toolspecific (size, structure)>
   <!ATTLIST toolspecific
       tool NMTOKEN #FIXED "nupn" 
       version NMTOKEN #FIXED "1.1">
   <!ELEMENT size EMPTY>
   <!ATTLIST size
      places      NMTOKEN #REQUIRED
      transitions NMTOKEN #REQUIRED
      arcs        NMTOKEN #REQUIRED>
   <!ELEMENT structure (unit)+>
   <!ATTLIST structure
      units NMTOKEN #REQUIRED
      root  IDREF #REQUIRED
      safe  (true | false) #REQUIRED>
   <!ELEMENT unit (places, subunits)>
   <!ATTLIST unit
      id ID #REQUIRED>
   <!ELEMENT places (#PCDATA)*>
   <!ELEMENT subunits (#PCDATA)*>

This DTD is shorter but less stringent than the XSD specification above. These are additional restrictions that cannot be expressed in the DTD framework:

5.3. RELAX NG (Compact Syntax) Schema Definition (RNC)

This is a RNC description of the NUPN-toolspecific section:

   element toolspecific {
      attribute tool { "nupn" },
      attribute version { "1.1" },
      element size {
         attribute places { xsd:positiveInteger },
         attribute transitions { xsd:nonNegativeInteger },
         attribute arcs { xsd:nonNegativeInteger },
         empty
      },
      element structure {
         attribute units { xsd:positiveInteger },
         attribute root { xsd:IDREF },
         attribute safe { xsd:boolean },
         element unit {
            attribute id { xsd:ID },
            element places {
               list { xsd:IDREF* }
            },
            element subunits {
               list { xsd:IDREF* }
            }
         }+
      }
   }

5.4. RELAX NG (XML Syntax) Schema Definition (RNG)

This is a RNG description of the NUPN-toolspecific section:

   <?xml version="1.0" encoding="UTF-8"?>
   <element name="toolspecific"
            xmlns="http://relaxng.org/ns/structure/1.0"
            datatypeLibrary="http://www.w3.org/2001/XMLSchema-datatypes">
      <attribute name="tool">
         <value>nupn</value>
      </attribute>
      <attribute name="version">
         <value>1.1</value>
      </attribute>
      <element name="size">
         <attribute name="places">
            <data type="positiveInteger"/>
         </attribute>
         <attribute name="transitions">
            <data type="nonNegativeInteger"/>
         </attribute>
         <attribute name="arcs">
            <data type="nonNegativeInteger"/>
         </attribute>
         <empty/>
      </element>
      <element name="structure">
         <attribute name="units">
            <data type="positiveInteger"/>
         </attribute>
         <attribute name="root">
            <data type="IDREF"/>
         </attribute>
         <attribute name="safe">
            <data type="boolean"/>
         </attribute>
         <oneOrMore>
            <element name="unit">
               <attribute name="id">
                  <data type="ID"/>
               </attribute>
               <element name="places">
                  <list>
                     <zeroOrMore>
                        <data type="IDREF"/>
                     </zeroOrMore>
                  </list>
               </element>
               <element name="subunits">
                  <list>
                     <zeroOrMore>
                        <data type="IDREF"/>
                     </zeroOrMore>
                  </list>
               </element>
            </element>
         </oneOrMore>
      </element>
   </element>

6. References

[Gar89] Hubert Garavel. Compilation et Vérification de Programmes LOTOS. Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989.

[GS90] Hubert Garavel and Joseph Sifakis. Compilation and Verification of LOTOS Specifications. Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification (Ottawa, Canada), pages 379-394, June 1990.

[GS06] Hubert Garavel and Wendelin Serwe. State Space Reduction for Process Algebra Specifications. Theoretical Computer Science, 351(2) 131-145, February 2006.

[Gar15] Hubert Garavel. Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets. Proceedings of the 36th International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS'15), Brussels, Belgium, June 2015.

[Gar19] Hubert Garavel. Nested-Unit Petri Nets. Journal of Logical and Algebraic Methods in Programming, vol. 104, pages 60-85, April 2019.

For more information about Nested-Unit Petri Nets, see the definition of the NUPN file format and the manual pages of the PNML2NUPN and CAESAR.BDD tools. Notice that these tools do not compete against other tools in the MCC but are used by the MCC team to automatically fill in and validate model forms.


Hubert Garavel. Version 1.2 (July 31, 2019).