\subsubsection{A simple mouse controller}

The task is to program a clock-controller for a mouse
\cite{esterel-2}. The program may assume that it is controlled by
the environment using {\tt start} and {\tt stop} signals. The
task of the program is to count the number of mouse-clicks that
occur during each such interval, and output {\tt none}, {\tt
single} or {\tt many} depending on whether there are zero, one or
more clicks.  

Our solution is similar to the one in \cite{esterel-2}. A process
({\tt mouse\_zero(X)}) is set up whose task is to accumulate in
{\tt X} the number of clicks that occur. (The process ceases
looking at the {\tt click} signal once the count reaches two;
instead it maintains forever the count two.)  The process is
aborted by the {\tt stop} signal, which also triggers off a
process which generates the appropriate output signal based on
the accumulated count.

The program illustrates two common idioms in \tgentzen{}
programming. First, note the tandem of {\tt
watching(stop,\ldots)} and {\tt whenever(stop, \ldots)} agents.
They are used to get the effect of a {\tt do \ldots watching
\ldots trigger \ldots} construct in which an agent is activated
when a {\tt do \ldots watching \ldots} agent is aborted. Second
note that the {\tt controller} uses a newly created private
channel ({\tt X}) for communication with its {\tt mouse\_n}
agents. This allows multiple controllers (perhaps on different
mice) to be simultaneously active, without interference.

% \begin{table}
\begin{ccprogram}
\agent controller(Click, Start, Stop):: 
   X^\[watching\(Stop, whenever(Start, mouse\_zero(X, Click))\),
     whenever\(Stop, 
              \[X:0 -> \{zero\}, 
               X:1 -> \{one\}, 
               X:2 -> \{many\}\]\)\]..

\agent mouse\_zero(X, Click) :: 
   watching(Click, always\ \{X:0\}),
   whenever(Click, next\ mouse\_one(X, Click))..

\agent mouse\_one(X, Click)  :: 
   watching(Click, always\ \{X:1\}),
   whenever(Click, next\ mouse\_many(X, Click))..

\agent mouse\_many(X,\_Click) :: always\ (\{X:2\})..
\end{ccprogram}
A single {\tt mouse(Count, X, Click)} predicate could have been
defined, but the recursion in its definition would not satisfy
the syntactic conditions for boundedness. 

%\caption{Counting clicks on a mouse}\label{mouse-lib}
%\end{table}