Completing model-check automation script with result extraction.