Очередной подход к RS-триггеру, теперь с TLA+

Я уже моделировал RS-триггер как полностью синхронную схему. Но в некоторых приложений таких моделей не достаточно, требуется рассмотреть переходные процессы, которые могут возникнуть. TLA+ разработан для анализа параллельных асинхронных систем. Поупражнявшись в решении головоломок с его помощью, можно начать применять этот инструмент и для более серьезных задач.

RS-триггер состоит из двух рекурсивно связанных NOR-элементов (NOT OR). Для начала опишем отдельный NOR.

NOR(a,b,c) == c' = ~ (a \/ b)

Этот элемент связывает три точке в схеме, его действие устанавливает сигнал в точке c в следующий момент времени в NOT(OR(a,b)). Когда именно это произойдет мы пока не указываем.
Теперь объединим два NOR в один RS-триггер.

RS == (\/ (NOR(r, q, p) /\ UNCHANGED q)
       \/ (NOR(p, s, q) /\ UNCHANGED p)
       \/ (NOR(r, q, p) /\ NOR(p, s, q)))
      /\ UNCHANGED <<r,s>>

Здесь явно описана асинхронная природа электронных схем. Может сработать один из двух NOR или оба сразу. При этом предполагаем, что входные сигналы r и s не изменяются.
RS-триггер работает корректно, если не подавать ему на вход оба сигнала r и s равными TRUE. Предполагаем, что схема, в составе которой работает моделируемое устройство следует этому соглашению. Также предполагаем, что изменения входных сигналов происходит когда переходные процессы уже завершились. Это должно обеспечиваться либо выбором тактовой частоты в синхронных схемах, либо дополнительной логикой в асинхронных.

Change == /\ p = ~ (r \/ q)
          /\ q = ~ (p \/ s)
          /\ IF r = FALSE /\ s = FALSE
             THEN \/ (r' = TRUE /\ s' = FALSE)
                  \/ (r' = FALSE /\ s' = TRUE) 
             ELSE r' = FALSE /\ s' = FALSE
          /\ UNCHANGED <<p,q>>

Что бы проверить, что установившееся состояние триггера соответствует выполняемой операции введем вспомогательные переменные, в которых будем хранить значения сигналов перед изменениями.

Check == /\ oldp' = p
         /\ oldq' = q
         /\ stable' = (r = FALSE /\ s = FALSE)

Теперь можно сформулировать предикат перехода.

Next == Check /\ (RS \/ Change)

Кроме корректности установившегося состояния триггера будем проверять так же непротиворечивость выходов в промежуточном состоянии — что оба выхода не могут одновременно принимать значение TRUE (в частности это означает, что мы имеем право передавать выходы одного триггера на другой).

OutputOk == p /= TRUE \/ q /= TRUE

И полный инвариант

Invariant == /\ (r = FALSE \/ s = FALSE)
             /\ (stable => oldq = q /\ oldp = p)
             /\ OutputOk

Еще одно хорошее свойство, которое, однако, не может быть записано в инварианте — что переходные процессы в триггере рано или поздно завершаться.

RSok == /\ [] (r = TRUE ~> q = TRUE)
        /\ [] (s = TRUE ~> p = TRUE)

"r ~> q" — синтаксический сахар для "r => <> q".
"=>" — логический оператор «следует».
"<>" — темпоральный оператор «когда-нибудь».
"[]" — темпоральный оператор «всегда».
Темпоральные операторы запрещено использовать в инварианте, но можно в PROPERTY (свойство всей модели).
С нашим свойством RSok есть небольшая проблема — оно не выполняется! Дело в том, что действие RS выполнившись может ничего не изменить, то есть в графе состояний образуется петля, в которой система, согласно нашей спецификации, может крутиться вечно. Эту петлю не сложно было бы убрать, добавив предусловия на срабатывание

RS == (\/ ((p /= ~ (r \/ q)) /\ NOR(r, q, p) /\ UNCHANGED q)
       \/ ((q /= ~ (p \/ s)) /\ NOR(p, s, q) /\ UNCHANGED p)
       \/ (((p /= ~ (r \/ q)) /\ (q /= ~ (p \/ s)) /\ NOR(r, q, p) /\ NOR(p, s, q)))
      /\ UNCHANGED <<r,s>>

Но дело обстоит хуже — если задана проверка темпоральных свойств модели, TLA+ автоматически добавляет петлю в каждый узел. Это делается для «композируемости» моделей — если мы составляем модель из нескольких, действие в одном компоненте оставляют без изменения состояния не связанных с ним компонентов. Таким образом свойства компонента должны быть инвариантны к наличию петель.
Что бы с этим как-то жить, TLA+ поддерживает «справедливость» (fairness) — ему можно указать, что если переход возможен, он когда-нибудь произойдет.

vars == <<r,s,p,q, stable, oldp, oldq>>
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Fairness указывается заклинанием WF_vars(Next)

Полный файл rs.tla
Теперь создадим конфигурацию для проверки модели rs.cfg

SPECIFICATION Spec
PROPERTY RSok
INVARIANT Invariant

Проверка модели запускается командой tlc2 rs.tla или указав значения из конфигурации в настройках модели в графической оболочке tla-toolbox.