比如传感器的一个什么任务 花了3.8秒， 产生不了迁移。

上面这种有可能系统一直在计算一些个什么任务 ，计算时间不在 条件范围之内，发生死锁

不变式 x<=3 表示系统在loop状态只能持续3个时间单位，，代码执行执行，知道能够在小于=3个时间内结束。

CPS和 RTS的区别

一个路径是一个状态序列

A【】 是所有路径 ，每条路径中的所有状态

A<>所有路径，每条路径至少一个状态

E<> 一条路径一个状态

E[]一条路径所有状态