%\section{Complete Example}
\begin{verbatim}
specification sample : noexit
                      B_LBC sample
                      B_CRT 0 sample
                        B_ENT 0
                          I_VAR 0 0
  type Natural_numbers is
    sorts nat
    opns 0: -> nat
         s: nat -> nat
    endtype
behaviour
  hide send, receive in
                            P_GTE 0
                            P_GTE 1
                          MK_HD  1 2
                        E_ENT
    ( producer [send] (0)
                        B_ENT 3
                            EVAL 0 0
                            P_GTE 0
                          MK_PR 3 1 1
                        E_ENT
    |||
                        B_ENT 2
                          MK_PI 3 4
                        E_ENT
      consumer [receive]
                        B_ENT 4
                            P_GTE 1
                          MK_PR 2 1 0
                        E_ENT
    )
    |[ send, receive ]|
                        B_ENT 1
                            P_GTE 0
                            P_GTE 1
                          MK_PE 2 5 2
                        E_ENT
    buffer [send, receive]
                        B_ENT 5
                            P_GTE 0
                            P_GTE 1
                          MK_PR 1 2 0
                        E_ENT
                      E_CRT
where
  process producer [g] (n: nat) : noexit :=
                      B_CRT 3 producer
                        B_ENT 0
                          I_VAR 1 1
    g !n ;
                              P_VAL 0
                            MK_EXP ! 7
                          MK_AD 1 0 1 -1
                        E_ENT
    producer [g] (s(n))
                        B_ENT 1
                              P_VAL 0
                            EVAL s 1
                            P_GTE 0
                          MK_PR 3 1 1
                        E_ENT
    endproc           E_CRT

  process consumer [g] : noexit :=
                      B_CRT 2 consumer
                        B_ENT 0
                          I_VAR 1 0
    g ?x: nat ;
                              P_VAR 0
                            MK_EXP ? 7
                          MK_AD 1 0 1 -1
                        E_ENT
    consumer [g]
                        B_ENT 1
                            P_GTE 0
                          MK_PR 2 1 0
                        E_ENT
    endproc           E_CRT

  process buffer [a, b] : noexit :=
                      B_CRT 1 buffer
                        B_ENT 0
                          I_VAR 1 0
    a ?d: nat ;
                              P_VAR 0
                            MK_EXP ? 7
                          MK_AD 2 0 1 -1
                        E_ENT
    b !d ;
                        B_ENT 2
                              P_VAL 0
                            MK_EXP ! 7
                          MK_AD 3 1 1 -1
                        E_ENT
    buffer [a, b]
                        B_ENT 3
                            P_GTE 0
                            P_GTE 1
                          MK_PR 1 2 0
                        E_ENT
    endproc           E_CRT
endspec               E_LBC
\end{verbatim}

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

