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 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:
Each property's definition resides in a property child element to the properties element.
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)
- 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.
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.
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