SMC time-locked；SMC time locked；
    含义：某个location的inv到期时，由于transition的guard或者receiving action的限制，并不能走出该location。

    1. 带inv的location，所有从该location离开的edge都有receiving action。不管能否保证a?能够一定收到a!，都有可能出现time-locked，具体原因可能是UPPAAL check的方法过于简单，就是直接按照receiving action前是否有inv来判断time-locked，而不是尝试运行。

    image.pngimage.png

    • 如上图所示，在进行如下模拟时UPPAAL在0时刻就对该模型检测出time-locked问题。

    simulate [<=100; 100] {Receiver.S1}

    • 如果将S0的invariant删除，或者添加一个从S0—>S1的空白transition，那么该模拟可以正常运行，但是模型仍然存在deadlock的问题。
    • 案例文件：time-locked1.xml。
      1. 带Urgent或者Committed的location，所有从该location离开的edge都有receiving action。这两种location相当于加了inv。
      2. deadlock会导致time-locked或者sanity problem，因此跑SMC前也要检查deadlock的情况。