Rework: implement "max-states"

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