% 
%
\section{Promela Specification for System}
%
% Give a brief overview of what Promela and model checking
% are. Explain why the encoding into Promela can be useful
% Explain the relationship between the state diagram and
% Promela code, and what you can do with the Promela code.
%
\subsection{Model Checking and Promela Overview}

% - Refer explicitly to the state diagrams that you encoded in Promela
% - Also, refer explicitly to any sequence diagrams that you validated
% through simulation with your Promela model. 
\subsection{Promela Model}

% If you wish to import the specs directly, then you need to put at the
% top of the ASCII file: \begin{verbatim} and at the bottom of the
% file \end{verbatim}.
% Otherwise, it is fine to enscript the file using ``enscript -2r -o
% output.ps project.promela'', which will generate a ps file that
% you may print and insert.  Be sure that the state diagram
% in the document is the one that you used to generate the Promela specs.
% 
%
% To directly import a Promela program in the file ``project.promela''
% insert the verbatim environment around the Promela code:
%\begin{verbatim}
%% Promela file
%\end{verbatim}
%
% Depending on the size of your proctypes, you may wish to present each
% proctype individually and give a small description as you go along. 
% In any case, please be sure that your proctypes are sufficiently commented.
% /* and */ are the comment delimiters. 
%