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

\title{{\Circus} Model for the Cruise Controller}

\author{Frank Zeyda}

\begin{document}

\maketitle

\tableofcontents

\newpage

\section{Constants and Events}

This section includes definitions of constants and channels for the automotive cruise controller example.

\subsection{Constants}

\input{Constants.circus}

\subsection{Events}

Below we declare a channel for each sensor and actuator event of the cruise controller.
%
\input{Events.circus}

\subsection{Mission Identifiers}

Mission identifiers for the cruise controller application. (We only have one mission.)

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

\subsection{Handler Identifiers}

Handler identifiers for the cruise controller application.

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

\subsection{Event Identifiers}

Event identifiers for the cruise controller application.
%
\begin{circusbox}
\input{EventIds.circus}
\end{circusbox}

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                            Aperiodic Event Handler                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Aperiodic Event Handlers}

In this section we present the framework and application models for aperiodic event handlers of the cruise controller application.

%\subsection{Framework Process}

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

\subsection{Framework Processes}

In this section we illustrates the instantiation of the framework process for the aperiodic event handlers of the cruise controller in order to obtain the models for particular aperiodic handlers.

\subsubsection{WheelShaft}

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

\subsubsection{Engine}

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

\subsubsection{Brake}

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

\subsubsection{Gear}

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

\subsubsection{Lever}

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

\newpage

\subsection{Application Processes}

In this section we illustrate the application model for aperiodic event handlers by defining a process for each aperiodic handler of the cruise controller. They all have very similar shapes.

\subsubsection{WheelShaft}

\newpage

\begin{circusbox}
\input{../../circus/WheelShaftApp.circus}
\end{circusbox}

\newpage

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

\newpage

%\paragraph{Note}

%\red{The channels for methods channels for \code{void handleAsyncEvent()} and \code{void handleAsyncLongEvent(int value)} seem redundant with the most recent revision of the model. Furthermore, I have not encoded the $handlerAsyncLongEvent$ method as an action here but data operations. What policy we adopt here is still subject to discussion. Clearly, however, since there no outputs a data operations is sufficient here.}

\subsubsection*{Interrupt Handler}

\verbatiminput{accs/interrupts/WheelShaftInterruptHandler.java}

\newpage

\subsubsection{Engine}

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

\subsubsection*{Interrupt Handler}

\verbatiminput{accs/interrupts/EngineInterruptHandler.java}

\nid \red{A problem here is that the types do not agree: whereas the channel type is $BOOL$ the value that is passed to the handler is of type $long$. There hence has to be a conversion from channel types to $long$.}

\newpage

\subsubsection{Brake}

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

\subsubsection*{Interrupt Handler}

\verbatiminput{accs/interrupts/BrakeInterruptHandler.java}

\nid \red{Here we again assume an implicit mapping from events to identifiers. To unify this case with the previous one for $Engine$, we could make the event id an implicit input. So although the underlying channels are not parametrised, a parameter is nevertheless passed to the handler.}

\newpage

\subsubsection{Gear}

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

\nid \green{Exactly the same case as $Brake$ --- the handler parameter is implicit.}

\subsubsection*{Interrupt Handler}

\verbatiminput{accs/interrupts/GearInterruptHandler.java}

\newpage

\subsubsection{Lever}

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

\subsubsection*{Interrupt Handler}

\verbatiminput{accs/interrupts/LeverInterruptHandler.java}

\newpage

\subsection{Composite Processes}

\subsubsection{WheelShaft}

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

\subsubsection{Engine}

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

\subsubsection{Brake}

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

\subsubsection{Gear}

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

\subsubsection{Lever}

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

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                            Periodic Event Handler                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Periodic Event Handlers}

In this section we present the framework and application model for periodic event handlers.

%\subsection{Framework Process}

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

\subsection{Framework Processes}

\subsubsection{SpeedMonitor}

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

\subsubsection{ThrottleController}

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

\subsection{Application Processes}

The application processes for handlers basically all have the same shape. They result from a lifting of the underlying data object. The latter is modelled by an {\OhCircus} class.

\subsubsection{SpeedMonitor}

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

\subsubsection{ThrottleController}

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

\newpage

\subsubsection{ThrottleController -- Alternative 1}

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

\newpage

\subsubsection{ThrottleController -- Alternative 2}

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

\newpage

\subsection{Composite Processes}

\subsubsection{SpeedMonitor}

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

\subsubsection{ThrottleController}

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

\newpage

\subsection{Top-level Model}

In this section we specify the top-level model of the entire cruise controller application. It is the composition of the safelet, mission sequencer, mission, as well as all handler components.

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

\newpage

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                 Data Objects                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Data Objects}

In this section we give the {\OhCircus} class definitions for all data objects of the Cruise Controller case study. It also illustrates how the respective Java classes are translated into formal models.

Not all of the specification can be parsed at the moment due to limitations of CZT to understand {\OhCircus}. The parts that are not subjected to the parser are highlighted in dark red.

\subsection{WheelShaft}

\input{WheelShaftClass.circus}

\newpage

\subsection{Engine}

\input{EngineClass.circus}

\newpage

\subsection{Brake}

\input{BrakeClass.circus}

\newpage

\subsection{Gear}

\input{GearClass.circus}

\newpage

\subsection{Lever}

\input{LeverClass.circus}

\newpage

\subsection{SpeedMonitor}

\input{SpeedMonitorClass.circus}

\newpage

\subsection{ThrottleController}

\input{ThrottleControllerClass.circus}

\newpage

\subsection{CruiseControl}

\input{CruiseControlClass.circus}

\nid The methods called by this class are:
%
\begin{itemize}
  \item \code{ThrottleController: void setCruiseSpeed(int speed)}
  \item \code{ThrottleController: void accelerate()}
  \item \code{ThrottleController: void schedulePeriodic()}
  \item \code{ThrottleController: void deschedulePeriodic()}
  \item \code{SpeedMonitor: int getCurrentSpeed()}
\end{itemize}

\end{document}
