ftsrg
Generalization of CegarChecker and related classes
Currently, the CegarChecker class, the SafetyResult class, and indirectly the SafetyChecker interface depend on the ARG and Trace classes. Only ARG can be used as abstraction, and only a Trace on an ARG can be used as a counterexample.
The CEGAR loop implementation in CegarChecker could be generalized by introducing two new generic type parameters: an Abstraction and a Counterexample (or Witness). Related interfaces, like the Abstractor and Refiner interfaces, would also get these new type parameters, so that the compatibility of the Abstractor and Refiner used when creating a CegarChecker can be enforced.
The SafetyResult class would also have to be generalized this way.
This would lead to better reusability of implemented algorithms and easier integration of model checking strategies that maintain something other than a single ARG throughout the CEGAR loop. Some examples that could build on this:
- Probabilistic extensions to Theta are currently under development. Probabilistic CEGAR algorithms use the same high-level loop, but with totally different abstractions (MDPs or Stochastic Games depending on the chosen approach)
- The hierarchical A* search strategy works with a list of ARGs instead of a single ARG
- Integrating decision diagram-based approaches into Theta might also be easier to implement by replacing ARG with another abstraction implementation class, and creating Abstractors and Refiners that can work with this class
Although it would be possible to create new, separate generalized versions of the classes only for the probabilistic part (so that no changes would be needed to the already written code), the other features need to be integrated with the formalism-specific parts anyway, and this can make the integration easier.
A possible implementation for this can be found on the argless branch of my fork.
