Dining Philosophers Clause Samples

Dining Philosophers. ‌ BRIC This case study is the asymmetric dining philosophers. In this case study, philosophers try to acquire a pair of shared forks in order to eat. The philoso- phers are sat in a table and there is a fork between each pair of philosophers. The random acquisition of the forks by the philosophers might lead to a deadlock, but in the asymmetric version, the order of acquisition of forks prevents deadlocks. In this section, we introduce a CML model for the forks and philosophers, and we demonstrate how to use to compose these components so as to create the asymmetric dining philosophers settings. Firstly, we introduce some global variable, or, as the CML terminology de- fines, values, that are useful for parametrising our model. The value N gives the number of philosophers, or forks, in our model. Hence, if N = 3 then we have three forks and three philosophers in our model. The value RANGE_SET gives a set of natural numbers that distinguishes the philosophers one from the other. The same set is used for distinguishing forks. values N : nat = 3 RANGE_SET : set of nat = {0,...,(N-1)} Next, we introduce the types used in our model. The RANGE type consists of the set of natural numbers such that its elements belong to the RANGE_SET value. The enumerated type REQUISITION gives the possible uses of a com- munication channel. The <req> states that an action is being requested by the channel, whereas the <ack> is used to acknowledge that an action has been performed. The enumerated type S_ACTION (S stands for Shared) gives the actions performed by forks and philosophers, which require interaction between them. The enumerated type I_ACTION (I stands for Individual) gives the actions performed by a philosopher that do not require interaction, i. e. individual tasks performed by the philosopher. types RANGE = nat inv n == n in set RANGE_SET REQUISITION = <req> | <ack> S_ACTION = <picksup> | <putsdown> I_ACTION = <eats> | <getsup> | <sitsdown> Moving forward, we introduce the channels used in our model. The channel pfk is used by the philosophers to perform interacting actions with forks. The channel fk is used by the forks to perfom actions that require interaction with philosophers. Lastly, the life channel is used by the philosophers to state which individual action they are doing. channels pfk : RANGE * RANGE * S_ACTION * REQUISITION fk : RANGE * RANGE * S_ACTION * REQUISITION life : RANGE * I_ACTION Additionally, some functions that are useful in the description o...