model-verification-dining-philosophers-problem/dining_philosophers_problem.pml at main · pieterjansevanrensburg/model-verification-dining-philosophers-problem · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
/*
This program seeks to solve the generalized dining philosophers' problem
using channels.

It is my implementation of the Resource Hierarchy Solution proposed by
Edsger W. Dijkstra (Wikipedia contributors, 2021).

This solution involves assigning a partial order to the forks and requires that
the forks' availability be checked with respect to said ordering i.e.
philosophers always checks lower ordered forks first and then higher
ordered forks (Wikipedia contributors, 2021).

The partial ordering is simply each fork's position in the array of
asynchronous channels.

Furthermore, each philosopher is treated as a seperate process that runs in
parallel (Wikipedia contributors, 2021).


Wikipedia contributors. (2021, March 8). Dining philosophers problem.
In Wikipedia, The Free Encyclopedia. Retrieved 18:18, March 28, 2021,
from https://en.wikipedia.org/w/index.php?title=Dining_philosophers_problem&oldid=1011067127
*/

/*
The total number of philophers (and forks) to consider in this problem.
*/
#define number_of_philosophers 5

/*
An array of asynchronous channels, where each channel represents a fork.
The indices of the array indicate the forks' assigned partial ordering.
*/
chan forks[number_of_philosophers] = [1] of {bool};

/*
A process representing a philosopher. It's parameters are as follows:
	lower_index_fork: A reference to a channel which represents the fork
	adjacent to the philosopher that has the lower array index
	(i.e. lower partial ordering).
	higher_index_fork: A reference to a channel which represents the fork
	adjacent to the philosopher that has the higher array index
	(i.e. higher partial ordering).
*/
proctype philosopher(chan lower_index_fork; chan higher_index_fork) {
	bool get;
	do 	::	true ->
		/*
		The philosopher tries to get the forks adjacent to them according to
		their partial ordering (lower index is checked first and then
		higher index).
		*/
		lower_index_fork?get;
		higher_index_fork?get;
		/*
		Now that the philosopher has both forks adjacent to them, they can
		eat.
		*/
		printf("philosopher %d is eating.", _pid)
		/*
		The philosopher releases the forks as they are done eating.
		*/
		higher_index_fork!get;
		lower_index_fork!get;
	od
}

init {
	/*
	Make all the forks available to the philosophers.
	*/
	int index = 0;
	do	::	index < number_of_philosophers -> forks[index]!true; index++;
		:: 	else -> break;
	od
	/*
	Start all philosopher processes at the same time.
	*/
	index = 0;
	atomic{
		do 	:: 	index < number_of_philosophers ->
				/*
				Note that we assign a partial ordering to the forks
				based on their positions in the array.

				This is done by simply assigning forks to philosophers in an
				ascending order, except for the final philosopher where the
				first fork in the array is assigned as their lower index fork
				and the higher index fork is the final fork in the array.
				*/
				if	:: 	index == (number_of_philosophers - 1) ->
						run philosopher(forks[0], forks[index]);
					:: 	else ->
						run philosopher(forks[index], forks[index + 1]);
				fi
				index++;
			:: else -> break;
		od
	}
}