🚀 go-pugleaf

I am new into LOTOS and I have just worked my way through the
introduction in LOTOS by Bolognesi and Brinkman.  Now, on trying to
use LOTOS, I have encountered a problem which is very basic to my
understanding of the formalism. I would appreciate any help with the
following:

I wish to define a ring of processes with the following layout:

                     1
                    / \
                   c   a
                  /     \
                 3 - b - 2

1, 2 and 3 are processes; a, b and c are actions.

My first approach is to formulate this in LOTOS as:

   hide a, b, c in
     node[c,a](1) ||
     node[a,b](2) ||
     node[b,c](3)
   where process node[in,out](n:int): exit := 
     ...
   end process

However, from the explanation of the semantic of the || operator, I
understand that this forces all processes to work in full
synchronization.  This would mean that if nodes 1 and 2 can
communicate action ``a'', that this communication can occur only if
node 3 also cooperates in it.

This is clearly not what I want, the |[...]| operator seems more
appropriate.  However, I am only able to use this operator between
nodes 1 and 2 and between 2 and 3:

     node[c,a](1) |[a]|
     node[a,b](2) |[b]|
     node[b,c](3)

The |[c]| operator misses. In order to represent the layout I want, I
need a two-dimensional formalism, while LOTOS, being a textual
formalism, clearly is one-dimensional.

I would like to know whether I am wrong about the semantics of the ||
operator, or whether such a ring indeed cannot be represented in
LOTOS.

Kind regards,				Jan Rekers

J. Rekers, Department of Computer Science, Leiden University
P.O. box 9512, 2300 RA Leiden, the Netherlands
email: rekers@rulwi.LeidenUniv.nl