Skip to content

Direct Witness Export

Marian Lingsch requested to merge direct-witness-export into trunk

Currently these are the ways in which CPAchecker interacts with YAML witnesses, in bold currently recommended methods. This Branch tries to unify and improve them such that there exist well defined ways to interact with them, without having them be read from GraphML witnesses. Some of these are already in trunk, but there they should be considered a prototype, since their performance has not yet been well-tested.

  • Export: GraphML to YAML correctness: In class WitnessToYamlWitnessConverter
  • Export: GraphML to YAML violation: In class InvariantWitnessWriter
  • Export: Counterexample to YAML violation: In class CounterexampleToWitness
  • Export: ARG to YAML correctness V2: In class ARGToWitnessV2
  • Export: ARG to YAML correctness V3 (WIP): In class ARGToWitnessV3
  • Validation: YAML to Automaton correctness (Used by MetaVal): In class AutomatonWitnessV2ParserCorrectness
  • Validation: YAML to Injection of Invariants in K-Induction: In class WitnessInvariantsExtractor
  • Validation: YAML to Automaton violation: In class AutomatonWitnessV2ParserWithOffsets
  • Validation: YAML to Automaton violation: In class AutomatonWitnessV2ParserViolation

Currently the performance of YAML witnesses, for this branch, is comparable to that of GraphML witnesses, the goal of this merge request is to also prepare them to be a drop-in replacement for GraphML witnesses.

In particular this merge request also contains WIP for support of the witness version V3, which extends V2 witnesses by function contracts. For this there is currently ongoing work in order to export them and validate them, for example using Ultimate Referee. Currently witness version V3 has not yet been officially proposed to the whole SV-COMP community.

This merge request also addresses the following issues related to the ASTStructure:

Edited by Marian Lingsch

Merge request reports