-
Notifications
You must be signed in to change notification settings - Fork 0
/
as5_phil.pj
147 lines (135 loc) · 5.34 KB
/
as5_phil.pj
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
import std.*;
const int MAX = 5;
// void philosopher(int id, chan<boolean>.write left, chan<boolean>.write right) {
// while (true) {
// println(id + ": I am thinking");
// par { // pick up forks
// left.write(true);
// right.write(true);
// }
// println(id + ": I am eating");
// par { // put down forks
// left.write(true);
// right.write(true);
// }
// }
// }
// fork is a reserved word for now, so use Fork
void Fork(int i, chan<boolean>.read left, chan<boolean>.read right) {
boolean any;
while (true) {
alt {
//right phil picks up
any = left.read(): { // This corresponds to forks_direction.left in FDR
println(i + ": picked up from the right."); // This corresponds to forks_motion.up in FDR
any = left.read(); // right phil puts down
println(i + ": put down from the right."); // This corresponds to forks_motion.down in FDR
}
// left phil picks up
any = right.read(): {
println(i + ": picked up from the left."); // This corresponds to forks_motion.up in FDR
any = right.read(); // left phil puts down
println(i + ": put down from the left."); // This corresponds to forks_motion.down in FDR
}
}
}
}
// void college() {
// // I handcoded this for you - I didn't check I got
// // it right, so you may wanna check that yourself ;-)
// chan<boolean> left0, left1, left2, left3, left4;
// chan<boolean> right0, right1, right2, right3, right4;
// par {
// philosopher(0, left0.write, right0.write);
// philosopher(1, left1.write, right1.write);
// philosopher(2, left2.write, right2.write);
// philosopher(3, left3.write, right3.write);
// philosopher(4, left4.write, right4.write);
// Fork(0, left0.read, right1.read);
// Fork(1, left1.read, right2.read);
// Fork(1, left2.read, right3.read);
// Fork(1, left3.read, right4.read);
// Fork(2, left4.read, right0.read);
// }
// }
void securePhilosopher(int id, chan<boolean>.write left, chan<boolean>.write right,
chan<boolean>.write sitdown, chan<boolean>.write getup) {
while (true) {
println(id + ": I am thinking"); //This corresponds to think.i in FDR
println(id + ": I want to sit down."); //This corresponds to sitdown.i in FDR
// ask to sit down
sitdown.write(true);
par { // pick up forks
left.write(true);
right.write(true);
}
println(id + ": I am eating"); //This corresponds to eat.i in FDR
par { // put down forks
left.write(true);
right.write(true);
}
println(id + ": I want to get up."); //This corresponds to getup.i in FDR
// get up
getup.write(true);
}
}
void security(chan<boolean>.read[] up, chan<boolean>.read[] down) {
// up.length does not cause an error!
const int maxSatDown = up.size - 1;
int satDown = 0;
boolean any;
while (true) {
println("Sat Down = " + satDown);
alt {
(satDown < maxSatDown) && any = down[0].read(): satDown = satDown + 1;
(satDown < maxSatDown) && any = down[1].read(): satDown = satDown + 1;
(satDown < maxSatDown) && any = down[2].read(): satDown = satDown + 1;
(satDown < maxSatDown) && any = down[3].read(): satDown = satDown + 1;
(satDown < maxSatDown) && any = down[4].read(): satDown = satDown + 1;
any = up[0].read(): satDown = satDown - 1;
any = up[1].read(): satDown = satDown - 1;
any = up[2].read(): satDown = satDown - 1;
any = up[3].read(): satDown = satDown - 1;
any = up[4].read(): satDown = satDown - 1;
}
}
}
void secureCollege() {
// I handcoded this for you - I didn't check I got
// it right, so you may wanna check that yourself ;-)
chan<boolean> left0, left1, left2, left3, left4;
chan<boolean> right0, right1, right2, right3, right4;
chan<boolean> down0, down1, down2, down3, down4;
chan<boolean> up0, up1, up2, up3, up4;
chan<boolean>.read[] ups = new chan<boolean>.read[5];
chan<boolean>.read[] downs = new chan<boolean>.read[5];
ups[0] = up0.read;
ups[1] = up1.read;
ups[2] = up2.read;
ups[3] = up3.read;
ups[4] = up4.read;
downs[0] = down0.read;
downs[1] = down1.read;
downs[2] = down2.read;
downs[3] = down3.read;
downs[4] = down4.read;
par {
//securePhilosopher(i, left[i].write, right[i].write, down[i].write, up[i].write)
securePhilosopher(0, left0.write, right0.write, down0.write, up0.write);
securePhilosopher(1, left1.write, right1.write, down1.write, up1.write);
securePhilosopher(2, left2.write, right2.write, down2.write, up2.write);
securePhilosopher(3, left3.write, right3.write, down3.write, up3.write);
securePhilosopher(4, left4.write, right4.write, down4.write, up4.write);
// fork(left[i].read, right[(i+1)%max].read);
Fork(0, left0.read, right1.read);
Fork(1, left1.read, right2.read);
Fork(2, left2.read, right3.read);
Fork(3, left3.read, right4.read);
Fork(4, left4.read, right0.read);
security(ups, downs);
}
}
public void main(string args[]) {
//college();
secureCollege();
}