Adjustments for modular CEGAR
This MR contains configurations and different adjustments for modular CEGAR, a decomposition of counterexample-guided abstraction refinement in three stateless, independent components "abstract-model explorer", "feasibility checker" and "precision refiner". As exchange formats, CPAchecker's predmap.txt and the GraphML witness formats can be used.
On example for the classic predicate abstraction with predicate refinement through CEGAR, with predmap.txt to exchange predicates and violation witness graphml for counterexamples:
graph TD
pred[Predicate Analysis] -- violation witness<br /> --> check
check[CEX check] -- violation witness --> refiner
refiner[refiner] -- predmap.txt --> joiner
joiner{Joiner} -- joined predmap.txt --> pred
joiner -- joined predmap.txt --> joiner
I'll add open to-dos in a minute.
Edited by Thomas Lemberger