求哲学家吃饭问题源代码

husterUID: 2110691

RT

Lyon_TonyUID: 178961

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)

husterUID: 2110691

谢谢tony

但是有的地方看不懂，能否大致说说思路？

Lyon_TonyUID: 178961

看这里

http://www.cs.mtu.edu/~shene/NSF ... ample-philos-1.html

husterUID: 2110691

谢！

hakeemchoiUID: 193092

靠　什么乱七八糟　呵呵

nmlyUID: 109487

funny codes...heihei

jorgeUID: 108878

为什么每次看到代码..还是会有点激动呢...

foolboy007UID: 28322

现在看到代码就头晕

husterUID: 2110691

学IT的就是累