\subsubsection{An automated teller machine}\label{ATM}
We present a program for the bank teller machine (ATM)
of~\cite{CRP}.  This machine accepts an ATM card and verifies the
identification number.  On receiving an incorrect number thrice,
the machine swallows the card; else it asks for an amount,
requests the bank's authorization, and releases the money if
authorization is received; keeping the card otherwise (!). The
customer may cancel the operation at any time.

Our solution is  presented below.
The structure of the program should be fairly clear. The basic
technique of {\em persistent tells} is used to communicate
information between losely coupled subsystems. Consider for
example the interaction between the ATM controller and the bank.
The ATM has access to the communication channels {\tt card} and
{\tt code}. It must communicate these channels to the bank, thus
allowing the bank to read other messages on the channel. (For
example, the display would be expected to add (also using
persistent tells)  tokens of the form {\tt card:N, code:P} to the store,
for {\tt N} the bank account number read from the card, and {\tt
P} the password read from the display.) Since there can be no
guarantee that the bank will process the information sent to it
in the current time instant --- for example, the bank may be
busy in this time instant servicing some other request ---  the
sender must maintain the item in the store indefinitely. This is
achieved by the idiom:
\begin{ccprogram}
\agent watching(received, always\ \{message\})..
\end{ccprogram}
\noindent Here, {\tt message} is the signal being sent to some
other agent, and {\tt received} is the signal that it uses to
acknowledge receipt. 

The program also illustrates a simple convention. Typically an
agent adds to the store a pure ``signal'' (that is, a $0$-ary
constant, e.g. {\tt auth}), together with some messages on the
signal (e.g. {\tt auth:false}). Another agent may detect the
signal by suspending on the constant; subsequently the messages
associated with the signal may be examined in detail.  This
technique is particularly useful in situations (such as with the
{\tt card} signal) in which an agent in the  environment may be
passing a complex (unbounded) data-structure (e.g., card number)
{\em through} the finite state controller to another agent in the
environment (e.g., bank). The code for the controller never has
to handle the complex data-structure, it merely senses
information on a (pure) signal and passes that on.  In this way,
the mobility of the underlying communication mechanism can be
used to maintain boundedness of the controller code. 

\begin{ccprogram}
\agent ready:: 
  [whenever(card,
   \quad  \[watching((keep\_card ; cancel),
            \quad \[verify\_code(0),
                   whenever(code\_ok, 
                     \quad \[\{display:enter\_amount\},
                            whenever(amount, verify\_funds)\]) \]),
           whenever((keep\_card ; cancel), keep\_card ~> \{emit\_card\}) \]),
  whenever((keep\_card; emit\_card),  next\ ready)]..

\agent verify\_code(Num):: 
  \[Num \lt 3 
    -> \[\{display: enter\_code\},
        \quad \R whenever(code,
                 \quad\[watching\(verif, 
                                  always\ \{bank:verify,bank:verify(card, code)\}\),
                        \R whenever(verif,
                          \quad \[verif: true  -> \{code\_ok\},
                                  \R verif: false 
                                     -> N1\$(N1\ is\ Num+1 -> next\ verify\_code(N1))\L\])\L
                       \])\L \],
  Num {={}}:{={}}\ 3 -> \{keep\_card\}\]..

\agent verify\_funds:: 
 \[watching\(auth, 
              always\ \{bank:request\_auth,bank: request\_auth(card, amount)\}\),
 whenever\(auth,
 \quad    \[auth : true -> \{delivermoney, emit\_card\},
     auth : false -> \{keep\_card\}\]\)]..
\end{ccprogram}

\newpage