哲学家就餐问题
问题描述：
    有五位哲学家围绕着餐桌坐，每一位哲学家要么思考要么等待，要么吃饭。为了吃饭，哲学家必须拿起两双筷子（分别放于左右两端）不幸的是，筷子的数量和哲学家相等，所以每只筷子必须由两位哲学家共享。
建模：
    有五个哲学家，分别用phil1，phil2，phil3，phil4，phil5表示，每个哲学家的状态有{thinking，waiting，eating}。
    五只筷子，分别用chopstick1，chopstick2，chopstick3，chopstick4，chopstick5表示。

要验证的PPTL性质：
1.[](phil1.state=waiting -><>phil1.state=eating)
含义：总是存在如果哲学家1处于等待状态，那么未来某个状态就会处于吃饭状态。
模型不满足该性质：因为系统可能发生死锁，哲学家一个永远处于等待状态。

2.[](phil1.state=eating -> (chopstick1=1 && chopstick2=1)  )
含义：总是存在如果哲学家1处于吃饭状态那么他一定拿了左筷子和右筷子。
模型满足该性质：因为哲学家1只有拿起了左筷子和右筷子之后才会处于吃饭状态。