Add model checking examples ABP, Onebit and BRP.

These were used in van de Pol and Weber's paper on parallel solving of parity games.