formal-methods - 形式化方法：[]<> 在 TLA 中无限频繁（总是最终）

Question

根据我对 TLA 的理解，最终的操作 (<>) 不允许在下一个状态下发生口吃。那么，是不是意味着下一个状态变量在无限频繁（[]<>）的情况下是不允许卡顿的呢？

以天气状况为例，无限常常可以描述为一年中最终会有很多天（我们不知道什么时候会发生）会下雨，但下雨天后天气一定是晴天？

我对无限经常的理解是正确的吗？如果我错了，请纠正我。

谢谢你。

Answer 1

该属性[]<> ϕ已通过任何跟踪验证

• 有无限的长度和
• 不验证<>[] ¬ϕ，即没有一个时间点在此之后ϕ是绝对false永远的。

满足的无限迹[] ϕ也满足[]<> ϕ，因为前者比后者强。反之则不一定。

例如

[]<> it_rains_today以下跟踪将满足类似的声明：

• 一丝丝它每天一整天不间断地下雨，直到永远
• 隔天下雨的痕迹，直到永远
• 每 10 年一天下一次雨，直到永远
• 每 1000 万年就下一次雨，直到永远

请注意，此类事件不需要以任何规律发生，只是更容易说出这样的例子。唯一的要求是没有时间点会永远停止下雨。