UPPAAL SMC 报错分析；SMC Query Language；SMC 语法； :::success

1. 本文基于uppaal-4.1.24版本，Win10 20H2。
2. 本文适合有SMC基础原理的用户查阅，SMC基础原理请阅读UPPAAL SMC Tutorial (官方教程)。

3. 这里总结软件界面内的操作，命令行操作请阅读UPPAAL 命令行 SMC。 :::

   运行SMC基本要求

   运行SMC最基本的要求：

4. 所有的通信都应该为broadcast channel，不能是channel。在 UPPAAL SMC官方教程 中“Modeling Tricks”章节中有提到如何将channel转化为broadcast channel。

5. 不应该有芝诺行为，即在一个跟时间有关的系统中，如果牵涉到有限时间内，无限多次的操作。(可以模拟但是结果容易没有意义)
6. 不应该有time-locked，详细看下一节“Time-Locked报错分析”。

   1. processes should be able to progress independently: only broadcast synchronization is allowed, the inputs cannot force the outputs.
   2. the system should not contain zeno behavior
   3. the system should not contain timelocks (should not stop time)
   4. the input handling should be deterministic

   参考链接-StackOverflow，顺序有改动。

Query Language

1. simulate [<=T; N] {E1, ..., Ek}

• 功能说明：在T时间内，模拟N次，并且记录E1, ..., Ek的观测。
• 例如：simulate [<=20; 1] {Sender.T0, Receiver.S1}。
• 在UPPAAL右击该语句可以查看分析图像。如下图：

• 注意：Ek可以是某个变量，详细请看 UPPAAL SMC Tutorial (官方教程)。

• 可以使用命令行验证来获取验证结果的具体坐标，参见uppaal 命令行 SMC。

  2. Pr[<=T] (<>psi)

• 功能说明：在T时间内，psi发生的概率是多少。

• 例如：Pr[<=20] (<>Sender.T0)。

• 在UPPAAL右键该语句同样可以查看许多结果，这里就不贴了。

  3. Pr[<=T] (<>psi) >= p

• 功能说明：在T时间内，psi发生的概率大于p的概率是多少。

• 例如：Pr[<=20] (<>Sender.T0) >= 0.1。
• 注意当侧的p的最小值和statistical parameters里的参数有关系。

在报Server exception: Invalid theta-delta的错误时，可以调小参数。

4. Pr[<=T1] (<>psi1) >= Pr[<=T2] (<>psi2)

• 类似3，不写了。

  5. E[<=T; N] (min: expr)和E[<=T; N] (max: expr)

• 暂时没用到，用到再回来写，欢迎学弟学妹们编辑。 :::success 注意在使用2-4模拟语句计算概率时，要注意一个概率论知识：在连续的事件上，某个具体的点发生的概率为0。比如在[0, 100]时间段，正好停在50时刻的概率应该为0。这样的话验证的结果就会 <= 0.09，对UPPAAL来说可以认为相当于0，不可能发生。因此可以尝试将问题改为：停在[49, 51]时间段内的概率，这样就能出来合适的结果。
  这个问题在TCPS21论文打算用SMC尝试时发现过，通过改为时间段初步解决，但是结果不是非常理想，至少能用了。 :::

  参考链接

1. UPPAAL SMC Tutorial (官方教程)
2. 多处理器实时系统可调度性分析的UPPAAL模型，注意这篇文章经验2的配图错了，把sa!和a?互换才对。
3. StackOverflow - violates model sanity with transition