1. Motivation

The proposed models in the MCC come with some known (or unknown) structural and behavioral properties. These properties and their values are the ones you read in the model forms (PDF files). We will refer to these static properties as generic precomputed properties (or generic properties).

Up to 2017, the information about these properties could not be exploited by tools at runtime. Feedback from tools developers then revealed that it would be highly desirable to represent them in a machine-readable format as in the PNML files of the model instances. Such additional information should remain optional, so that competing tools are free to use it or not. In particular, a property such as SAFENESS is deemed usefull by tools developers.

PNML provides the toolspecific concept to make room for ad hoc additional information that the standard has not defined beforehand. We use this concept to encode the generic properties definitions in XML. However, this encoding is output in separate XML files alongside the PNML files of the models because not only the information it carries should remain optional, but also we want to avoid: i) cluttering the PNML files of the models, ii) growing them too large, and iii) introduce subtle errors.

The extracted information about these generic properties resides in two separate files:

the properties definitions that are output in a single file once and for all,
the properties values as extracted from the forms, in a verdicts file for each model.

The verdicts file references the considered model and the analyzed properties of that model.

The reason for separating the verdicts from the definitions is to design a future-proof approach that enables tools to produce verdicts in that format, therefore allowing automated processing of verdicts and traces in further sophisticated analysis workflows. Currently, the MCC runs competing tools against generated dynamic properties (e.g., CTL, LTL), that are encoded in a specific XML format and answered in one-line text outputs for result processing and score computation during the examinations. Beyond the examinations, and to enhance interoperability, the verdicts of these dynamic properties could also be produced by the tools in an XML-based format for off-line analysis.

This manual explains the definition of the generic precomputed properties. It links to the unique XML instance of this definition encoding the properties the MCC provides in a model form.

The properties verdicts dedicated manual explains the definition of properties verdicts.

2. Format of the Generic Precomputed Properties

An instance of the generic properties definition is made available in a toolspecific element at the root of a standalone XML file:

The toolspecific root element to encapsulate the generic precomputed properties definitions

The attributes tool and version are mandatory. They provide the displayed predefined values, genericpropertiesdefinition and 1.1, respectively. Every time the grammar of the generic properties definition will be updated, we will increment the version number.

Then, a mandatory, single properties element is created as a child element of the root element toolspecific:

properties element as a mandatory child element of toolspecific

Each property's definition resides in a property child element to the properties element.




All arcs have multiplicity one (i.e., are unity weighted).

Example of a generic property definition

A property consists of:

a mandatory name attribute specifying its name (spelled in capital letters);
a mandatory value attribute specifying the type of the property value;
an optional child element description, which provides a textual description of the property.

The properties definition grammar specifies allowed values for the name attribute (see section 4 below). They come straight from the current fixed set of properties in a model form. Consequently, the grammar will also be updated each time that set is updated. Currently, all listed properties take their value from a 3-valued Boolean set of literals {true, false, unknown}. This set is symbolically named Optional-Boolean (see. grammar in section 4).

3. MCC version of the Generic Precomputed Properties

The unique instance of the generic properties definition that the MCC provides includes all the properties you will find in current model forms. It is provided in the file named (follow the link) GenericPropertiesDefinition.xml.

4. Grammar for the Generic Precomputed Properties

To enable XML-based tool support, we provide below the grammar of the generic properties definition in RELAX NG Compact Syntax, RELAX NG XML Syntax, and XSD (XML Schema Definition).

4.1. Definition in RELAX NG Compact Syntax (RNC)

documentation [
    "Toolspecific element definition for named generic (structural and behavioral) properties in the MCC.\x{a}" ~
    "This definition does not handle generated dynamic properties whose formulas have another specific XML syntax\x{a}" ~
    "(cf. MCC formulas manual).\x{a}" ~
    "This definition enables instances where only properties, their names, descriptions, and value types are specified.\x{a}" ~
    "Version 1.1\x{a}" ~
    "Author: The Model Checking Contest Model Board\x{a}" ~
    "License: Apache Public License 2.0"
]

## Whitespace normalization is performed on enumerated values. 
## This means that, for example, "CONNECTED" matches " CONNECTED",  or " CONNECTED ".

optionalboolean-attr-content = attribute value { 
    ## Optional-Boolean represents the meta specification of
    ## the set {true, false, unknown}, i.e., xsd:boolean U {unknown}, 
    ## using a symbolic name.
   "Optional-Boolean"
 }

start =
    element toolspecific {
        attribute tool { "genericpropertiesdefinition" },
        attribute version { "1.1" },
        element properties {
            element property {
                ((attribute name { "CONNECTED" },
                  optionalboolean-attr-content)
                 | (attribute name { "CONSERVATIVE" },
                     optionalboolean-attr-content)
                 | (attribute name { "DEADLOCK" },
                     optionalboolean-attr-content)
                 | (attribute name { "EXTENDED_FREE_CHOICE" },
                     optionalboolean-attr-content)
                 | (attribute name { "LIVE" },
                     optionalboolean-attr-content)
                 | (attribute name { "LOOP_FREE" },
                     optionalboolean-attr-content)
                 | (attribute name { "MARKED_GRAPH" },
                     optionalboolean-attr-content)
                 | (attribute name { "NESTED_UNITS" },
                     optionalboolean-attr-content)
                 | (attribute name { "ORDINARY" },
                     optionalboolean-attr-content)
                 | (attribute name { "QUASI_LIVE" },
                     optionalboolean-attr-content)
                 | (attribute name { "REVERSIBLE" },
                     optionalboolean-attr-content)
                 | (attribute name { "SAFE" },
                     optionalboolean-attr-content)
                 | (attribute name { "SIMPLE_FREE_CHOICE" },
                     optionalboolean-attr-content)
                 | (attribute name { "SINK_PLACE" },
                     optionalboolean-attr-content)
                 | (attribute name { "SINK_TRANSITION" },
                     optionalboolean-attr-content)
                 | (attribute name { "SOURCE_PLACE" },
                     optionalboolean-attr-content)
                 | (attribute name { "SOURCE_TRANSITION" },
                     optionalboolean-attr-content)
                 | (attribute name { "STATE_MACHINE" },
                     optionalboolean-attr-content)
                 | (attribute name { "STRONGLY_CONNECTED" },
                    optionalboolean-attr-content)
                 | (attribute name { "SUBCONSERVATIVE" },
                     optionalboolean-attr-content)),
                element description { text }?
            }+
        }
    }

Grammar of the Generic precomputed properties in RNC

The order in which attributes occur should be respected, although attribute order is not significant in XML.
The name of a property must take one of the values listed above, from CONNECTED to SUBCONSERVATIVE.

You can download the grammar in List. 4 from this link.

4.2. Definition in RELAX NG XML Syntax

Instead of showing you directly the content of the XML Syntax version of the grammar, we display below its conceptual model (Fig. 1) and provide a link to access and download the corresponding XML file.

Conceptual model of the RNG grammar
of the generic precomputed properties in the Model Checking Contest — Conceptual model of the RNG grammar of the generic properties

4.3. Definition in XSD

Here also, we show you the conceptual model (Fig. 2) of the grammar in XSD and provide a link to access and download the corresponding XML file.

Conceptual model of the XSD grammar of
the generic precomputed properties in the Model Checking Contest — Conceptual model of the XSD grammar of the generic properties

5. Download

All referenced grammars documents (i.e. generic properties, and properties verdicts definitions) are available in a single archive that you can download by following this link.

6. Tooling

You need not spending time integrating the parsing/reading of the file GenericPropertiesDefinition.xml in your tool. It suffices to have a look at it and understand the definitions. The verdicts of these properties are much more important to integrate in your tool. Their definitions are self-contained, and detailed on the following page. However, if you still want to integrate the generic properties definition in your tool, please feel free to proceed.

Lom M. Hillah
Apr. 3, 2018