Switching from Spec Explorer, I found ModelJUnit a very good MBT tool for Java users. Advantages: simple, easy to use, fast-but-efficient exploration algorithms. Disadvantages: no test data generation and data coverage report, no depth-first-search exploration. In general, this is a very good MBT tool among the ones I tried. Will post some improvement requests/bug report in the Bug Tracker.