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

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

--------------------------------- MODULE rs ---------------------------------  VARIABLES r,s,p,q, stable, oldp, oldq  vars == <<r,s,p,q, stable, oldp, oldq>>  NOR(a,b,c) == c' = ~ (a \/ b)  Init == /\ r = FALSE         /\ s = FALSE         /\ p = TRUE         /\ q = FALSE         /\ stable = FALSE         /\ oldp = p         /\ oldq = q  RS == (\/ (NOR(r, q, p) /\ UNCHANGED q)        \/ (NOR(p, s, q) /\ UNCHANGED p)        \/ (NOR(r, q, p) /\ NOR(p, s, q)))       /\ UNCHANGED <<r,s>>  Check == /\ oldp' = p          /\ oldq' = q          /\ stable' = (r = FALSE /\ s = FALSE)  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>>  Next == Check /\ (RS \/ Change)  OutputOk == p /= TRUE \/ q /= TRUE  Invariant == /\ (r = FALSE \/ s = FALSE)              /\ (stable => oldq = q /\ oldp = p)              /\ OutputOk   Spec == Init /\ [][Next]_vars /\ WF_vars(Next) RSok == /\ [] (r ~> q)         /\ [] (s ~> p)  ================================================================================= 

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

SPECIFICATION Spec PROPERTY RSok INVARIANT Invariant 

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