Is Statestep a model checker?
If you use Statestep to model a finite state machine then you will find that it automatically performs the most useful function of a model checker, that is, to check that no undesirable state can be reached. Unlike an ordinary model checker, Statestep can interactively check this reachability property (and other properties) even while the model is still being created, without reporting spurious errors. Another advantage is that it can explain its reasoning so you can see how the problem arises. On the other hand, a model checker will allow you to describe (in temporal logic) more general properties to check, for example, is it possible to get from state X to state Y without going through state Z? Thus, while there is some overlap in functionality, Statestep is not a model checker as the term is ordinarily understood.
