When a limit of states is supplied and so many states are explored during the model checking process, the run should terminate gracefully.