Integration of an AEFD runtime with the OBP2 debug and model-checking infrastructure.