1. Motivation

The proposed models in the MCC come with some known (or unknown) structural and behavioral properties. These properties and their verdicts are the ones you read in the model forms (PDF files). Each verdict is provided either by the model submitter (i.e. true, false, or unknown), or the MCC if possible. We will refer to these verdicts as generic precomputed properties verdicts (or generic properties).

In 2017, feedback from developers of the competing tools in the MCC revealed that it would be highly desirable to represent those properties and their verdicts 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.

PNML provides the toolspecific concept to make room for ad hoc additional information the standard has not defined beforehand. We use this concept to encode the generic properties definitions and their verdicts in XML. However, this encoding is 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), encoded in a specific XML format and answered in one-line text outputs. Then post-processing these outputs yields 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 verdicts format for generic precomputed properties. It provides an example of the verdicts encoded in an XML file for one of the models in the MCC.

The generic properties definition dedicated manual explains the definition of the generic precomputed properties.

2. Format of Generic Precomputed Properties Verdict

An instance of the verdicts 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, propertiesverdict and 1.0, respectively. Every time the grammar of the verdicts definition will be updated, we will increment the version number.

Then, a mandatory, single modelreference element, child element of the root toolspecific, must indicate the name of the referenced model (see List. 2). It is the model whose properties verdicts are produced in the file (in the example below, AirplaneLD is an actual model in the MCC).

Each verdict's definition resides in a verdict child element to the toolspecific element. The example below (List. 3) shows the verdict of the GENERIC property named SAFE, whose value is unknown for AirplaneLD. The attributes category, reference, and value are mandatory. The optional explanation was extracted from the model (LaTeX) form. For each verdict, the optional tool identification element statedby indicates which tool has produced the verdict, and when. The tool and version attributes are mandatory. The date and reference (any URL you deem useful in this context, could be the tool's homepage) are optional.

stated by CAESARBDD version 2.6 to be true on 8 instance(s) out of 9, and unknown on the remaining 1 instance(s)

The verdicts definitions grammar specifies allowed values for the category attribute (see section 4 below). The grammar also specifies allowed values for the reference attribute. Consequently, the grammar will be updated each time those sets are updated.

There is actually more information for verdicts that you can include. The example above (List. 3) is typically what you should expect for the verdicts extracted from the submitted models forms in the MCC. The example below (List. 4) displays possible additional information a verdict can carry.

any explanation the tool could provide


SEQUENTIAL_PROCESSING
SAT_SMT

In the example above (List. 4), the verdict consists of:

• a mandatory category attribute specifying the considered category of property. It is either GENERIC (properties found in a model form), or one of the categories listed in the MCC tool submission manual, i.e., StateSpace, UpperBounds, ReachabilityDeadlock, etc., or another category of property that was not predefined;
• a mandatory reference attribute specifying the generic property name (e.g., LIVE, SAFE, etc.), or formula that was examined. In the case of a formula from the MCC, the formula ID (from the formula XML file) must be used as value for this attribute. If the category is StateSpace, then the value of this attribute must be one of {STATE_SPACE STATES, STATE_SPACE TRANSITIONS, DEADLOCK, ...}, as specified in the MCC tool submission manual. Otherwise, it could just be any text providing information about the type of property;
• a mandatory value attribute stating the computed value for the property or formula that was examined. It is either one of {true, false, unknown} for the generic properties, of free text (including the values from the previous 3-valued set) for any other category of property;
• optional child elements, modelinstance, each referencing the model instance for which the computed value of the property (or formula) holds;
• an optional child element, explanation, containing any useful explanation that the tool could provide as free text;
• in the optional tool identification statedby element (presented earlier, see List. 3), one or more techniques used by the verdict-producing tool may be listed. These techniques are referenced in the MCC tool submission manual. Furthermore, tools may use the trace element to produce any well-formed XML content that could be interpreted as evidence (e.g. counterexample) supporting the verdict. The actual content is not predefined, leaving this definition for the future.

3. MCC version of Properties Verdicts

Each model in the MCC has a single properties verdict file, named GenericPropertiesVerdict.xml. You will find it in the Tool Submission Kit, in the mccYEAR-input.vmdk disk image. YEAR is the MCC year, starting from 2018. Each model instance directory contains all the artefacts related to that model. We provide here for your perusal, the properties verdict file for AirplaneLD.

4. Grammar for Properties Verdicts

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

4.1. Definition in RELAX NG Compact Syntax (RNC)

documentation [
    "Tool-specific fragement element definition for specifying the verdicts to named generic\x{a}"~
    "(structural and behavioral) properties in the MCC.\x{a}" ~
    "This definition also aims to be compatible with indicating, in the future,\x{a}"~
    "verdicts for properties whose formulas have another specific XML syntax (cf. MCC formulas manual).\x{a}" ~
    "This definition enables instances where reference to properties, their names, their actual computed values,\x{a}" ~
    "and the model (possibly instances) to which they apply, are specified.\x{a}"~
    "Version 2.0 adds the new property DEAD_PLACES, and replaces QUASI_LIVE with DEAD_TRANSITIONS.\x{a}" ~
    "It also adds new categories for MCC formulas: QuasiLiveness, StableMarking, Liveness, and OneSafe.\x{a}" ~
    "Finally, version 2.0 adds IMPLICIT to the list of techniques.\x{a}" ~
    "Author: The Model Checking Contest Model Board\x{a}" ~
    "Version: 2.0\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 ".

start = toolspecific.element

toolspecific.element = element toolspecific {
    attribute tool { "propertiesverdict" },
    attribute version { "2.0" },
    modelreference.element,
    verdict.element+
}

modelreference.element = element modelreference {
    attribute modelname {text}
}

verdict.element = element verdict {
    verdictvalue.attr.content,
    modelinstance.element*,
    explanation.element?,
    toolidentification.element?,
    techniques.element?,
    trace.element?
}

verdictvalue.attr.content = 
    ## Either the property whose value you are reporting is a generic one within 
    ## a constrained set, or it is one of the other categories of the MCC, or free text.
    ## In the latter case, we strongly advised whenever possible to use the
    ## conventions of the MCC (e.g., UpperBounds as value for the category attribute, the 
    ## property id (from the property XML file) or predefined values as STATE_SPACE STATES
    ## as value for the reference attribute, and the actual value (int or bool) for the 
    ## value attribute.
    genericproperty-verdictvalue.attr.content
   | mccformula-verdictvalue.attr.content
   | otherproperty-verdictvalue.attr.content

 genericproperty-verdictvalue.attr.content = 
    attribute category { "GENERIC" },
    attribute reference {
        "CONNECTED" | "CONSERVATIVE" | "DEAD_PLACES" | "DEAD_TRANSITIONS" 
        | "DEADLOCK" | "EXTENDED_FREE_CHOICE" | "LIVE" | "LOOP_FREE" 
        | "MARKED_GRAPH"  | "NESTED_UNITS" | "ORDINARY" | "REVERSIBLE" 
        | "SAFE" | "SIMPLE_FREE_CHOICE" | "SINK_PLACE" | "SINK_TRANSITION" 
        | "SOURCE_PLACE" | "STATE_MACHINE" | "STRONGLY_CONNECTED" | "SUBCONSERVATIVE"
    },
    attribute value { 
       ## The syntax (0, 1) is excluded for booleans.
       ## Your application should stick with 'true' or 'false',
       ## in addition to the third value 'unknown'.
       (xsd:boolean - ("0"|"1")) |  "unknown" 
    }

 mccformula-verdictvalue.attr.content = 
    attribute category { "StateSpace" | "UpperBounds"
    | "ReachabilityDeadlock" | "QuasiLiveness" | "StableMarking" | "Liveness" | "OneSafe"
    | "ReachabilityFireability" | "ReachabilityCardinality"
    | "LTLFireability" | "LTLCardinality" | "CTLFireability" | "CTLCardinality"
    },
    attribute reference {
        "STATE_SPACE STATES" | "STATE_SPACE TRANSITIONS" 
        | "STATE SPACE MAX_TOKEN_PER_MARKING" | "STATE_SPACE MAX_TOKEN_IN_PLACE"
        | text
    },
    attribute value { text }

 otherproperty-verdictvalue.attr.content = 
    attribute category { text },
    attribute reference { text },
    attribute value { text }

 modelinstance.element = element modelinstance {
    attribute reference { text }
 }
 
 explanation.element = element explanation { text }
 
 toolidentification.element  = element statedby {
    attribute tool { text},
    attribute version { text },
    attribute date {
       ## Preferred value of date attribute must be 
       ## time-zoned dateTime values, in UTC or with offset. 
       ## Example: 2018-01-01T10:00:05
       xsd:dateTime { pattern = ".+T.+(Z|[+-\\].+)"}
     }?,
     attribute reference { xsd:anyURI {pattern = "http[s]?://.*"}}?
 }
 
 techniques.element = element techniques {
    technique.element+
 }
 
 technique.element = element technique {
    "SEQUENTIAL_PROCESSING" | "PARALLEL_PROCESSING" | "COLLATERAL_PROCESSING"
    | "ABSTRACTIONS" | "DECISION_DIAGRAMS" | "EXPLICIT" | "IMPLICIT" | "NET_UNFOLDING"
    | "UNFOLDING_TO_PT" | "STRUCTURAL_REDUCTION" | "SAT_SMT" | "STATE_COMPRESSION"
    | "STUBBORN_SETS" | "SYMMETRIES" | "TOPOLOGICAL" | "USE_NUPN" 
 }
 
 trace.element = element trace { 
    ## Any well-formed XML. More specific definition left for the future.
    anyElement.content 
}
 
 anyElement.content = 
   element * {
    (attribute * {text}
    | text
    | anyElement.content) *
 }

The order in which attributes occur should be respected, although attribute order is not significant in XML.

You can download the grammar in List. 5 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 display the conceptual model (Fig. 2) of the generic properties definition XSD grammar 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

In contrast with the GenericPropertiesDefinition.xml content described in the generic properties definition manual, it might be worth investing some time to integrate properties verdicts parsing/reading in your tool. We hope that in a not so distant future, it will be possible to produce and exchange verdicts, and possibly their corresponding traces among tools.

Lom M. Hillah
Jul. 8, 2020