🚀 go-pugleaf

In article 7536@rulway.LeidenUniv.nl, rekers@elc2 (Jan Rekers) writes:
> 
> 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
> 

The semantics of the LOTOS parallel operator is indeed not trivial, and I
do not want to discuss it -- there are much more competent people to do so.
However, the parallel operator, in conjunction with the hide operator, is
powerfull enough to specify a ring topology.  (I assume these two operators
allow to specify any static toplogy.  To specify dynamic changing topolgies,
recursion over these operators is necessary.)

Here follows my solution:

specification ring : noexit
behaviour
  hide b,c in
    (
    hide a in
      ( node1 [c,a]
        |[a]|
        node2 [a,b]
      )
      |[c,b]|
      node3 [b,c]
    )
where
  process node1 [p,q] : noexit :=
     p ; q ; node1 [p,q]
  endproc
  process node2 [p,q] : noexit :=
     p ; q ; node2 [p,q]
  endproc
  process node3 [p,q] : noexit :=
     q ; p ; node3 [p,q]
  endproc
endspec

Note that I introduced 3 node processes.  Two of them are identical; the difference
of the third one (node3) is that in its inital state (so to say) it is ready to
synchronise at its output gate, whereas the others try to synchronise at their
input gates in their initial states.

Simulation the above specification using the simulator Smile (a component of
LITE, the LOTOSPHERE Integrated Tool Environment) one obtains the following
simulation tree:

<root-node>
    I(c) 
        I(a) 
            I(b)  (* Recursion detected *)
                I(c)  (* Recursion detected *)
                    I(a)  (* Recursion detected *)
                        I(b)  (* Recursion detected *)
                            I(c)  (* Recursion detected *)

Kind regards,

Eric Dubuis

---
*****************************************************************************
Eric Dubuis,					Tel.:	 +41 31 999 3790
Ascom Tech Ltd., V/TID,				Fax:	 +41 31 991 5211
CH-3018 Berne, Switzerland			E-mail:	 dubuis@tech.ascom.ch