%\section{The Language}
The \LBM\ is defined by its (programming) language.
It is a stack machine driven via a number of
instructions that may be classified into three major groups:
\begin{description}
\item[stack:]
  The stack will be basically used to perform data evaluation,
  and as intermediate stage to store data for other instructions.
  It is a polymorphic stack,
  that may hold:
  booleans,
  integers,
  data,
  gates, and
  experiments.
\item[automata:]
  The activity of the BUT is described by means of a state machine
  that moves between states upon successful synchronization.
\item[kernel:]
  Eventually, the BUT will block waiting for some synchronization to
  take place.
  The BUT will make a {\em kernel call} to offer a rendez--vous.
\end{description}

One of the most simple instructions removes one item from the stack:
  \verb/POP/.

\subsection{Data Evaluation in the Stack}
For data there is a clear distinction between a {\em variable}
and a {\em value}.
A variable is a buck ready to contain a {\em value}.
Variables are local to BUTs,
but values may be exchanged.
Within a BUT a variable is uniquely identified (or denoted)
by its {\bf index}.
Values may exist either on the stack or loaded into some variable.

\begin{itemize}
\item[]
  \verb/P_VAR variable_index/		\\
  push the index of a variable
\item[]
  \verb/P_VAL variable_index/		\\
  push a data value
\item[]
  \verb/L_VAR variable_index/		\\
  load a variable taking a value from the stack.
  The stack is not modified at all.
\item[]
  \verb/I_VAR total_number_of_variables variable_parameters/	\\
  initialize.
  Makes room for a number of variables,
  and loads a number of them with initial data.
\end{itemize}
\verb/I_VAR/ is intended for BUT instantiation.
At that moment,
room is made for all the variables in the BUT.
Those coming as actual parameters are directly loaded.
The others, internal variables,
will be loaded as their values become known.
Data values are passed at the stack between the caller and the callee.

Usually,
data are evaluated on the stack
(as it will be shown below),
and eventually loaded into some indexed position by means of \verb/L_VAR/,
or directly used from the stack.
\begin{itemize}
\item[]
  \verb/EVAL operation number_of_arguments/	\\
  It takes $N$ operands from stack,
  and calls the {\tt operation} with so many arguments,
  pushing the result back to the stack.
  Arguments to \verb/EVAL/ are removed from the stack.
\item[]
  \verb/EQUAL sort/				\\
  Takes $2$ arguments from the stack,
  checks them for equality,
  according to the initial algebra semantics for their \verb/sort/,
  and pushes the result (a {\tt boolean}) back to the stack.
\end{itemize}

\subsection{Gate Manipulation}
For gates,
there exist no concept of contents and container.
There is no similar concept to pass of data values.
Gates are statically identified by mean of an index,
and dynamically handled by means of relabeling.

Gate identification is a very specific problem derived from the very
peculiar mechanisms of \LOTOS, most notably the relabeling concept.
Gate values are not truly shared between BUTs.
Gates are not passed at process instantiation,
as data values are.
Gates have a rather isolated existence inside their definition scope,
and only when offers exported from the scope are considered outside,
the involved gate is changed from referring to the local name,
to refer to the external name.
This mechanism of changing names {\em on leave} is known as
``dynamic relabeling'',
and only requires to know gate indexes in their scope,
and indexes correspondences at scope boundaries.

%In most usual cases,
%gates are used in such a manner that call by value is a valid
%semantics model;
%but their are situations where it makes a difference.
%For instance,
%\begin{verbatim}
%  P [a, a]
%  where
%    process P [m, n] : noexit :=
%      m; stop || n; stop
%      endproc
%\end{verbatim}
%deadlocks,
%despite being both (local) $m$ and $n$ instantiated
%to the same external gate $a$.

\LB\ assumes the following handling of gate indexes.
During semantics analysis,
a unique index is given to each gate declared in the scope of a
process definition.
This is a direct mapping for gates declared as formal gates.
Other gates,
as those declared by means of \verb/hide/ operators,
get an scope extended to the innermost enclosing process definition.
This scope extension should not make any harm at run time,
since semantics analysis did its job previously.

These gate indexes are directly used as gate identification at
run-time.
Special care must be paid to relabeling,
that may only occur at
process instantiation,
and sum-- and par--expressions.
At this places,
it is needed a translation between the index above,
and the index below.

There is a single local instruction on gates,
since relabeling implies to inform the run-time support.
\begin{itemize}
\item[]
  \verb/P_GTE gate_index/		\\
  pushes the index onto the stack.
%\item[]
%  \verb/L_GTE gate_index gate_value/		\\
%  loads a value at an indexed position.
%  It is not using the stack.
%\item[]
%  \verb/I_GTE number_of_gates gate_parameters/		\\
%  initialization.
%  Makes room for so many gates,
%  and loads a few of them.
\end{itemize}
%\verb/I_GTE/ is intended for BUT instantiation.
%If no new gate is declared within it,
%the total number of gates is just the number of gate parameters,
%and all of them are loaded upon instantiation.
%There may be more gates
%(e.g. created via the {\tt hide} operator)
%for which room is made at instantiation time,
%but there value is loaded later on,
%by means of the \verb/L_GTE/ instruction.
%but their is no value associated to it,
%neither at instantiation time,
%nor at any moment later.

\subsection{BUT Description Instructions}
This set of instructions is organized as pairs of instructions:
\begin{verbatim}
    B_xxx  < argument > ...
      < body >
    E_xxx
\end{verbatim}
denoting the Beginning and End of some description.
This model has been chosen to easily match syntax parentheses in
most programming languages.
Easy code generation out of this is a must.

These instruction pairs do not make any sense by themselves,
but strictly organized in a certain context.
Therefore,
we shall use a bit of BNF
(Backus--Naur Form)
to denote their relationship,
but still more information will be provided later on,
when dealing with the mapping from \LOTOS\ to \LB.

%The following conventions are followed:
%\begin{center}
%  \begin{tabular}{l l}
%    \hline
%    ITEM		& constant				\\
%    item		& to be further refined			\\
%    $[$ it $]$	& 0 or 1 instances of it		\\
%    $[$ it $]*$	& 0 or more instances of it		\\
%    $[$ it $]+$	& 1 or more instances of it		\\
%    \hline
%  \end{tabular}
%\end{center}

The outmost instruction pair in a \LB\ description:
\begin{verbatim}
lbc :: B_LBC  specification_name
         [ BUT_definition ]+
         [ predicate ]*
       E_LBC
\end{verbatim}
The code for \LB\ will describe 1 or more BUTs.
There is always at least one,
corresponding to the {\em main} behaviour in a \LOTOS\ specification.
This main BUT is always labeled as $0$.
There are as many more as {\tt process} definitions in the source
specification.
Therefore there is a one to one mapping of processes to BUTs,
and BUTs may be identified by the name of their corresponding
{\tt process identifier}\footnote{
  The argument to \verb/B\_LBC/ is just for debugging purposes.
  }.

\LOTOS\ {\tt predicates} on {\tt action prefix expressions}
are translated into boolean valued functions.
There may be no predicate at all in a \LOTOS\ specification.

\begin{verbatim}
BUT_definition :: B_CRT  BUT_#  process_name
                    initial_state
                    [ state ]*
                  E_CRT
\end{verbatim}
Each \LOTOS\ {\tt process} is mapped to a \LB\ behaviour unit.
It is modeled as a state machine.
There is at least one initial state,
and there may be more\footnote{
  The second argument to \verb/B\_CRT/ is just for debugging purposes.
  }.

\begin{verbatim}
initial_state :: B_ENT  0
                   [ I_VAR  number_of_variables  parameter_variables ]
                   state_description
                 E_ENT

state :: B_ENT  state_#
           state_description
         E_ENT
\end{verbatim}

BUTs must be initialized upon instantiation.
Actual arguments are provided in the stack,
and must be loaded onto the formal variables.

Some activities may be carried on per state.
Local variables may be introduced via {\tt let expressions} in
\LOTOS.
These variables do exist from the initialization stage of the BUT
instantiation,
when all the variables in the BUT were created
(where creation just means making room for them).
But the value for a variable is not known at initialization time,
and it must be evaluated in a concrete state.

Furthermore,
guards may show up in certain states.
They must be evaluated,
and react to their result.

Once all the local variables are evaluated,
and guards are evaluated and found to be passed,
the BUT may proceed to instruct the Kernel of the next
synchronization requirements.
\begin{verbatim}
state_description :: [ local_definition  |  guard ]*
                     kernel_call
\end{verbatim}

\begin{verbatim}
local_definition :: B_LET
                      [ value_expression
                        [ L_VAR var_index ]+
                      POP                    ]+
                    E_LET
\end{verbatim}
LET constructs load a data value in one or more BUT variable(s).
\verb/value_expression/ will evaluate a data expression onto the
stack.
This value is loaded into as many variables as required,
and removed.

Guards may be stated by giving to expressions that are to check for
equality,
or by giving a single \verb/bool/ expression to be compared against
\verb/true/.
During semantics analysis,
the second case is expanded with the second expression,
and there is no longer but a single situation.
\begin{verbatim}
guard :: B_GRD
           value_expression
           value_expression
         EQUAL sort
         E_GRD
\end{verbatim}
A boolean value is pushed on top of the stack.
If it is {\tt false},
the BUT stops.
Otherwise, it may continue.

\LOTOS\ specification predicates,
are transformed into boolean valued functions.
LOTOS accepts two formats for predicates,
either two terms, or only one.
This second case is transformed into the first one during the analysis
phase,
by expanding a ``true'' value.
The stack is used as for guard evaluation:
\begin{verbatim}
predicate :: B_PRD  predicate_#
               value_expression
               value_expression
             EQUAL sort
             E_PRD
\end{verbatim}

\subsection{Kernel Call Instructions}
State transition is performed upon successful synchronization.
Since more partners may be involved in synchronization,
each BUT will just inform the kernel of its synchronization
requirements,
both architecture and offers,
and wait for the kernel to inform of success.

\begin{verbatim}
kernel_call :: synchronization_pattern
             | synchronization_offer

synchronization_pattern ::  hiding_expression
    | enable_expression   | disable_expression
    | parallel_expression | choice_expression
    | BUT_instantiation   | relabelling

synchronization_offer :: stop_expression | internal_action
                       | external_offer  | exit_expression
\end{verbatim}

For most of these kernel calls,
with the exceptions of {\tt stop} and {\tt BUT instantiation},
the following state(s) is(are) indicated to the kernel,
for it to return control
back to the adequate continuation state.

\begin{verbatim}
hiding_expression :: [ P_GTE gate_index ]+
                     MK_HD  next_state  number_of_gates
\end{verbatim}
This instruction informs the kernel of the creation of new gate on
which synchronization may take place.
The stack is used as intermediate storage for the values of the new
gate(s).

\begin{verbatim}
enable_expression :: [ P_VAR variable_index ]*
                     MK_EN  enabling_state  enabled_state  number_of_variables
\end{verbatim}
The BUT may split into two BUTs related by a
\LOTOS\ {\tt enable} operator.
A few variables may be used to capture {\tt exit} values.
The stack is used as intermediate storage for the indexes of the
variables to be used in capturing {\tt exit} values.

\begin{verbatim}
disable_expression :: MK_DIS normal_state disabling_state
\end{verbatim}
The BUT may split into two BUTs related by a
\LOTOS\ {\tt disable} operator.

\begin{verbatim}
parallel_expression :: parallel_explicit
    | parallel_interleaving | parallel_synchronization

parallel_explicit :: [ P_GTE gate_index ]*
                     MK_PE  state  state  number_ gates

parallel_interleaving :: MK_PI state state

parallel_synchronization :: MK_PS state state
\end{verbatim}
The BUT may split into two BUTs related by a
\LOTOS\ {\tt disable} operator.
There are three possibilities,
corresponding to full synchronization, interleaving,
and synchronization limited to some explicit gates
The stack is used as intermediate storage for the values of the
gate(s) on which synchronization is required.

\begin{verbatim}
choice_expression :: MK_CH state state
\end{verbatim}
The BUT may offer a number of exclusive choices.
These are grouped in pairs to simplify the code.
Some states will just split into two choices.
By composition of states of this kind,
as many choices as needed may be ``simultaneously'' offered for
synchronization.

\begin{verbatim}
BUT_instantiation :: [ value_expression ]*
                     [ P_GTE gate_index ]*
                     MK_PR  BUT_#  number_gates  number_values
\end{verbatim}
A BUT may eventually call another one.
In fact,
the old one does not exist any longer,
but is replaced by the new one.
The stack is used as an intermediate stage for actual gates and
values.

There is an implicit relabeling in \verb/BUT_instantiation/.
There may also be explicit relabeling as a consequence of compile
time expansion of sum-- and par--expressions	\\
\centerline{
  \verb/choice g in [a, b, c] [] B/ $\rightarrow$
  \((B)[a/g]\) []
  \((B)[b/g]\) []
  \((B)[c/g]\)
  }

%\begin{tabbing}
%mmmm \= mm \= mm \=	\kill
%  \> \verb/choice g in [a, b, c] [] B/ $\rightarrow$	\\
%  \> \>    \> \((B)[a/g]\)	\\
%  \> \> [] \> \((B)[b/g]\)	\\
%  \> \> [] \> \((B)[c/g]\)	\\
%\end{tabbing}

\begin{itemize}
\item[]
  \verb/RLBL outer_gate_index inner_gate_index/	\\
  instructs the kernel of the correspondence between gate indexes.
\end{itemize}

\subsection{Offers for Rendezvous}
One of the most simple offers by a BUT is the no--offer:
\begin{verbatim}
stop_expression :: MK_ST
\end{verbatim}

The next simplest transition is the {\tt internal} step:
\begin{verbatim}
internal_action :: MK_I next_state
\end{verbatim}
If the internal event occurs,
the BUT will resume at the {\tt next state}.

In action denotations,
a number of experiments are offered on a gate
for consideration by the environment.
If the pattern is accepted,
the BUT will move to the next state.
The complexity arises from the large (and variable) number of items to
consider in making such an offer
\begin{verbatim}
external_offer :: [ experiment ]*
                  MK_AD  next_state  gate  number_exps  predicate

experiment :: single_offer | multiple_offer

single_offer :: value_expression
                MK_EXP "!" sort

multiple_offer :: P_VAR  variable_index
                  MK_EXP  "?"  sort
\end{verbatim}

For a multiple offer,
a variable must be identified that will hold the data value
that will be eventually used in the rendez-vous.
Some partner is expected to provide a single value
for synchronization to succeed.
This value is stored in the variable whose index is provided.

lastly,
it is quite similar to offer an {\tt exit}
since there may be concrete values offered as exit status,
or multiple values.
Single offers are handled as \verb/gate !value/,
while multiple offers are handled as \verb/gate ?fv: sort/,
where \verb/fv/ is just a funny variable
that is never used.
\begin{verbatim}
exit_expression :: [ experiment ]*
                   MK_EX  number_of_offers
\end{verbatim}

% Local Variables:
% mode: indented-text
% comment-column: 0
% comment-start: "% "
% comment-end: ""
% comment-start-skip: "% *"

