Формальный метод: []‹› Бесконечно часто (Всегда в конце концов) в TLA

Насколько я понимаю, в TLA возможное действие (‹>) не позволяет заиканию произойти в следующем состоянии. Значит ли это, что следующая переменная состояния не может заикаться в случае бесконечно часто ([]‹>)?

Возьмем в качестве примера погодные условия, которые бесконечно часто можно описать так: в конце концов, много дней в году (мы не знаем, когда это произойдет) будет идти дождь, но после дождливого дня должна быть солнечная погода?

Верно ли мое понимание бесконечно часто? Поправьте меня, если я ошибаюсь.

Спасибо.


formal-methods
person Ng Yk    schedule 13.12.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Свойство []<> ϕ проверяется любой трассировкой, которая

  • имеет бесконечную длину и
  • не проверяет <>[] ¬ϕ, т. е. нет момента времени, после которого ϕ окончательно становится false навсегда

Бесконечная трасса, удовлетворяющая [] ϕ, также удовлетворяет []<> ϕ, поскольку первое сильнее второго. Обратное не обязательно имеет место.

например

Такой оператор, как []<> it_rains_today, будет удовлетворяться следующими трассировками:

  • След с.т. непрерывно идет дождь каждый день весь день, на всю вечность
  • След с.т. дождь идет через день, целую вечность
  • След с.т. дождь идет один день каждые 10 лет, на всю вечность
  • След с.т. дождь идет один день каждые 10 миллионов лет, на всю вечность

Обратите внимание, что нет никаких требований, чтобы такое событие происходило с какой-либо регулярностью, просто проще сформулировать такие примеры. Единственное требование состоит в том, что не существует временного момента, после которого дождь полностью прекращается навсегда.

person Patrick Trentin    schedule 13.12.2017
comment
A trace s.t. it uninterruptedly rains every day all day, for all eternity Разве это не означает, что дождь идет вечно? И разве это предполагаемое состояние не принадлежит []<> it_rains_today? - person Ng Yk; 14.12.2017
comment
@NgYk Это именно то, что это значит. Бесконечная трасса, удовлетворяющая [] ϕ, также удовлетворяет []<> ϕ, поскольку первое сильнее второго. Обратное не обязательно имеет место. - person Patrick Trentin; 14.12.2017