\documentclass{article}
\usepackage{fullpage}
\usepackage{wasysym}
\usepackage{verbatim}
\usepackage{sverb}
\usepackage[usenames,dvipsnames]{color}
\usepackage[colour]{circus}
\usepackage{hijac}

\title{A Simple Protocol\\Safety-Critical Java Program and its {\Circus} Model}

\author{Ana Cavalcanti, Andy Wellings, and Frank Zeyda}

\begin{document}

\maketitle

\tableofcontents

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{External Events}

\begin{circusbox}
\input{Events.circus}
\end{circusbox}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Framework Model}

\subsection{Safelet Framework Process}

\begin{circusbox}
\input{SafeletFW.circus}
\end{circusbox}

\subsection{Mission Sequencer Framework Process}

\begin{circusbox}
\input{MissionSequencerFW.circus}
\end{circusbox}

\subsection{Mission Framework Process}

\begin{circusbox}
\input{MissionFW.circus}
\end{circusbox}

\subsection{Event Handler Framework Process}

\begin{circusbox}
\input{EventHandlerFW.circus}
\end{circusbox}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{MainSafelet}

\subsection{Application Process}

\begin{circusbox}
\input{MainSafeletApp.circus}
\end{circusbox}

\subsection{Composite Process}

\begin{circusbox}
\input{MainSafelet.circus}
\end{circusbox}

\subsection{Java Code}

\verbinput{jtres/MainSafelet.java}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{MainMissionSequencer}

\subsection{Application Process}

\begin{circusbox}
\input{MainMissionSequencerApp.circus}
\end{circusbox}

\subsection{Composite Process}

\begin{circusbox}
\input{MainMissionSequencer.circus}
\end{circusbox}

\newpage

\subsection{Java Code}

\verbinput{jtres/MainMissionSequencer.java}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{MainMission}

\subsection{Application Process}

\begin{circusbox}
\input{MainMissionApp.circus}
\end{circusbox}

\subsection{Composite Process}

\begin{circusbox}
\input{MainMission.circus}
\end{circusbox}

\newpage

\subsection{Java Code}

\verbinput{jtres/MainMission.java}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Handler1}

\subsection{Framework Process}

\begin{circusbox}
\input{Handler1FW.circus}
\end{circusbox}

\subsection{Application Process}

\begin{circusbox}
\input{Handler1App.circus}
\end{circusbox}

\subsection{Composite Process}

\begin{circusbox}
\input{Handler1.circus}
\end{circusbox}

\subsection{Data Object}

\begin{circusbox}
\input{Handler1Class.circus}
\end{circusbox}

\subsection{Java Code}

\verbinput{jtres/Handler1.java}

%\noindent
%\begin{alert}
%The correspondence between the $\circenter area \circspot A$ construct and the code above is still informal and an open issue. An alternative design may, for instance, store the $value$ variable accessed inside the body of the construct in an instance variable of the class. Then we would not have to pass it explicitly to the constructor of $MissionMemoryEntry$ as instance variables of the outer class can be directly accessed.
%\end{alert}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Handler2}

\subsection{Framework Process}

\begin{circusbox}
\input{Handler2FW.circus}
\end{circusbox}

\subsection{Application Process}

\begin{circusbox}
\input{Handler2App.circus}
\end{circusbox}

\subsection{Composite Process}

\begin{circusbox}
\input{Handler2.circus}
\end{circusbox}

\subsection{Data Object}

\begin{circusbox}
\input{Handler2Class.circus}
\end{circusbox}

\newpage

\subsection{Java Code}

\verbinput{jtres/Handler2.java}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{List}

In this section I provide a model for the implementation of the List class in the abstract model. We would expect that it data-refines the $List$ class specified in the paper. Note that none if it can be type-checked at the moment with the CZT {\Circus} tools.

\subsection{Data Object}

%\begin{circusbox}
\input{List.circus}
%\end{circusbox}

\newpage

\subsection{Java Code}

\verbinput{jtres/List.java}

\begin{comment}
\noindent
\begin{alert}
There have been a few changes to the $List$ class when working towards a `final' implementation.
\begin{enumerate}
  \item There was a bug in the \code{insert(int value)} method which did not set \code{node.next.empty} to \code{true} when the next element had already been allocated.

  \item The previous \code{void insert(int value)} did not do the full job of clearing the list when it reaches 50 elements, and only inserting the value if it is not already contained in the list. I thus renamed \code{void insert(int value)} into \code{void append(int value)} and let the new \code{void insert(int value)} method do the entire job.

  \item A private synchronized method \code{boolean contains(int value)} has been added to facilitate implementation of \code{insert(int value)}.

  \item Setting \code{next} to \code{null} in the constructor. Strictly, this may not be necessary though.
\end{enumerate}
\end{alert}
\end{comment}

\begin{comment}
\begin{note}
  Andy Wellings now seems to fully agrees with the code now. \smiley
\end{note}
\end{comment}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{System}

\begin{circusbox}
\input{System.circus}
\end{circusbox}

\end{document}
