[未归类] 求哲学家吃饭问题源代码 [复制链接]

huster
UID: 2110691

荣誉版主

Rank: 9 Rank: 9 Rank: 9

声望: 205
寄托币: 40936
注册时间: 2005-6-24
精华: 21
帖子: 270

电梯直达

楼主

发表于 2006-11-3 14:10:10 |只看该作者 |倒序浏览

寄托领跑四六级

0 0

使用道具举报

Lyon_Tony
UID: 178961

元老版主

Rank: 11

声望: 46
寄托币: 46892
注册时间: 2004-9-17
精华: 52
帖子: 507

沙发

发表于 2006-11-3 14:41:01 |只看该作者

program dining
const N=5;
STARVELIMIT=100;
var
starvation.0..0: integer[0];
deadlock.0..0: integer[0];
iter.0..0: integer[0];
fork.1..N: integer [all(, j:1..N | 0)];
want2eat.1..N: integer [all(, j:1..N | 0)];
eat.1..N: integer [all(, j:1..N | 0)];
eatcount.1..N: integer [all(, j:1..N | 0)];
process
p: 1..N
actions
-- Philosopher decides he wants to eat
(want2eat.p == 0) and
(fork.(1 + ((p+N-1) mod N)) == 0) and
(fork.(1 + (p mod N)) == 0)
-> iter.0:= iter.0+ 1;
   want2eat.p := iter.0
[]
-- Philosopher can pick up left fork
(want2eat.p > 0) and
(fork.(1 + ((p+N-1) mod N)) == 0)
-> fork.(1 + ((p+N-1) mod N)) := p;
   iter.0:= iter.0+ 1
[]

-- Philosopher can pick up right fork
(want2eat.p > 0) and
(fork.(1 + (p mod N)) == 0)
-> fork.(1 + (p mod N)) := p;
   iter.0:= iter.0+ 1
[]
-- Philosopher starts eating
(want2eat.p > 0) and
(eat.p == 0) and
(fork.(1 + ((p+N-1) mod N)) == p) and
(fork.(1 + (p mod N)) == p)
-> eat.p := 1;
   eatcount.p := eatcount.p + 1;
   iter.0:= iter.0+ 1
[]
-- Philosopher decides to stop eating
(eat.p == 1) and
(want2eat.p > 0)
-> want2eat.p := 0;
   iter.0:= iter.0+ 1
[]
-- Philosopher stops eating and lays down forks
(eat.p == 1) and
(want2eat.p == 0)
-> eat.p := 0;
   fork.(1 + ((p+N-1) mod N)) := 0;
   fork.(1 + (p mod N)) := 0;
   iter.0:= iter.0+ 1
[]

-- Deadlock occurs when everybody wants to eat and everybody
-- holds one and only one fork.
(all (and j:1..N | (
  (want2eat.j > 0) and
  (
((fork.(1 + ((j+N-1) mod N)) == j) and (fork.(1 + (j mod N)) != j)
   and (fork.(1 + (j mod N)) != 0)) or
   ((fork.(1 + (j mod N)) == j) and (fork.(1 + ((j+N-1) mod N)) != j)
   and (fork.(1 + ((j+N-1) mod N)) != 0))
)
)
  )
)
-> deadlock.0 := 1;
   iter.0:= iter.0+ 1
[]

-- Starvation occurs when some philosopher has wanted to eat for
-- too many iterations
(want2eat.p > 0) and
(iter.0 > (want2eat.p + STARVELIMIT))
-> starvation.0 := p;
   iter.0 := iter.0 + 1
topology 5 ring
semantics interleaving
invariant
(deadlock.0 == 0) and
(starvation.0 == 0)

An opportunity is never lost but missed,
an opportunity missed is never lost but found by others.

双非DIY美硕申请总结

使用道具举报