🚀 go-pugleaf

In article <1992Oct1.141058.19700@hasler.ascom.ch> dubuis@tech.ascom.ch writes:
>In article 7536@rulway.LeidenUniv.nl, rekers@elc2 (Jan Rekers) writes:
>> 
>> I wish to define a ring of processes with the following layout:
>> 
>>                      1
>>                     / \
>>                    c   a
>>                   /     \
>>                  3 - b - 2
>
>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

The solution works as it should, but it is somehow asymetrical.

It does a perfect job in hiding the action ``a'', which should be
private between nodes 1 and 2 from any behaviour of node 3.

However, it does not prevent node 2 to perform an action ``c''
which should be used only to communicate between nodes 1 and 3,
neither does it forbid node 1 to break in the communication of 
action ``b'' between nodes 2 and 3.

From the specification of the nodes themselves, I understand that such
disruptions will never occur, but I think that they should be prevented
at top-level with the |[...]| operator.

According to me, LOTOS should have a possibility to separate the
declaration of processes from the declaration of their interaction
with other processes. That would allow for more symetrical solutions
for the above problem. Something like this:

hide a, b, c in
  declare processes
    n1 := node[c,a],
    n2 := node[a,b],
    n3 := node[b,c]
  with communications
    n1 |[a]| n2,
    n2 |[b]| n3,
    n3 |[c]| n1

Don't fuss about the syntax just invented, just about the idea's
behind it. Did I just made a perfect fool of myself?

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
-- 
J. Rekers, Department of Computer Science, Leiden University
P.O. box 9512, 2300 RA Leiden, the Netherlands
email: rekers@rulwi.LeidenUniv.nl