Basic model checking algorithm is working.