Translation of CSP model to pycsp - synchronizing on shared alphabet events

[Andy Clegg]

Hi,

I'm attempting to implement a system using pycsp that I have formally
modelled in CSP. I am a bit stuck on how the concepts of how processes
with shared alphabets translate into code. As an example, I have:

A = w -> z -> A
B = x -> z -> B
C = y -> z -> C

If I want to implement the system (A || B || C), how do I make sure
that all 3 processes synchronize at z? How are these events modelled
in pycsp?

Many thanks,

Andy

[Rune Møllegaard Friborg]

Hi Andy,

You mention that you want all three processes to synchronize at z
(similar to a barrier), but I read your description

A = w -> z -> A
B = x -> z -> B
C = y -> z -> C

as you want all processes to participate in the event z..

Creating w,z,y and z as channels and having processes A,B,C
communicate on the channels, should
create the result you want.

w,z,y and z must be connected to processes that implement the events.

Was this helpfull?

- Rune

[Andy]

Hi Rune,

Thanks for your input - yes I would like all the processes to

participate in the event z.

If I were to create w,x,y,z as channels, and if I assume that A is the
process that sets event z in motion, then presumably A should send a
message over channel z to signify that event z is happening. How can
I ensure that processes B and C can both receive the message? From my
experiments with channels, as soon as the message is read by one
reader, it is gone, and not available for other readers.

Many thanks again,

Andy

2010/11/22 Rune Møllegaard Friborg <ru...@diku.dk>:

[Rune Møllegaard Friborg]

I'll try an provide an answer through a piece of code.

w,x,y,z = Channel() * 4

@process
def eventProcess(cin, label=''):
while True:
print 'eventP(' + label + "):" + str(cin())

The formal semantics for evenProcess should correspond to:

eventProcess = cin -> eventProcess

Now we create A, B and C

@process actionProcess(cout1, cout2, label=''):
while True:
cout1(label)
cout2(label)

and finally we put everything together

Parallel(
eventProcess(w.reader(), 'w'), eventProcess(x.reader(), 'x'),
eventProcess(y.reader(), 'y'), eventProcess(z.reader(), 'z'),
actionProcess(w.writer(), z.writer(), 'A'),
actionProcess(x.writer(), z.writer(), 'B'),
actionProcess(y.writer(), z.writer(), 'C')
)

- Rune

[Andy]

That code is interesting, thanks. However, if I modify it slightly, as follows:
@process
def actionProcess(cout1, cout2, label='', sleep=1):
while True:
cout1(label)
time.sleep(sleep)
cout2(label)

This allows a process to be modelled which can take significantly
longer to complete it's first event. If I set up the processes as
such:

Parallel(
eventProcess(w.reader(), 'w'), eventProcess(x.reader(), 'x'),
eventProcess(y.reader(), 'y'), eventProcess(z.reader(), 'z'),
actionProcess(w.writer(), z.writer(), 'A'),
actionProcess(x.writer(), z.writer(), 'B'),

actionProcess(y.writer(), z.writer(), 'C', 5) # note that process C
sleeps for 5 seconds between the y and z events
)
i.e. the processes 'A' and 'B' run a lot faster than 'C', then we can
see that rather than synchronizing on event z (or participating in it
at the same time), processes 'A' and 'B' just keep looping through,
ignoring the fact that 'C' has not reached z yet. If I filter the
output to just include processes A and C, we get:

eventP(w):A
eventP(y):C
eventP(z):A
eventP(w):A
eventP(z):A

This shows that process A keeps cycling in spite of C. In this
situation, how can I make both processes A and B wait until C is ready
to participate in z?

Thanks for your continued help, I really appreciate it :)

Andy

[Rune Møllegaard Friborg]

Hi Andy,

Then, I think it is something similar to a barrier you are seeking.

This can be implemented using a barrier process.

@process
def Barrier(nprocesses, signalIN, signalOUT):
while True:
for i in range (nprocesses):
signalIN()
for i in range (nprocesses):
signalOUT(0)

But, I believe the formal semantics is different, from the lines you wrote.

Perhaps, someone can add this?

- Rune