Simulating Truly Concurrent CSP - Formal Methods: Foundations and Applications - page 139

6.2 One-Place Buffer

A specification of a one-place buffer is

COPY = left ? x → right ! x → COPY .

The implementation ( SYSTEM ) presented in [3] is proved to be equivalent (in
the failures-divergences model) to that specification. Since it uses parallel compo-
sition, it is of interest to check whether or not there are actually any concurrent
events in the implementation; there might be concurrent τ events at least. There
are no concurrent events in the implementation if the bag never grows beyond
size one. This property can be built into the controller by modifying it as follows.

C 2 ( X )=# X < 2&( s ? x → C 2 ( X [[ x ]])

→

sh ? x C 2 ( X [[ x ]] )

→

C 2 ( X ∪

[[ x ]] )
eh ? x → C 2 ( X ∪

e ? x

[[ x ]] )

term → SKIP )

Checking Hr (( T ( SYSTEM ); term C 2 ([[]])) = T COPY with

FDR proves that there are no concurrent events in the implementation.

→ SKIP ) | S Con |

6.3 Dining Philosophers

The well-known example of the dining philosophers reveals a disadvantage of our
approach: poor performance within FDR. Indeed the size of the transition system
of the controller grows rapidly. In this example, N is the number of philosophers.
The number of events available is 3 N +2 N 2 . The set of all lists containing event
labels and with maximum length n has i =0 (3 N +2 N 2 ) i elements, which is
20,440 for N =3and n = 3 or 551,881 for N =3and n = 4. Reducing these
sets to create specifications like the one presented in the first example does not
solve this problem. The set of all lists with maximum length n and at most one
renamed eat event in it contains 19,756 elements for N =3and n =3and
517,420 in the case of N =3and n = 4. So checking the assertion that the eat
event never occurs concurrently with another eat event with N =3takesabout
90 minutes.

7 Related and Further Work

The work reported here relates particularly to other approaches to 'non inter-
leaving' or 'truly concurrent' semantics of process algebra. In particular, it has
been influenced by the work of Kwiatkowska and Phillips [7] and Taubner and
Vogler [12]. In a sense, our approach combines the two by simulating the concur-
rency relation developed in the former, while maintaining the concurrent events
in a structure that generalizes the steps defined in the latter.