🚀 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

In article <1992Oct1.085838.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.
 
You can specify this in LOTOS:

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


However, the ring is a deadlock since 2 is waiting for 1,
3 for 2, and 1 for 3.

You need something to kick off the ring, such as:

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

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