\contentsline {section}{\numberline {1}Introduction}{2}
\contentsline {section}{\numberline {2}Installation}{2}
\contentsline {section}{\numberline {3}Running HSF-SPIN}{3}
\contentsline {subsection}{\numberline {3.1}A first example}{3}
\contentsline {subsection}{\numberline {3.2}Compile-Time Options}{4}
\contentsline {subsection}{\numberline {3.3}Run-Time Options}{5}
\contentsline {paragraph}{Error to be checked}{6}
\contentsline {paragraph}{Search Algorithm}{6}
\contentsline {paragraph}{Heuristic Estimate}{7}
\contentsline {paragraph}{User defined dangers for deadlock detection}{7}
\contentsline {paragraph}{Weighting in A*}{7}
\contentsline {paragraph}{Depth bound}{7}
\contentsline {paragraph}{Maximum Heuristic Value}{7}
\contentsline {paragraph}{Number of Supertraces}{8}
\contentsline {paragraph}{Size of Hash Table}{8}
\contentsline {paragraph}{Size of Cache for IDA*}{8}
\contentsline {paragraph}{Size of Bitstate Hash Table}{8}
\contentsline {paragraph}{Writing the Error Trail}{8}
\contentsline {section}{\numberline {4}HSF-SPIN's Output Format}{8}
\contentsline {subsection}{\numberline {4.1}Improved NDFS in Spin}{8}
\contentsline {subsection}{\numberline {4.2}Analyzing Strongly Connected Components}{9}
\contentsline {section}{\numberline {5}Practical use of HSF-SPIN}{9}
\contentsline {section}{\numberline {6}Examples}{9}
\contentsline {paragraph}{Getting a shorter trail}{9}
\contentsline {paragraph}{Improved Nested Depth-First Search}{11}
\contentsline {section}{\numberline {7}Contact}{12}
