Model checking learning agent systems using Promela with embedded C code and abstraction