Я уже моделировал 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
--------------------------------- 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 SpecPROPERTY RSokINVARIANT InvariantПроверка модели запускается командой tlc2 rs.tla или указав значения из конфигурации в настройках модели в графической оболочке tla-toolbox.
