实验三

fig5

A[] Obs.taken imply x >=2 表示对于所有路径，x >=2时，迁移到状态taken一定会发生

E<> Obs.idle and x > 3表示存在一条路径，x>3时，迁移到idle状态

fig6

guard : x >= 2

invariant: x <=3

fig7

guard ： x>=2 and x<=3

no invariant.

• x > 3时发生dead lock，迁移不再发生.

总结：

位置不变量的含义：是一个进阶条件，在设置了位置不变量条件的状态下，变量必须满足指定的条件。

也就是在fig6中，loop状态下，clock x的值不允许超过3个时间单元