tools
HSF-SPIN
HSF-SPIN an experimental model checker which can be seen as a directed model checking extension to Spin. It implements various heuristic estimates and algorithms in order to direct the search into a specific error situation. As consequence might be able to find shorter trails than blind depth-first search while finding errors in larger state spaces.
HSF-SPIN is not maintained but you can download (zip) and install it and ask me for help.
