L09 (10.14.): Model checking examples