-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPHILOSOPHERS_0_UNFAIR_N5.lnt
324 lines (245 loc) · 8.98 KB
/
PHILOSOPHERS_0_UNFAIR_N5.lnt
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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
module PHILOSOPHERS_0_UNFAIR_N5 is
function BOUND:Nat is return 0 end function
function DISABLELSTIG:Nat is return 1 end function
function MAXCOMPONENTS:Nat is return 5 end function
function MAXKEYE:Nat is return 5 end function
function MAXKEYI:Nat is return 1 end function
function MAXKEYL:Nat is return 1 end function
function MAXPC:Nat is return 1 end function
function MAXTUPLE:Nat is return 1 end function
function undef_value:Int is return -128 end function
type ID is X:Nat where X < MAXCOMPONENTS with "==", "!=" end type
type PC is array [ 0 .. 0 ] of Nat end type
type Iface is array [ 0 .. 0 ] of Int with "get", "set" end type
channel IdChannel is (ID) end channel
channel Boolch is (Bool) end channel
type Env is array [ 0 .. 4 ] of Int with "get", "set" end type
process env [action: Any] (in out E:Env, key:Int, val:Int) is
E[IntToNat(key)] := val;
action("E", key, val)
end process
type Agent is agent(id: ID, I: Iface, init:Bool, pc:PC) with "get", "set" end type
type Agents is array [ 0 .. 4 ] of Agent with "get", "set" end type
type Sys is sys(agents: Agents,env: Env) with "get", "set" end type
function emptyAgent: Agent is
return Agent(ID(0), Iface(0), false, PC(0))
end function
process attr [action: Any] (in out a:Agent, key:Nat, val:Int) is
var Inew: Iface in
Inew := a.I;
Inew[key] := val;
a := a.{I => Inew}
end var;
action("I", a.id, key, val)
end process
process INITAGENT (in out a:Agent) is
var I:Iface, x: Int, p:PC in
I := a.I;
p := a.pc;
if (Nat(a.id) >= 0) and (Nat(a.id) < 5) then
p[0] := 9;
x := any Int where (((x) == ((0 of Int))));
I[0] := x
end if;
a := a.{I => I, init => true, pc => p}
end var
end process
process INITENV(in out e: Env) is
var x: Int in
x := any Int where (((x) == ((0 of Int))));
e[0] := x;
x := any Int where (((x) == ((0 of Int))));
e[1] := x;
x := any Int where (((x) == ((0 of Int))));
e[2] := x;
x := any Int where (((x) == ((0 of Int))));
e[3] := x;
x := any Int where (((x) == ((0 of Int))));
e[4] := x end var
end process
process action_0_2 [action: Any] (in out agent: Agent, in out E: Env) is
--(status, 0) <- 0
attr[action](!?agent, 0, (0 of Int));
var p: PC in
p := agent.pc;
p[0] := 9;
agent := agent.{pc => p}
end var
end process
process action_0_3 [action: Any] (in out agent: Agent, in out E: Env) is
--(fork, 0)[id] <-- 0
env[action](!?E, 0 + (NatToInt(Nat(agent.id)) of Int), (0 of Int));
var p: PC in
p := agent.pc;
p[0] := 2;
agent := agent.{pc => p}
end var
end process
process action_0_4 [action: Any] (in out agent: Agent, in out E: Env) is
--(status, 0) <- 3
attr[action](!?agent, 0, (3 of Int));
var p: PC in
p := agent.pc;
p[0] := 3;
agent := agent.{pc => p}
end var
end process
process action_0_5 [action: Any] (in out agent: Agent, in out E: Env) is
--(fork, 0)[id + 1 % 5] <-- 0
env[action](!?E, 0 + (((NatToInt(Nat(agent.id)) of Int)) + ((1 of Int))) mod ((5 of Int)), (0 of Int));
var p: PC in
p := agent.pc;
p[0] := 4;
agent := agent.{pc => p}
end var
end process
process action_0_6 [action: Any] (in out agent: Agent, in out E: Env) is
--(status, 0) <- 2
attr[action](!?agent, 0, (2 of Int));
var p: PC in
p := agent.pc;
p[0] := 5;
agent := agent.{pc => p}
end var
end process
process action_0_7 [action: Any] (in out agent: Agent, in out E: Env) is
--((fork, 0)[id + 1 % 5]) == (0)->(fork, 0)[id + 1 % 5] <-- 1
env[action](!?E, 0 + (((NatToInt(Nat(agent.id)) of Int)) + ((1 of Int))) mod ((5 of Int)), (1 of Int));
var p: PC in
p := agent.pc;
p[0] := 6;
agent := agent.{pc => p}
end var
end process
process action_0_8 [action: Any] (in out agent: Agent, in out E: Env) is
--(status, 0) <- 1
attr[action](!?agent, 0, (1 of Int));
var p: PC in
p := agent.pc;
p[0] := 7;
agent := agent.{pc => p}
end var
end process
process action_0_9 [action: Any] (in out agent: Agent, in out E: Env) is
--((fork, 0)[id]) == (0)->(fork, 0)[id] <-- 1
env[action](!?E, 0 + (NatToInt(Nat(agent.id)) of Int), (1 of Int));
var p: PC in
p := agent.pc;
p[0] := 8;
agent := agent.{pc => p}
end var
end process
process lastAgent [last: IdChannel] is
var tid: ID in
tid := 0;
loop
last(tid);
last(?tid)
end loop
end var
end process
process step [last: IdChannel, mon, action: Any] (in out sys: Sys) is
var a:Agent, tid:ID, agents:Agents, firstAgent: Int, E: Env in
agents := sys.agents;
last(?tid);
action(tid);
a := agents[Nat(tid)];
if (a.init == false) then INITAGENT(!?a); action(a) end if;
E := sys.env;
if canProceed(a, sys.env) then
firstAgent := NatToInt(Nat(tid));
select
only if (a.pc[0] == 2) then action_0_2[action](!?a, !?e) end if
[]
only if (a.pc[0] == 3) then action_0_3[action](!?a, !?e) end if
[]
only if (a.pc[0] == 4) then action_0_4[action](!?a, !?e) end if
[]
only if (a.pc[0] == 5) then action_0_5[action](!?a, !?e) end if
[]
only if (a.pc[0] == 6) then action_0_6[action](!?a, !?e) end if
[]
only if (a.pc[0] == 7) and ((E[IntToNat(0 + (((firstAgent of Int)) + ((1 of Int))) mod ((5 of Int)))]) == ((0 of Int))) then action_0_7[action](!?a, !?e) end if
[]
only if (a.pc[0] == 8) then action_0_8[action](!?a, !?e) end if
[]
only if (a.pc[0] == 9) and ((E[IntToNat(0 + (firstAgent of Int))]) == ((0 of Int))) then action_0_9[action](!?a, !?e) end if
end select
end if;
agents[Nat(tid)] := a;
sys := sys.{ agents => agents, env => e};
--- scheduler ---
tid := any ID;
last(tid) -- store tid for later retrieval
--- end scheduler ---
end var
end process
process monitor [mon: any] (agents: Agents) is
if(agents[0].init) and (agents[1].init) and (agents[2].init) and (agents[3].init) and (agents[4].init) then
-- P1
if not((((agents[0].I[IntToNat(0)]) != ((1 of Int)))) or (((agents[1].I[IntToNat(0)]) != ((1 of Int)))) or (((agents[2].I[IntToNat(0)]) != ((1 of Int)))) or (((agents[3].I[IntToNat(0)]) != ((1 of Int)))) or (((agents[4].I[IntToNat(0)]) != ((1 of Int))))) then mon(false); stop end if
end if
end process
function canProceed(a: Agent, E: Env): Bool is
var firstAgent: Int in
firstAgent := NatToInt(Nat(a.id));
return
(
((a.pc[0] == 2))
or
((a.pc[0] == 3))
or
((a.pc[0] == 4))
or
((a.pc[0] == 5))
or
((a.pc[0] == 6))
or
((a.pc[0] == 7) and ((E[IntToNat(0 + (((firstAgent of Int)) + ((1 of Int))) mod ((5 of Int)))]) == ((0 of Int))))
or
((a.pc[0] == 8))
or
((a.pc[0] == 9) and ((E[IntToNat(0 + (firstAgent of Int))]) == ((0 of Int))))
)
end var
end function
function existsEnabledAgent (sys: Sys): Bool is
var n: Nat in
for n := 0 while (n < MAXCOMPONENTS) by n := n + 1 loop
if not(sys.agents[n].init) or canProceed(sys.agents[n], sys.env) then
return true
end if
end loop;
return false
end var
end function
process MAIN [monitor, action: Any] is
var sys: Sys, agents: Agents, e:Env in
agents := Agents(emptyAgent);
var tid: Nat, a: Agent in
for tid := 0 while tid < MAXCOMPONENTS by tid := tid + 1 loop
a := agents[tid].{id => ID(tid)};
INITAGENT(!?a);
agents[tid] := a; action(a)
end loop;
e := Env(0);
INITENV(!?e);
action(e);
sys := Sys(agents, e)
end var;
hide last:IdChannel in
par last in
lastAgent [last]
||
loop
monitor[monitor](sys.agents);
if not(existsEnabledAgent(sys)) then
monitor("deadlock"); stop
end if;
step[last, monitor, action](!?sys)
end loop
end par
end hide
end var
end process
end module