sosy-lab/sv-witnesses

Linter rejects witness with tool-specific edge data element

hernanponcedeleon opened this issue · 1 comments

hernanponcedeleon commented

The attached violation witness has specific edge data elements that can be used by the Dartagnan-based validator to reduce the search space.

witness.graphml.zip

This is allowed by the standard as stated in the following sentence:

"Tools may introduce their own data nodes with custom keys and values. Other tools should ignore data nodes they do not know or are unable to handle."

However the linter rejects the witness with the following output

WARNING : line 60: Unknown key for edge data element: event-id
WARNING : line 62: Unknown key for edge data element: stored-value
WARNING : line 67: Unknown key for edge data element: event-id
WARNING : line 69: Unknown key for edge data element: stored-value
WARNING : line 74: Unknown key for edge data element: event-id
WARNING : line 76: Unknown key for edge data element: stored-value
WARNING : line 80: Unknown key for edge data element: event-id
WARNING : line 82: Unknown key for edge data element: stored-value
WARNING : line 86: Unknown key for edge data element: event-id
WARNING : line 88: Unknown key for edge data element: stored-value
WARNING : line 92: Unknown key for edge data element: event-id
WARNING : line 93: Unknown key for edge data element: loaded-value

witnesslint finished with exit code 1
SvenUmbricht commented

The linter does allow for tool-specific data elements, the problem is that you provided the wrong scope in the key declarations, e.g. the witness declares stored-value as a graph data element via
<key attr.name="stored-value" attr.type="string" for="graph" id="stored-value"/> but is using stored-value as an edge data element, so the above line should be <key attr.name="stored-value" attr.type="string" for="edge" id="stored-value"/>
instead. Same for event-id and probably the other Dartagnan-specific keys as well.

  • 👍1