Dijkstra的饭桌上的哲学家
FSE
Copyright (C) Microsoft Corporation. All rights reserved.
1 Embedding
这个例子是下面这个名字空间的一部分：
namespace DiningPhilosophers
2 Model
一群哲学家坐在桌边。每人的左边和右边各有一个餐叉。我们用下面这个只有一个域index的结构来定义餐叉：
structure Fork
index as Integer
哲学家被定义成具有唯一的索引，能够反映他们当前所处的状态，以及具有如下两种能力：报告他们是否能够改变状态(canMove)，以及能够执行状态的改变(move)。因为status 可以改变，所以哲学家是class而不是structure。
abstract class Philosopher
var status as State = Thinking
index as Integer
abstract canMove(table as Table) as Boolean
abstract move(table as Table)
为了简单起见，我们假定哲学家具有固定的数量(5个)。
numPhilosophers as Integer = 5
同样，我们有五把餐叉。
numForks as Integer = numPhilosophers
forks as Set of Fork = {Fork(i) | i in {1..numForks}}
哲学家左边的餐叉与哲学家具有相同的索引。哲学家右边的餐叉的索引比哲学家的索引大（是哲学家总数的模）。
left(p as Philosopher) as Fork
return Fork(p.index)
right(p as Philosopher) as Fork
return Fork(p.index mod numPhilosophers + 1)
思考中的哲学家没有餐叉。（谁需要一把餐叉来思考？）思考中的哲学家可能变得饥饿。饥饿的哲学家试图得到他左边的餐叉从而变成“左手拿餐叉的饥饿的哲学家”。但是只拿到一把餐叉是不够的，只有得到两把餐叉哲学家才开始吃东西。 而右边的餐叉只有在没有人用时才能被得到。吃完东西之后，哲学家只有一件事可以做，那就是放下两把餐叉继续思考。所以，一个成功的哲学家吃一次东西的过程是这样的： Thinking -> Hungry -> HungryWithLeftFork -> Eating -> Thinking
enum State
Thinking
Hungry
HungryWithLeftFork
Eating
我们现在为这五位哲学家定义一张桌子：
class Table
philosophers as Set of Philosopher
用一个变量来描述哪把餐叉正被哪个哲学家使用。另一个变量定义了一个正在吃东西的哲学家的集合：
class Table
var holder as Map of Fork to Philosopher = { -> }
var fed as Set of Philosopher = {}
下面的方法描述了哲学家的动作。能够动作的哲学家是随机选取的。如果没有哲学家能够动作，那么一个死锁发生了。
class Table
var stepNo as Integer = 0
[EntryPoint]
Move()
choose phil in philosophers where phil.canMove(me)
phil.move(me)
stepNo := stepNo + 1
EntryPoint使得被标记的方法能够被外部世界调用，例如可以被C#调用。
2.1 Greedy Philosophers
贪婪的哲学家在吃完东西并开始思考之前绝不会放下餐叉，这会导致死锁。
class GreedyPhilosopher extends Philosopher
override move(table as Table)
match status
Thinking : status := Hungry
Hungry : if not (left(me) in table.holder)
table.holder(left(me)) :=
me as Philosopher
status := HungryWithLeftFork
HungryWithLeftFork
: if not (right(me) in table.holder)
table.holder(right(me)) :=
me as Philosopher
status := Eating
add me to table.fed
Eating : remove table.holder(left(me))
remove table.holder(right(me))
status := Thinking
canMove方法指出哲学家是否能够改变状态：
class GreedyPhilosopher
override canMove(table as Table) as Boolean
return status = Thinking
or (status = Hungry and
left(me) notin table.holder)
or (status = HungryWithLeftFork and
right(me) notin table.holder)
or status = Eating
2.2 Generous Philosophers
慷慨的哲学家并不坚持一定要有一个成功的哲学家的生活。在拿到左手的叉子之后，如果发现无法得到右手的餐叉，慷慨的哲学家就会放下左手的餐叉，继续思考一会。因此，如果所有人都是慷慨的哲学家，那么不会有死锁，但是有可能有人饿死。:)
class GenerousPhilosopher extends Philosopher
override move(table as Table)
match status
Thinking : status := Hungry
Hungry : if not (left(me) in table.holder)
table.holder(left(me)) :=
me as Philosopher
status := HungryWithLeftFork
HungryWithLeftFork
: if not (right(me) in table.holder)
table.holder(right(me)) :=
me as Philosopher
status := Eating
add me to table.fed
else
// someone else is holding the
// right fork
// put the left one down and
// try again another time
remove table.holder(left(me))
status := Thinking
Eating : remove table.holder(left(me))
remove table.holder(right(me))
status := Thinking
注意，决定慷慨的哲学家的状态能否改变的条件要比贪婪的哲学家宽松。
class GenerousPhilosopher
override canMove(table as Table) as Boolean
return status = Thinking
or (status = Hungry and
left(me) notin table.holder)
or status = HungryWithLeftFork
or status = Eating
3 Providing the View
我们提供两个方法来初始化，一个初始化贪婪的哲学家，另一个初始化慷慨的哲学家。
class Table
[EntryPoint]
shared InitGreedy() as Table
philosophers = { new GreedyPhilosopher(i) as Philosopher |
i in [1..numPhilosophers] }
return new Table(philosophers)
[EntryPoint]
shared InitGenerous() as Table
philosophers = { new GenerousPhilosopher(i) as Philosopher |
i in [1..numPhilosophers] }
return new Table(philosophers)
给出哲学家的索引，下面的方法将指出该哲学家拿有餐叉，以及是否正在吃东西。
class Table
HoldsLeft(pIndex as Integer) as Boolean
return exists (i,p) in holder where p.index = pIndex and
left(p) = i
HoldsRight(pIndex as Integer) as Boolean
return exists (i,p) in holder where p.index = pIndex and
right(p) = i
IsFeeded(pIndex as Integer) as Boolean
return exists p in fed where p.index = pIndex
IsDeadlock() as Boolean
return forall p in philosophers holds not p.canMove(me)
IsGreedy() as Boolean
return exists p in philosophers where p is GreedyPhilosopher
StepNo() as Integer
return stepNo
本类阅读TOP10