Interpretation of the GenericPropertiesVerdict.xml values

Dear MCC organizers,
   I was wondering whether the values stored in the GenericPropertiesVerdict.xml file should
be considered trustable, i.e. when a model is declared SAFE or LIVE, it is surely this way,
or if instead this is only an hint. There is no mention of the trustability of these values in the
Tool Submission Manual.

   This is an important issue, since:
- if I remember correctly, a few years ago some of these values were incorrect for some models;
- if a tool "trusts" these values, it could use some feature that would not work correctly if the
 property was wrongly declared;
- what happens if a MCC model declares a wrong property value, making a tool mis-compute a result?

Also, the property list contains a DEADLOCK property. What is the purpose of having a ReachabilityDeadlock
examination when the response value is already stored in the xml file? Should we just return this value
instead of doing any computation?

Regards
--Elvio

Dear Elvio,

These values should be trusted as much as those exposed in the model forms. They are extracted from there. Values of such properties in the model forms are provided by the submitter. They are quickly checked by the model board but not to such a full extent (checking time is limited to 1 mn) to guarantee 100% correctness. Large instances of many models typically have not been fully checked (and it is often reported as footnotes in the model forms).

For instance, Bernard reported the case of RwMutex where all previous editions of the MCC showed that all its instances are safe, but the model form was still displaying 'unknown' for that property. In such cases only we update the model form, and subsequently the GenericPropertiesVerdict.xml. The values stated in that file (and the model form where they come from) are therefore not even strictly instance-based. This is a first imperfect attempt to make that information readable for tools, as a hint from the model form. More work is needed in the future to exploit the actual results of the MCC to (perfectly) relate those properties values to the actual instances the values correspond to (true, false, unknown according to data drawn from the examination results).

About the deadlock property, it is listed in a model form and therefore extracted as the others into the GenericPropertiesVerdict file. So, w.r.t. what I said earlier, you should not take it as 100% correct across all instances of the model.

Kind regards,
Lom

Sorry Lom,
but I don't fully understand your response. Are non-trivial properties (like SAFE) just declared by the model submitters, or are they checked by some/multiple tools? From the descriptions in the xml, it appears that some values are "confirmed" by tools. Is this a manual process?
For new (surprise) models, the value that will appear has been tested (even with 1min time bound), or is just what the model submitter sent?
In that case, wouldn't it be better if the value is simply "unknown" if it is not confirmed yet by any tool?
Otherwise, I think that the usefulness of these values is very limited, if there is no strict guarantee on their correctness.

Regards
--Elvio