I am suggesting that a feature be added to the Analyzer so that as the command "Execute" is being... executed, the user is updated on the progress of the solver. This could be done with a simple progress bar, or even printouts to the output area every x number of states. This would be nice because it's often impossible to tell how long the solver will take; thus it's impossible to know whether it's worth waiting for or whether it would be better to just scrap the execution, reduce the scope, and start again.

I know from my experience with progress bars that come with operating systems that progress bars are not always very accurate time estimators, and are often way off the mark. However, from a psychological point of view, any indication of progress, albeit inaccurate, is welcomed as it makes the wait seem shorter. It puts thoughts like "The program is frozen" and "This will take forever" out of our heads and replaces them with ones like "The program is running very slowly" and "this will take a few minutes, I'll get a cup of tea and come back to it".