L09 (10.10): Model checking examples