grape: allow or-communication of channels

mCRL2org / mCRL2

The Git repository for the mCRL2 toolset.

https://mcrl2.org/

Boost Software License 1.0

88 stars 37 forks source link

grape: allow or-communication of channels #462

Closed jgroote closed 12 years ago

jgroote commented 16 years ago

Issue migrated from trac ticket # 460

component: grapemcrl2 | priority: minor | resolution: wontfix

2008-09-01 16:44:40: A.H.J.Mathijssen@tue.nl created the issue

In grape it is currently only possible to express an and-communication between multiple channels (by means of a multi-party communication), but it is impossible to express an or-communication between multiple channels. Or-communication is essential for specifications in which an action of a process P might communicate with an action of precisely one of the processes Q0,...,Qn. For instance, in the dining philosophers protocol, a philosophers communicates with either its left-hand side fork or its right-hand side fork.

In the interface, the possibility of or-communication can be enabled by allowing more than one communication line to be attached to a single channel of a process/architecture reference.

jgroote commented 16 years ago