Как выполнить исчерпывающую проверку состояния в 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)