Violation-Witness Validation Config doesn't use Witness-Validation Configs
This is more of a question that may turn into an issue:
We have a config includes/witness-validation.properties
that sets some options that are necessary for witness validation.
An excerpt from that file:
cpa.automaton.treatErrorsAsTargets = false
WitnessAutomaton.cpa.automaton.treatErrorsAsTargets = true
analysis.traversal.byAutomatonVariable = __DISTANCE_TO_VIOLATION
These options seem to me like they make a lot of sense, and I actually had to use the first two to make a custom violation-witness-config work with witnessValidation.properties
.
Now comes the part I find fishy: Our default violation-witness-validation.properties
config does not use these options,
and neither does components/violationWitnessValidation.properties
that is used in the restart algorithm of the first.
Instead, the latter config sets specification =
to the empty value. I assume this is equal to cpa.automaton.treatErrorsAsTargets = false
?
Now my question: Why don't we include includes/witness-validation.properties
, which seems to be the generic way to define configs for witness validation? Should I be aware of anything when using this config myself, or was this just an oversight/pragmatism of some sort?