Dekker算法
    Dekker互斥算法是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。两个全局共享的状态变量flag[0]和flag[1]，表示临界区状态及哪个进程想要占用临界区，初始值为0。全局共享变量turn（值为1或0）表示能进入临界区的进程序号，初始值任意，一般为0。

要验证的PPTL性质
1.[]!(proc1.st=critical && proc2.st = critical)
含义：总是有进程1 和 进程2 不可能同时处于关键区。
模型满足该性质。

2.[] (proc1.st=entering -> <> proc1.st=critical)
含义：总是有如果进程1尝试进入关键区，那么他在未来某个时刻一定处于关键区。
模型满足该性质。