\documentclass[10pt]{llncs}

\usepackage{llncsdoc}
\usepackage{graphicx}
\usepackage{amssymb,amsmath}
\usepackage{latexsym}
\usepackage{nopageno}

\newcommand{\prism}{\mbox{\textup{P}\scalebox{0.75}{{\textsc{RISM}}}}}
\newcommand{\gap}{\mbox{\textup{G}\scalebox{0.75}{{\textsc{AP}}}}}
\newcommand{\grape}{\mbox{\textup{G}\scalebox{0.75}{{\textsc{RAPE}}}}}
\newcommand{\uppaal}{\mbox{\textup{U}\scalebox{0.75}{{\textsc{PPAAL}}}}}
\newcommand{\spin}{\mbox{\textup{S}\scalebox{0.75}{{\textsc{PIN}}}}}
\newcommand{\topspin}{Top\textup{S}\scalebox{0.75}{{\textsc{PIN}}}}
\newcommand{\spintogrape}{\spin-to-\grape}

\newcommand{\m}{\mathcal{M}}

%\newtheorem{definition}{Definition}
%\newtheorem{theorem}{Theorem}

\title{\protect\topspin\ User Manual}

\author{Alastair F. Donaldson}
\institute{Department of Computing Science\\
  University of Glasgow\\
  Glasgow, Scotland.\\
\tt{\{ally\}@dcs.gla.ac.uk}}

\pagestyle{plain}

\begin{document}

\maketitle

\begin{abstract}
This document is a short user manual for the \topspin\ symmetry
reduction package for the \spin\ model checker.
\end{abstract}

\section{Introduction}
%
\topspin\ \cite{domi2} is an automatic symmetry reduction package
for the \spin\ model checker \cite{ho}.  \topspin\ can potentially
aid in the verification of {\it safety} properties of concurrent
distributed systems modelled in Promela, if the system exhibits
replicated structure.  Safety properties can be specified using
assertions or monitor processes.  The tool does not yet support
$LTL$ model checking with never claims.  This document outlines the
process of downloading, configuring and installing \topspin. For
details of symmetry reduction techniques see a recent survey
\cite{midoca}. We are keen for questions, queries and bug reports --
please use the email address above.
%
\section{Installing \protect\topspin}
%
Section~\ref{sec:installing:prerequisites} provides details of how
to get hold of prerequisite packages which \topspin\ requires.
Downloading of \topspin\ is described in
Section~\ref{sec:installing:download}, while
Section~\ref{sec:installing:configure} explains how to configure
\topspin.
%
\subsection{Prerequisites}\label{sec:installing:prerequisites}
%
\topspin\ is implemented in Java 5, and uses an additional PERL
script, and thus requires a recent Java distribution and a PERL
implementation to run. \spin\ also requires the {\bf gcc} compiler
to be installed.  \topspin\ runs under Linux or Windows.

The automatic symmetry detection component of \topspin\ uses the
{\it saucy} graph automorphism program \cite{dalisama}, and the
\gap\ computational algebra system \cite{gap} is used for symmetry
detection, classification of group structure before search and (if
the {\it segment} strategy is used) representative computation
during search. This section provides details on how to get hold of
these required packages.\ \\

\noindent {\bf Java 5} This can be downloaded free from \texttt{www.java.sun.com}.\ \\

\noindent {\bf PERL} This comes as standard with most Linux
distributions, and can be downloaded from \texttt{www.perl.com}.\ \\

\noindent {\bf gcc}  The GNU C compiler also comes as standard with
Linux, and can be downloaded from \texttt{gcc.gnu.org}.\ \\

\noindent Make sure \texttt{java}, \texttt{perl} and \texttt{gcc}
are on your
path before you try to use \topspin.\ \\

\noindent {\bf \gap} Windows and Linux distributions of \gap\ can be
downloaded from \texttt{www.gap-system.org}, and detailed
installation instructions are available from
this location.\ \\

\noindent {\bf \emph{saucy}} Source code for the graph automorphism
program \cite{dalisama} can be downloaded from
\texttt{vlsicad.eecs.umich.edu/BK/SAUCY}, and is straightforward
to compile using \texttt{gcc}.\ \\

One of the files in the \topspin\ distribution,
\texttt{PreparePan.pl}, is Linux system dependent as it uses various
Linux commands such as \texttt{cp} and \texttt{ls}.  If you have
\texttt{cygwin} installed under Windows (see \texttt{www.cygwin.com}
for details), this is fine.  Otherwise please email the author and a
Windows version of this file will be prepared.
%
\subsection{Downloading
\protect\topspin}\label{sec:installing:download}
%
Go to \texttt{www.dcs.gla.ac.uk/people/personal/ally/topspin} and
download a \texttt{.zip} file containing the most recent \topspin\
distribution.  This archive contains the following:

\begin{itemize}
\item \texttt{TopSPIN.jar} -- the executable \texttt{.jar} file
containing \topspin.
\item \texttt{config} -- a plain text file containing configuration
details, which must be edited as described in
Section~\ref{sec:installing:configure}.
\item \texttt{Documentation} -- a folder containing this document
and some related research papers.
\item \texttt{lib} -- a folder containing \texttt{junit.jar}, the
JUnit test framework used in the \topspin\ implementation (see
texttt{www.junit.org}).
\item \texttt{TempFiles} -- an empty folder which \topspin\ will
use for temporary storage.
\item \texttt{Common} -- a folder containing various \gap\ and C
source code files used by \topspin.
\end{itemize}

Extract this archive using something like WinZip
(\texttt{www.winzip.com}) to an appropriate location (e.g.
\texttt{C:/Program Files/TopSPIN/}). We refer to this location below
as \texttt{topspinfolder}.
%
\subsection{Configuring
\protect\topspin}\label{sec:installing:configure}

{\bf Creating a \gap\ workspace}  So that \gap\ can be started by
\topspin\ in a state where the \gap\ code in the
\texttt{topspinfolder/Common} directory is already loaded, you must
create a {\it workspace}.  Navigate to the \texttt{Common}
directory, start \gap\ and type:
\begin{verbatim}
Read("WorkspaceGenerator.gap");

SaveWorkspace("gapworkspace");

quit;
\end{verbatim}
%
The middle command should output \texttt{true}.\ \\

\noindent {\bf Editing the \texttt{config} file} A text file called
\texttt{config} is provided with the distribution.  Edit this file
so that \texttt{gap} and \texttt{saucy} refer to the absolute
locations of your \gap\ and {\it saucy} executables, and
\texttt{tempfiles} and \texttt{common} refer to the folders
\texttt{TempFiles} and \texttt{Common} within the \topspin\
distribution.

{\it To run \topspin\ you need to copy \texttt{config} to your
current directory}.  This is easy to forget!
%
\section{Running \protect\topspin}
%
To run \topspin, navigate to the folder in which you would like your
executable verifier to be generated (as you would when using \spin\
as standard).  Copy the \texttt{config} file to this directory. Then
type
\begin{verbatim}
java -jar topspinfolder/TopSPIN.jar detect_opt reduce_opt model
\end{verbatim}
Here \texttt{model} is the name of the Promela specification you
wish to check, \texttt{detect\_opt} is a symmetry detection option
(see Section~\ref{sec:running:detection}), and
$\texttt{reduce\_opt}$ is a symmetry reduction option (see
Section~\ref{sec:running:reduction}). If neither option is
specified, the Promela file is just type-checked. If only a symmetry
detection option is given, the detected symmetries are displayed but
no verifier is generated.

If both symmetry reduction options are specified then an executable
verifier, \texttt{sympan.c}, is generated.  This can be compiled and
executed using the same method that would be used with the
\texttt{pan.c} file generated by \spin, except that the file
\texttt{group.o} must appear in the compilation command.  For
example, one could compile \texttt{sympan.c} as follows:
%
\begin{verbatim}
gcc -w -o sympan -D_POSIX_SOURCE -MEMLIM=256 -DSAFETY -DNOCLAIM
-DNOFAIR sympan.c group.o
\end{verbatim}
%
\subsection{Symmetry Detection Options}\label{sec:running:detection}
%
\topspin\ provides two techniques for automatic symmetry detection
-- {\it static channel diagram} or {\it identifier adjacency
diagram} analysis.  Additionally, \topspin\ allows generators for a
symmetry group to be specified manually.  The following options
specify which symmetry detection method should be used, and should
be given as the first parameter to \topspin:\ \\

\noindent{\bf -scd} With this option, symmetry detection is via
static channel diagram analysis.  Details of this technique in
general can be found in \cite{domica}, with \spin-specific details
in \cite{domi}. Static channel diagram analysis works well when
fixed communication links
are passed to processes as parameters on instantiation.\ \\

\noindent{\bf -iad} {\it Identifier adjacency diagrams} are a
(currently unpublished) alternative to static channel diagrams, and
are suitable for symmetry detection when the communication structure
of a model is encoded in the Promela specification via a lookup
macro. For example.......   Occurrences of literal {\it pid} values
or channel names are used to build a directed graph, from which
model automorphisms are derived using the computational group
theoretic
approach of \cite{domi}.\ \\

\noindent{\bf -manual $<$filename$>$}

\noindent If a specification is know to exhibit component symmetry,
but this symmetry is not detected using the above approaches, it is
possible to manually specify generators for a symmetry group.  The
file specified by {\bf $<$filename$>$} should contain one line per
generator, and each generator should be a product of permutations of
global channel names and literal {\it pid} values.
%
\subsection{Symmetry Reduction Options}\label{sec:running:reduction}

\noindent{\bf -enumerate} The {\it enumerate} symmetry reduction
option computes orbit representatives by exhaustively enumerating
images of a state under a group $G$.  Thus the time complexity of
computing a representative is proportional to $|G|$, which may be as
large as $|n!|$ where $n$ is the number of system components.
Enumeration is memory optimal and is suitable when $G$ is small, or
for purposes of
comparison with other strategies.\ \\

\noindent{\bf -fast} With the {\it fast} option, a symmetry
reduction strategy will be chosen for the group $G$ based on its
structure, as described in \cite{domi3}.  If $G$ is small, the {\it
enumerate} option may be used.  If $G$ is unclassifiable, the
approximate {\it hillclimbing} option (below) will be used.
Otherwise a strategy based on minimising sets for $G$ will be
applied, resulting in fast representative computation.  Memory
optimality is not guaranteed if components in the specification hold
references to one another, but in practice a close-to-optimal factor
of reduction is usually
achieved.\ \\

\noindent{\bf -hillclimbing}  This option means that representatives
will be computed using an approximate strategy described in
\cite{domi3}
based on hillclimbing local search.\ \\

\noindent{\bf -segment}  This is an experimental option described in
\cite{domi4} which combines features of the {\it fast} and {\it
enumerate} options to provide memory optimal verification using an
approach which, for groups with identifiable structure, is less
na\"ive than pure enumeration.  To use this option, you must copy
your executable \texttt{sympan} file into
\texttt{topspinfolder/Common}, navigate there, launch \gap, and type
%
\begin{verbatim}
Read("Verify.gap");

Verify("sympan",[]);
\end{verbatim}
%
Currently it is not possible to pass command line arguments to
\texttt{sympan} this way, so you must make modifications directly to
\texttt{sympan.c} before compiling it.  The most common command line
argument is one to change the maximum search depth.  To do this via
\texttt{sympan.c}, open the file and find the line where the
variable \texttt{maxdepth} is initialised (to 10000 by default).
Change the initial value to a more appropriate one.
%
\section{Troubleshooting}
%
This section will be expanded to include a list of common problems
with the use of \topspin.  In the mean time, please email the author
with any queries.
%
\begin{thebibliography}{1}

\bibitem{dalisama}
P.~T. Darga, M.~H. Liffiton, K.~A. Sakallah, and I.~L. Markov.
\newblock Exploiting structure in symmetry detection for {CNF}.
\newblock In {\em DAC'04}, pages 530--534. {ACM} Press, 2004.

\bibitem{domi}
A.F. Donaldson and A.~Miller.
\newblock Automatic symmetry detection for model checking using computational
  group theory.
\newblock In {\em FM'05}, LNCS 3582, pages 418--496.  Springer, 2005.

\bibitem{domi2}
A.F. Donaldson and A.~Miller.
\newblock A computational group theoretic symmetry reduction package for the \spin\ model checker.
\newblock In {\em AMAST'06}, LNCS 4019, pages 374--380.  Springer, 2006.

\bibitem{domi3}
A.F. Donaldson and A.~Miller.
\newblock Exact and approximate strategies for symmetry reduction in model checking.
\newblock In {\em FM'06}, to appear in LNCS.  Springer, 2006.

\bibitem{domi4}
A.F. Donaldson and A.~Miller.
\newblock Extending symmetry reduction techniques to a realistic model of computation.
\newblock Submitted for publication, June 2006.

\bibitem{domica}
A.F.~Donaldson, A.~Miller, and M.~Calder.
\newblock Finding symmetry in models of concurrent systems by static channel
  diagram analysis.
\newblock In {\em AVoCS'04}, ENTCS 128(6), pages 161--177. {E}lsevier {S}cience {P}ublishers {B.V}, 2005.

\bibitem{gap}
The~Gap~Group.
\newblock {\em GAP--Groups Algorithms and Programming, Version 4.2}.
\newblock Aachen, St. Andrews, 1999.
\newblock http://www-gap.dcs.st-and.ac.uk/\~{}gap.

\bibitem{ho}
G.~J. Holzmann.
\newblock {\em The {SPIN} model checker: primer and reference manual}.
\newblock Addison Wesley, 2003.

\bibitem{midoca}
A. Miller, A. Donaldson and M.~Calder.
\newblock Symmetry in temporal logic model checking.
\newblock {\em Computing Surveys}, To appear, 2006.



\end{thebibliography}
\end{document}
