Direct Witness Export
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
: