
\nbbb{Behaviour Definitions}

A typical, informal rendition of abstracted behaviours, \texttt{BA,
  BC, BD, ...} is shown in Fig.\,\vref{ictac.cmds}.

\begin{figure}[h]
  \begin{center}
    \epsfig{file=cmds.eps,width=14.1cm}
    \label{ictac.cmds}
    \caption{Communicating Behaviours}
  \end{center}
\end{figure}

%\noindent
\begynd
\pind Figure\,\vref{ictac.cmds} should be understood as
  follows:\footnote{The explanation of Fig.\,\ref{ictac.cmds}
  is in now way an attempt to explain the semantics of
  behaviours. That is left to the \texttt{RSL$^{+}$} formalization's.}
\begynd
\pind The \sort{bold faced} labels \sort{BA, BB, BC, ...} are meant to
      designate behaviours.
\pind The \sort{black arrows}, from behaviour \sort{Bx} to behaviour
      \sort{By} are meant to designate \texttt{CSP}-like
      \textsl{communications} from  \sort{Bx} to   \sort{By}.
\pind The \sort{open arrows} (``white''), from behaviour \sort{Bx} to behaviour
      \sort{By} are meant to designate possible \texttt{CSP}-like
      \textsl{communications} from  \sort{Bx} to   \sort{By}.
\pind These latter communications, the ``possible'' ones, are then
      thought of as \textsl{in response} to the ``earlier'', in the
      figure: ``immediately prior, next to'' communication from
      \sort{Bx} to \sort{By}.
\afslut
\afslut

\begynd
\pind Figure\,\vref{ictac.cmds} is now given a more precise
      ``meaning'' -- with this ``meaning'' suggesting a general
      ``pattern'' for behaviour definitions:
\afslut

\begin{enumerate}\setei
\item \label{bd-0000} There are behaviours \texttt{B, ...} with
                      identities \texttt{bi, ... }.
\begin{enumerate}
\item \label{bd-0010} These behaviours,typically, have the form
                      of internal, {\NONDETCHOICE},
                      non-deterministically ``choosing'' between  
\item \label{bd-0020} \textsl{pro-actively}
                      initiating communications with other behaviors
\item \label{bd-0030} and \textsl{re-actively} responding to such
                      initiatives.
\end{enumerate}
\savei\end{enumerate}


%\RSLatex
%value
%&\ref{bd-0010}.&   B(bi)(mereo)(stat)(mon)(prg) is
%&\ref{bd-0020}.&       pro_active_B(bai)(mereo)(stat)(mon)(prg)
%&\ref{bd-0030}.&   |^| re_active_B(bai)(mereo)(stat)(mon)(prg) 
%\endRSLatex
\bp
\kw{value}\\
\ref{bd-0010}.\ \ \ B(bi)(mereo)(stat)(mon)(prg) {\IS}\\
\ref{bd-0020}.\ \ \ \ \ \ \ pro\_active\_B(bai)(mereo)(stat)(mon)(prg)\\
\ref{bd-0030}.\ \ \ {\NONDETCHOICE} re\_active\_B(bai)(mereo)(stat)(mon)(prg) 
\ep

\begin{enumerate}\setei
\item \label{bd-0049} \iprf{bd-0020} The pro-active behaviour (\texttt{B}) internal
                     deterministically ({\NONDETCHOICE}) choosing between a number of
                     initiating actions:
\begin{multicols}{2}
\begin{enumerate} 
\item \label{bd-0050} action 1,
\item \label{bd-0060} action 2,
\item \label{bd-0070} ...,
\item \label{bd-0080} action n.
\end{enumerate}
\end{multicols}
\savei\end{enumerate}
%\RSLatex 
%value
%&\ref{bd-0049}.,\iprf{bd-0020}.&  pro_active_B(bi)(mereo)(stat)(mon)(prg) is
%&\ref{bd-0050}.&                  B_action_1(bi)(mereo)(stat)(mon)(prg)
%&\ref{bd-0060}.\,\,\,&             |^| B_action_2(bi)(mereo)(stat)(mon)(prg)  
%&\ref{bd-0070}.\,\,\,&             |^| ...
%&\ref{bd-0080}.\,\,\,&             |^| B_action_m(bi)(mereo)(stat)(mon)(prg)   
%\endRSLatex 
\bp
\kw{value}\\
\ref{bd-0049}.,\iprf{bd-0020}.\ \ pro\_active\_B(bi)(mereo)(stat)(mon)(prg) {\IS}\\
\ref{bd-0050}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ B\_action\_1(bi)(mereo)(stat)(mon)(prg)\\
\ref{bd-0060}.\,\,\,\ \ \ \ \ \ \ \ \ \ \ \ \ {\NONDETCHOICE} B\_action\_2(bi)(mereo)(stat)(mon)(prg)\ \ \\
\ref{bd-0070}.\,\,\,\ \ \ \ \ \ \ \ \ \ \ \ \ {\NONDETCHOICE} {\DOTDOTDOT}\\
\ref{bd-0080}.\,\,\,\ \ \ \ \ \ \ \ \ \ \ \ \ {\NONDETCHOICE} B\_action\_m(bi)(mereo)(stat)(mon)(prg)\ \ \ 
\ep

\noindent
\begynd
\pind 
\afslut

\begin{enumerate}\setei
\item \iprf{bd-0020}. The \texttt{respond}ing behaviour (\texttt{B})
                      reacts to a number of such initiating actions by
\begin{enumerate}
\item \label{bd-0021} external non-deterministically ({\DETCHOICE})
                      offering to accept messages from responding
                      behaviours, 
\item \label{bd-0022} and then performing corresponding actions.
\end{enumerate}
\savei\end{enumerate}

%\RSLatex 
%value
%&\ref{bd-0021}.,\iprf{bd-0020}.&  respond_B(bi)(mereo)(stat)(mon)(prg) is
%&\ref{bd-0021}.&                  let msg = |=| { &\commq{bj,bi}& | bj:BI :- &bj\,&isin&\,&bis } in
%&\ref{bd-0022}.&                  react_behaviour_B(bi)(mereo)(stat)(mon)(prg)(&\brcolor{msg}&) end  
%\endRSLatex 
\bp
\kw{value}\\
\ref{bd-0021}.,\iprf{bd-0020}.\ \ respond\_B(bi)(mereo)(stat)(mon)(prg) {\IS}\\
\ref{bd-0021}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \kw{let} msg {\EQ} {\DETCHOICE} {\LBRACE} \commq{bj,bi} {\BAR} bj:BI {\RDOT} bj\,{\ISIN}\,bis {\RBRACE} \kw{in}\\
\ref{bd-0022}.\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ react\_behaviour\_B(bi)(mereo)(stat)(mon)(prg)(\brcolor{msg}) \kw{end}\ \ 
\ep
  
\begin{enumerate}\setei
\item \label{bd-0090} The \texttt{react\_behaviour\_B}  inquires as to
                      the type of the message, say,  
                      a command, received (\brcolor{?}): if it is:
\begin{enumerate} 
\item \label{bd-0100} of type \texttt{Cmd\_i} then it
                      performs action \texttt{act\_cmd\_i}, 
\item \label{bd-0110} of type \texttt{Cmd\_j} then it
                      performs action \texttt{act\_cmd\_j},
\item \label{bd-0120} ..., or
\item \label{bd-0130} of type \texttt{Cmd\_k} then it
                      performs action \texttt{act\_cmd\_k}.
\item \label{bd-0140} If it is of neither of these types then it
                      ``skips'' treatment of that response by resuming
                      to be the behaviour \texttt{B}. 
\end{enumerate}
\savei\end{enumerate}
%\RSLatex 
%value
%&\ref{bd-0090}.&  react_behaviour_B(bi)(mereo)(stat)(mon)(prg)(&\brcolor{msg}&) is
%&\ref{bd-0100}.&       is_action_i(msg) -> B_action_i(bi)(mereo)(stat)(mon)(prg)(&\brcolor{msg}&),
%&\ref{bd-0110}.&       is_action_j(msg) -> B_action_j(bi)(mereo)(stat)(mon)(prg)(&\brcolor{msg}&),
%&\ref{bd-0120}.&       ...,
%&\ref{bd-0130}.&       is_action_k(msg) -> B_action_k(bi)(mereo)(stat)(mon)(prg)&(\brcolor{msg})&,
%&\ref{bd-0140}.&       _ -> B(bi)(mereo)(stat)(mon)(prg)  
%\endRSLatex 
\bp
\kw{value}\\
\ref{bd-0090}.\ \ react\_behaviour\_B(bi)(mereo)(stat)(mon)(prg)(\brcolor{msg}) {\IS}\\
\ref{bd-0100}.\ \ \ \ \ \ \ is\_action\_i(msg) {\RIGHTARROW} B\_action\_i(bi)(mereo)(stat)(mon)(prg)(\brcolor{msg}),\\
\ref{bd-0110}.\ \ \ \ \ \ \ is\_action\_j(msg) {\RIGHTARROW} B\_action\_j(bi)(mereo)(stat)(mon)(prg)(\brcolor{msg}),\\
\ref{bd-0120}.\ \ \ \ \ \ \ {\DOTDOTDOT},\\
\ref{bd-0130}.\ \ \ \ \ \ \ is\_action\_k(msg) {\RIGHTARROW} B\_action\_k(bi)(mereo)(stat)(mon)(prg)(\brcolor{msg}),\\
\ref{bd-0140}.\ \ \ \ \ \ \ {\UNDERLINE} {\RIGHTARROW} B(bi)(mereo)(stat)(mon)(prg)\ \ 
\ep

\nbbb{Action Definitions}

\begynd
\pind \textsl{``Actions are what makes behaviours meaningful''}
\begynd
\pind We remind the reader that our function (incl.\,behaviour) definitions
\pind are expressed in a functional, ``applicative'', style.
\pind {[} that is, there are no assignable variables {]}
\pind The actions elaborate to \sort{value}s.
\pind These values may be 
\begynd
\pind Booleans, numbers, sets, Cartesians, lists,
      maps and functions
\afslut (over these), 
\pind or the values by be \texttt{()}, of type \sort{Unit}, 
\pind as are the values (also of never-ending) behaviours.
\afslut
\afslut

\begynd
\pind Action signatures usually ``follow that'', i.e., are the same as
      ``their'' initiating behaviour signatures.
\afslut


\begin{enumerate}\setei
\item \label{act-0000} Actions, as semantic quantities,
\begin{enumerate}
\item \label{act-0010}  evaluate some values,
\item \label{act-0020}  typically change some programmable attributes,
\item \label{act-0030}  and may communicate, ``issue'' or inform, 
                        to some other behaviours, some requests,
                        respectively information --
\item \label{act-0040}  whereupon the ``revert'', ``tail-recursively''
                        to the activating Behaviour.
\end{enumerate}
\savei\end{enumerate}


%\RSLatex
%&\ref{act-0000}.&  action_i(bi)(mereo)(stat)(mon)(prg) is
%&\ref{act-0010}.&      let v = evaluate_i(bi)(mereo)(stat)(mon)(prg) in
%&\ref{act-0020}.&      let (bj,prg&$'$&) = elaborate_i(v)(bi)(mereo)(stat)(mon)(prg) in
%&\ref{act-0030}.&      &{\comms{bi,bj}}$\mathcal{E}$(prg$'$)& ;
%&\ref{act-0040}.&      behaviour(bi)(mereo)(stat)(mon)(prg&$'$&)
%&\ref{act-0000}.\,&       end end  
%\endRSLatex
\bp
\ref{act-0000}.\ \ action\_i(bi)(mereo)(stat)(mon)(prg) {\IS}\\
\ref{act-0010}.\ \ \ \ \ \ \kw{let} v {\EQ} evaluate\_i(bi)(mereo)(stat)(mon)(prg) \kw{in}\\
\ref{act-0020}.\ \ \ \ \ \ \kw{let} (bj,prg$'$) {\EQ} elaborate\_i(v)(bi)(mereo)(stat)(mon)(prg) \kw{in}\\
\ref{act-0030}.\ \ \ \ \ \ {\comms{bi,bj}}$\mathcal{E}$(prg$'$) ;\\
\ref{act-0040}.\ \ \ \ \ \ behaviour(bi)(mereo)(stat)(mon)(prg$'$)\\
\ref{act-0000}.\,\ \ \ \ \ \ \ \kw{end} \kw{end}\ \ 
\ep

\noindent
\begynd
\pind Variants of Item \iprf{act-0030} are also used: 
\afslut

%\RSLatex
%     { &{\comms{bi,bj}}$\mathcal{E}$(prg$'$)& | bj isin bis } ;
%\endRSLatex 
\bp 
\>\>\ {\LBRACE} {\comms{bi,bj}}$\mathcal{E}$(prg$'$) {\BAR} bj {\ISIN} bis {\RBRACE} ;
\ep

\noindent
\begynd
\pind where \texttt{bj} ranges over \texttt{bis}, a set of behaviour identities.
\afslut

%%  LocalWords:  Behaviour behaviours BD ictac cmds RSL behaviour CSP
%%  LocalWords:  deterministically mereo mon prg bai bd ing Cmd cmd
%%  LocalWords:  msg bj applicative Booleans Cartesians
