tla+ - 如何在 TLA+ 中执行详尽的状态检查？

Question

是否可以检查模型中的每个合法状态是否已达到？如果可能的话，该属性应该如何写？

考虑下面调制 24 小时时钟的模块。我可以检查它hour是否处于非法状态，即它在 0 到 23 之间。但是如果我写了一个错误的Next谓词，例如hour' = (hour + 1) % 23，不是所有状态都达到了，但属性不会捕获这个错误。

----------------------------- MODULE Clock -----------------------------
EXTENDS Naturals
VARIABLE hour

Init ==
    hour \in 0..23

Next == 
    hour' = (hour + 1) % 24

Spec == 
    /\ Init
    /\ [][Next]_hour

\* Properties
hourMinBound == [](hour >= 0)
hourMaxBound == [](hour <= 23)
=============================================================================

Answer 1

尝试

ReachesAllStates == \A h \in 0..23: <>(hour = h)

这将检查它是否至少到达每个状态一次。要检查它是否不断到达每个状态，您需要

KeepsReachingAllStates == \A h \in 0..23: []<>(hour = h)