%\section{Semantics}
The \LBM\ consists of four principal registers:
\begin{itemize}
\item[S]
  {\bf The Stack}:
  used to hold intermediate results:
  data values, gate and variable indexes,
  and experiment offers.

\item[F]
  {\bf The Frame}:
  (or environment)
  used to bind values to variables.

\item[C]
  {\bf The Code}:
  used to hold the \LBM\ code being executed.

\item[K]
  {\bf The Kernel Tree}:
  (a pointer to)
  used as a directed graph to preserve synchronization structure
  between concurrent behaviour units,
  as well as to remember next state after synchronization
  for offers.
\end{itemize}

The entire state of a BUT can be denoted by giving the content of its
four registers.
Thus,
each instruction in the machine can be described by giving the state
of the machine before and after its execution.
We call this a {\em machine transition}.
We will write it in the form	\\
\centerline{\((S, F, C, K) \rightarrow (S', F', C', K')\)}	\\
where the tuple on the left of the arrow gives the state before,
and the tuple on the right, the state after.
When we wish to indicate that part of a tuple in the before state is
repeated in the after state,
we shall split apart relevant information on the left hand side,
by expanding the structure of the corresponding register,
and repeat the same pieces in the right hand side,
as appropriate.

BUTs may be in a stable or in an unstable state.
Unstable BUTs shall be denoted as \((S, F, C, K)^*\),
%and will perform autonomous transitions into a new state.
the superscript is removed for stable states.
Unstable BUTs will perform spontaneous transitions until a stable
state is reached.
Then,
control is given to the kernel.
Eventually the kernel will return control by marking the BUT as
unstable.

The complete system is described by a collection of BUTs,
each one with its own state,
plus a shared Kernel Tree.
It holds dynamic information related to BUT synchronization
environment.
A BUT is allowed to extend the Kt along its branch,
but has no other opportunity to make use of it,
nor to access the dynamic environment via it.

The Kt holds the following types of information
\begin{tabbing}
mmmm \= \kill
  \> $\bullet\;$ hide \{set of gate indexes\}	\\
  \> $\bullet\;$ \verb/>>/ [list of variable indexes]	\\
  \> $\bullet\;$ \verb/|[]|/ \{set of gate indexes\}	\\
  \> $\bullet\;$ other operators:
		\verb/[>/, \verb/|||/, \verb/||/, \verb/[]/	\\
  \> $\bullet\;$ relabel \{pairs of gate indexes\}
\end{tabbing}

%\begin{itemize}
%\item
%  hide \{set of gate indexes\}
%\item
%  \verb/>>/ [list of variable indexes]
%\item
%  \verb/|[]|/ \{set of gate indexes\}
%\item
%  other operators:
%  \verb/[>/,
%  \verb/|||/,
%  \verb/||/,
%  \verb/[]/
%\item
%  relabel \{pairs of gate indexes\}
%%\item
%%  offer $<$gate, list of experiments, predicate$>$
%\end{itemize}

Lastly,
BUT may provide offers for synchronization to the kernel,
being each of these offers composed of	\\
\centerline{$<$gate, list of experiments, predicate$>$}

The code is organized in such a way that given
a BUT identification, $b$, and
a BUT entry point, $e$,
the next instruction may be found as \(C^b_e\).
When only one BUT is involved in a transition,
we shall write the shorter form \(C_e\) to identify entry $e$ of
current BUT.
When strict sequencing of instructions is the rule,
we shall use structural decomposition on the left hand side,
\(c:C\),
to denote that current instruction $c$ is followed by the code $C$.

The initial state of the system is denoted by an empty Kt,
and a single unstable BUT that holds
the main behaviour of the specification:
an empty stack, and a fresh (empty) frame.
\[
  (\mbox{nil}, \mbox{NewFrame}, C^0_0, \mbox{nil})^*
\]
By convention,
the main BUT is number 0,
and the first entry of every BUT is number 0.

In the remainder of this section,
we give the transitions for each \LBM\ instruction.

\subsection{Stack Manipulation Instructions}
\begin{quote}
  \( (s:S, F, \verb/POP/:C, K)^* \rightarrow (S, F, C, K)^* \)
\end{quote}
where the top element on the stack S is removed.
The code steps to the next instruction.

\begin{quote}
  \((S, F, \verb/P_VAR/\;i:C, K)^* \rightarrow (i:S, F, C, K)^*\)
\end{quote}

\begin{quote}
  \( (S, F, \verb/P_VAL/\;i:C, K)^* \rightarrow
      (F(i):S, F, C, K)^*\)
\end{quote}

\begin{quote}
  \((v:S, F, \verb/L_VAR/\;i:C, K)^* \rightarrow
    (v:S, F[F(i) \leftarrow v], C, K)^*\)
\end{quote}

\begin{quote}
  \( (S, F, \verb/I_VAR/\;t\;i:C, K)^* \rightarrow
    (\mbox{pop}^i(S), F', C, K)^*\)
  \\[-4ex]
  \begin{quote}
    where \(F' \leftarrow F[F \leftarrow \mbox{allocate}(t),
	       \forall j \in [0..i-1] F(j) \leftarrow \mbox{top}^j(S)]\)
  \end{quote}
\end{quote}

\begin{quote}
  \( (S, F, \verb/EVAL/\;o\;n:C, K)^* \rightarrow
    (v:\mbox{pop}^n(S), F, C, K)^*\)
  \\[-4ex]
  \begin{quote}
    where \(v \leftarrow o(\mbox{top}^0(S), \ldots \mbox{top}^{n-1}(S))\)
  \end{quote}
\end{quote}

\begin{quote}
  \( (s_0:s_1:S, F, \verb/EQUAL/\;s:C, K)^* \rightarrow
    ((s_0 =_s s_1):S, F, C, K)^*\)
\end{quote}

\begin{quote}
  \((S, F, \verb/P_GTE/\;i:C, K)^* \rightarrow (i:S, F, C, K)^*\)
\end{quote}

Instructions \verb/B_LBC/ and \verb/E_LBC/ have no semantics meaning;
they are just for syntax bracketing.

Instructions \verb/B_CRT/ and \verb/E_CRT/ have no semantics meaning;
they are just for syntax bracketing.
\verb/B_CRT/ associates a BUT identification to the following code,
and this information will be saved somewhere for later use when
evaluating \(C^b_e\).

Instructions \verb/B_ENT/ and \verb/E_ENT/ have no semantics meaning;
they are just for syntax bracketing.
\verb/B_ENT/ associates an entry number to the following code,
and this information will be saved somewhere for later use when
evaluating \(C^b_e\).

Instructions \verb/B_LET/ and \verb/E_LET/ have no semantics meaning;
they are just for syntax bracketing.

Instruction \verb/B_GRD/ has no semantics meaning;
it is just for bracketing purposes.

\begin{quote}
  \( ( \mbox{true}:S, F, \verb/E_GRD/:C, K)^* \rightarrow
    (S, F, C, K)^* \)	\\
  \( (\mbox{false}:S, F, \verb/E_GRD/:C, K)^* \rightarrow
    (\mbox{nil}, \mbox{nil}, \mbox{nil}, K)\)
\end{quote}
where the value on top of the stack is used to either step to the
next instruction,
that is another unstable state
(and the machine goes on);
or to a stable state, namely the \verb/stop/ state.

\begin{quote}
  \( (S, F, \verb/MK_HD/\;c\;n, K)^* \rightarrow
    (\mbox{pop}^n(S), F, C_c, K')^* \)
  \\[-4ex]
  \begin{quote}
    where \(K' \leftarrow \mbox{hide}\{\mbox{top}^i(S), i=0..n-1\} : K\) 
  \end{quote}
\end{quote}

The Kt is extended with a hiding node that holds the indexes of the
gates that only exist under this node.

\begin{quote}
  \( (S, F, \verb/MK_EN/\;c_1\;c_2\;n, K)^* \rightarrow
	  \{(S', F, C_{c_1}, K')^*, (S', F, C_{c_2}, K')\} \)
  \\[-4ex]
  \begin{quote}
    where \(S' \leftarrow \mbox{pop}^n(S)\)	\\
    and   \(K' \leftarrow \verb/>>/[\mbox{top}^i(S), i=0..n-1] : K\) 
  \end{quote}
\end{quote}

The BUT splits into two concurrent machines. 
One of them, the enabling branch, 
is still unstable and needs further unfolding.
The other one, the enable side,
is just recorded onto the Kernel Tree.

\begin{quote}
  \( (S, F, \verb/MK_DIS/\;c_1\;c_2, K)^* \rightarrow
	  \{(S, F, C_{c_1}, K')^*, (S, F, C_{c_2}, K')^*\} \)	\\[-4ex]
  \begin{quote}
    where \(K' \leftarrow \verb/[>/ : K\)
  \end{quote}
\end{quote}

The machine splits in two unstable pieces,
both of them working under a Kt enriched with a disabling node.

\begin{quote}
  \( (S, F, \verb/MK_PE/\;c_1\;c_2\;n, K)^* \rightarrow
	  \{(S', F, C_{c_1}, K')^*, (S', F, C_{c_2}, K')^*\} \)	\\[-4ex]
  \begin{quote}
    where \(S' \leftarrow \mbox{pop}^n(S)\)	\\
    and   \(K' \leftarrow \verb/|[]|/\{\mbox{top}^i(S), i=0..n-1\} : K\) 
  \end{quote}
\end{quote}

The machine splits into two unstable machines,
that need further unfolding.
The parameters are recorded into the Kt.

\begin{quote}
  \( (S, F, \verb/MK_PI/\;c_1\;c_2, K)^* \rightarrow
	  \{(S, F, C_{c_1}, K')^*, (S, F, C_{c_2}, K')^*\} \)	\\[-4ex]
  \begin{quote}
    where \(K' \leftarrow \verb/|||/ : K\) 
  \end{quote}
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_PS/\;c_1\;c_2, K)^* \rightarrow
	  \{(S, F, C_{c_1}, K')^*, (S, F, C_{c_2}, K')^*\} \)	\\[-4ex]
  \begin{quote}
    where \(K' \leftarrow \verb/||/ : K\) 
  \end{quote}
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_CH/\;c_1\;c_2, K)^* \rightarrow
	  \{(S, F, C_{c_1}, K')^*, (S, F, C_{c_2}, K')^*\} \)	\\[-4ex]
  \begin{quote}
    where \(K' \leftarrow \verb/[]/ : K\) 
  \end{quote}
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_PR/\;B\;g\;v, K)^* \rightarrow
    (\mbox{pop}^g(S),
      \mbox{NewFrame},
      C^B_0,
      \verb/relabel/\{\mbox{top}^i(S) \leftrightarrow i, i=0..g-1\} : K)^* \)
\end{quote}
where internal index $i$ is associated to external index
\(\mbox{top}^i(S)\).

\begin{quote}
  \( (S, F, \verb/RLBL/\;e\;i:C, K)^* \rightarrow
    (S, F, C, \verb/relabel/\{e \leftrightarrow i\} : K)^* \)
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_ST/, K)^* \rightarrow
	  (\mbox{nil}, \mbox{nil}, \mbox{nil}, K) \)
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_I/\;c, K)^* \rightarrow (S, F, C_c, K) \)
%  \\[-4ex]
%  \begin{quote}
%    where \(K' \leftarrow \mbox{offer}<i, (S, F, C_c, K')>:K) \)
%  \end{quote}
\end{quote}

An offer \(<i, nil, nil>\) is handed to the kernel,
and the BUT stabilizes.
Upon occurrence,
the state becomes unstable,
and the BUT resumes at \(C_c\).

\begin{quote}
  \( (S, F, \verb/MK_AD/\;c\;g\;e\;p, K)^* \rightarrow
    (\mbox{pop}^e(S), F, C_c, K) \)
\end{quote}

An offer
\(<g, [\mbox{top}^i(S), i=0..e-1], p>\)
is handed to the kernel,

\begin{quote}
  \( (v:S, F, \verb/MK_EXP/\;\verb/"!"/\;s:C, K)^* \rightarrow
	  (\mbox{experiment}(\verb/"!"/, v, s):S, F, C, K)^* \)
\end{quote}

\begin{quote}
  \( (i:S, F, \verb/MK_EXP/\;\verb/"?"/\;s:C, K)^* \rightarrow
    (\mbox{experiment}(\verb/"?"/, i, s):S, F, C, K)^* \)
\end{quote}

\begin{quote}
  \( (S, F, \verb/MK_EX/\;e, K)^* \rightarrow
      (\mbox{nil}, \mbox{nil}, \mbox{nil}, K) \)
\end{quote}

An offer
\(<\mbox{exit}, [\mbox{top}^i(S), i=0..e-1], nil>\)
is handed to the kernel.

The complete \LOTOS\ machine follows the following instruction cycle:

\small
\begin{tabbing}
mmmm \= mm \= mm \= mm \= \kill
  \> start \((\mbox{nil}, \mbox{NewFrame}, C^0_0, \mbox{nil})^*\) \\
  \> LOOP \\
  \>   \> FOREACH unstable BUT \\
  \>   \>   \> WHILE unstable \\
  \>   \>   \>   \> perform \LBM\ instruction \\
  \>   \> select a collection of offers for rendezvous \\
  \>   \> IF (collection found) THEN \\
  \>   \>   \> perform rendezvous AND
		mark the selected collection as unstable \\
  \>   \> ELSE \\
  \>   \>   \> exit loop \\
  \> ENDLOOP
\end{tabbing}
\normalsize

The selection of partners for rendezvous is a complicated algorithm
that is performed by the run time support.
Details may be found in \cite{topo:rendezvous}.
Upon finding enough and convenient partners for participating in a
rendezvous,
the kernel tree may need to be pruned.
This situation happens for mutually exclusive offers,
namely:
\begin{tabbing}
mm \= \kill
  \> $\bullet\;$ \verb/[]/:
    when a branch of a choice operator is selected,
    the other ones must be removed;	\\
  \> $\bullet\;$ \verb/[>/:
    when the disabling branch is selected,
    the normal behaviour must be removed.
\end{tabbing}
Lastly,
when an \verb/exit/ event occur,
if there is a branch waiting at an enabling operator,
the enabled branch becomes unstable.

This completes the dynamic semantics of the \LBM.

