// The dining philosophers problem in PEPA // Original model due to Hoare, ÒCommunicating sequential processes,Ó // Communications of the ACM, vol. 21, pp. 666Ð677, 1978. // This version from S. Benkirane, // ÒProcess algebra and epidemiology: evaluating the ability of PEPA to describe biological systems,Ó // Ph.D. dissertation, University of Stirling, 2011, draft. // Modified to track starvation in philosophers. // Variable rates n = 5.62; h = 10; e = 10; r = 100; a = 100; // Fixed rates big = 1000000; slow = 0.001; // Philosophers think, get hungry, acquire two forks, eat, then release forks // To avoid deadlock, a single acquired fork may be released. Pthink = (hungry,h).P0; P0 = (acquire,big).P1 + (starve,slow).S; P1 = (acquire,big).Peat + (release,n).P0 + (starve,slow).S1; Peat = (eating,e).PR2; PR2 = (release,r).PR1; PR1 = (release,r).Pthink; S = (idle,slow).S; S1 = (release,r).S; //Forks are a resource, to be acquired Fork_A = (acquire,a).Fork_U; Fork_U = (release,big).Fork_A; (Pthink[20])(Fork_A[15])