// the number of philosophers #define N 2 // the number of available tokens and the states of the forks byte c = N-1; bool f[N] = true; mtype = { GET, PUT }; // the channels between the philosophers and the coin pool chan crequest[N] = [1] of { mtype }; chan creply[N] = [1] of { mtype }; // the channels between the philosophers and the forks chan frequest[2*N] = [1] of { mtype }; chan freply[2*N] = [1] of { mtype }; // select a request channel i suitable for coin number c // (continues running, until such a channel is available) inline selectRequest(i, c) { select (i : 0..(N-1)); do :: c == 0 && crequest[i] ? [ PUT ] -> break; :: c > 0 && len(crequest[i]) > 0 -> break; :: else -> i = (i == N-1 -> 0 : i+1); od; } // the pool of coins proctype coins() { byte i; do :: true -> selectRequest(i, c); if :: crequest[i] ? GET -> c = c-1; creply[i] ! GET; :: crequest[i] ? PUT -> c = c+1; fi; od; } // fork i proctype fork(byte i) { skip; } // philosopher i proctype philosopher(byte i) { eating: skip; } // create N philosophers and N forks and 1 coin pool init { atomic { byte i = 0; do :: i < N -> run philosopher(i); run fork(i); i = i+1; :: else -> break; od; run coins(); } }