Указание жизнеспособности, чтобы цикл не происходил в TLA +

Я пишу спецификацию простого взаимодействия клиент-сервер для изучения TLA +:

-------------------------------- MODULE Bar --------------------------------
VARIABLES
    sessionOK, \* if session is OK or expired
    msg        \* message currently on the wire

vars == <<msg, sessionOK>>

TypeOK ==
    /\ sessionOK \in {TRUE, FALSE}
    /\ msg \in {
         "Query",
         "OK",
         "Unauthorized",
         "null"
       }

Init ==
    /\ msg = "null"
    /\ sessionOK = FALSE

Query ==
    /\ msg \in {"null", "OK"}
    /\ msg' = "Query"
    /\ UNCHANGED <<sessionOK>>

OK ==
    /\ msg = "Query"
    /\ sessionOK = TRUE
    /\ msg' = "OK"
    /\ UNCHANGED <<sessionOK>>

Unauthorized ==
    /\ msg = "Query"
    /\ sessionOK = FALSE
    /\ msg' = "Unauthorized"
    /\ UNCHANGED <<sessionOK>>

Authorize ==
    /\ msg = "Unauthorized"
    /\ msg' = "null"
    /\ sessionOK' = TRUE

Expire ==
    /\ sessionOK = TRUE
    /\ sessionOK' = FALSE
    /\ UNCHANGED <<msg>>

Next ==
    \/ Query
    \/ Unauthorized
    \/ OK
    \/ Authorize
    \/ Expire

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

=============================================================================

Как вы можете надеяться, клиент может выполнить некоторый запрос к серверу, и если сеанс в порядке, он получит результат, в противном случае он получит сообщение, которое ему необходимо авторизовать, а затем повторить попытку. Сессия может истечь в любой момент.

Я хочу быть уверенным, что клиент в конечном итоге получит результат, поэтому я добавил эту строку в свойства:

(msg = "Query") ~> (msg = "OK")

После проверки модели я сталкиваюсь с контрпримером, подобным этому: Init -> (Query -> Unauthorized -> Authorize -> Expire), где часть в круглых скобках повторяется бесконечно. Моей первой мыслью было сделать жесткое требование справедливости на OK шаге. Однако проблема в том, что в этом сценарии OK шаг никогда не включается.

Я мог бы добавить такие вещи, как []<><<OK>>_vars (который гласит: «Всегда бывает, что в конечном итоге OK происходит»), но это похоже на обман, и, судя по тому, что я понял, определение живучести с использованием произвольных временных формул - а не слабой или сильной справедливости - нахмурилось на.

Как я могу использовать слабую или сильную справедливость, чтобы гарантировать, что запрос в конечном итоге получит ответ? А может у меня модель плохая? У меня нет идей ...


tla+
person urxvtcd    schedule 15.03.2020    source источник
comment
Как OK должно случиться? Не похоже, что это часть Next.   -  person Hovercouch    schedule 16.03.2020
comment
Ах, моя беда, должно быть, ошиблась при подготовке минимального примера. Исправлю через минуту.   -  person urxvtcd    schedule 16.03.2020
comment
Если OK нельзя включить, это похоже на проблему дизайна. Вы пытаетесь сказать, что если тайм-аут не истечет, то со временем все будет в порядке?   -  person Hovercouch    schedule 17.03.2020
comment
Да, точно. В реальном мире, если клиент получает сообщение Unauthorized, он возобновляет сеанс и немедленно повторяет попытку, а время, необходимое для повторной попытки, на порядки меньше, чем время жизни сеанса, поэтому это не проблема. Но я не знаю, как это смоделировать.   -  person urxvtcd    schedule 18.03.2020
comment
Думаю, я понял это после прочтения этой ветки groups.google.com/ forum / #! topic / tlaplus / 7KLn9O-rwPo, где, как указывает сам Лези Лэмпорт, мы можем использовать соединение в НФ. Собственностью сейчас доволен. Spec == /\ Init /\ [][Next]_vars /\ WF_vars(Next) /\ SF_vars(OK) /\ SF_vars(Query /\ (sessionOK = TRUE)) Как вы думаете, это нормально?   -  person urxvtcd    schedule 18.03.2020

Ответы (1)


arrow_upward
1
arrow_downward

Я отвечаю на свой вопрос. Если кто-то думает, что у него есть лучший ответ, поделитесь, пожалуйста.

Я нашел этот поток с подходящим названием Как проверить, что процесс в конечном итоге завершится успешно после неопределенного количество повторных попыток?, где, как указывает сам Лесли Лэмпорт, мы можем просто утверждать справедливость соединения действия и некоторой другой формулы. В нашем сценарии Spec тогда выглядит так:

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)
    /\ SF_vars(OK)
    /\ SF_vars(Query /\ (sessionOK = TRUE))

Итак, что означает каждая из этих формул в совокупности? Первые три совершенно очевидны и были включены в мою попытку определения Spec.

  1. Init истинно в первом состоянии поведения.
  2. Next верно для каждого шага поведения (с допустимым заиканием).
  3. Next будет продолжать происходить, если он будет продолжать работать бесконечно, чтобы система не останавливалась в процессе обмена сообщениями.

Четвертый - моя интуиция: он исправляет ситуацию, когда делается запрос, а затем истекает срок сеанса.

  1. Если OK повторно включается (это возможно), то в конечном итоге это произойдет.

И в-пятых, чего не хватало: это исправляет ситуацию, когда OK никогда не был включен, потому что время сеанса истекло раньше, чем могло произойти Query.

  1. Если Query может случиться неоднократно и сеанс действителен в то же время, в конечном итоге это произойдет.
person urxvtcd    schedule 22.03.2020