Моделирование конечных автоматов

По-описанию напоминает Simulink или LabVIEW.

конечных автоматов

JFLAP, не? Вроде даже гуглоии на первое место её ставит. Тем более если тебе надо наглядно-обучающе.

Помню лет 30 назад, еще в универе, была какая-то программулина, которую мы использовали на теории автоматов (предмет такой был). Названия, конечно, не вспомню, но что-то мне подсказывает, что спустя 30 лет и особенно сейчас таких тулзов должно быть чуть меньше чем, разве что, гуталина

А вообще да, сиквенс диаграммы хорошо это описывают

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

с учетом того что гуталиновых фабрик уже не осталось, то фактически вы правы (хотя и подразумевали прямо противоположное). Програмулин таких нет вообще. Что-то чуть похожее это офтопиковый набор DeedsSuite.

Сиквенс диаграммы это вообще про другое.

Сиквенс диаграммы это вообще про другое

как это про другое? диаграммы состояний описывают. ну, сам автомат, правильней графом рисовать, да. я за 30 лет конечно многое забыл, но фсм в работе описываем сиквенс диаграммами (граф переходов, только для фиксации множества состояний и их связей). наверное правильней сказать, что диаграммы - это уже прикладная часть.

Напиши.

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

«Исконно-православно-отечественный»™ визуальный язык ДРАКОН © (drakon.su)/

P.S. Для андроид можно сотворить КО из Logic Circuit Simulator Pro.

С ЛабВью осторожным надо быть. Был тут парнишка один на ЛОР, так вот, он его использовал. И до того прошаренный был в этой программе, что стал какие-то странные посты строчить. Как будто рехнулся, ей богу.

как это про другое?

Сиквенс это обмен между двумя и более акторами. И упор именно последовательность обменов (кто за кем и что). Правильную последовательность.

А КА, это про переходы между состояниями. Причем у КА нет привязки к последовательности. Тебе что-то валится на вход, что изменяет твое состояние. Да, какое-то множество КА можно описать как последовательность действий. Но не все.

Напиши.

Это я всегда успею. Попробую еще поискать.

Тут даже больше вопрос не в моделирование, а в удобном представлении.

Вот есть у меня задача. Есть входные сигналы (пару десятков), есть куча состояний, есть куча выходных состояний. Как это все формально описать так, чтобы из записи было сразу видно, что ошибок нет, что перечислил все возможные варианты, чтобы сразу недостижимые и запрещенные состояния были откинуты. И чтобы это все можно было окинуть взглядом. Раньше как-то все удавалось все сразу в голове держать, а сейчас похоже мозги усохли, не помещается.

Я имел ввиду, что граф состояний описивыет конечное их число и переходами. А сиквенс, описывает внешнюю систему, которая двигается по этому графу. Сам по себе граф - справочник. Возможно для КА есть какой-то другой дсл, я не знаю (или не помню, давно в теорию не смотрел), но в реальной работе используются эти два представления.

Поправь, если ошибаюсь. Всегда полезно освежить знания

У тебя

Входы-> Черный яшик (ЧЯ)-> выходы

N состояний == N ЧЯ

Описываешь каждый ЧЯ как таблицу или функцию состояний Входы->Выходы

Описываешь как (из-за чего) меняются состояния (ЧЯ)

Т.о. разбиваешь большую задачу на мелкие

Как это все формально описать так, чтобы из записи было сразу видно, что ошибок нет,

Собственно, и ответ тут маячит (формальная верификация). Полноценно и по науке, надо писать такое на специализированных язычках, в которых сами доказательства сущности первого класса и автоматизируются компилятором - Coq, Agda, Idris, или более близкие к народу - Haskell, Rust+Creusot, Ada+spark и т.п.

Т.о. разбиваешь большую задачу на мелкие

Вот у меня все состояния можно описать 18битами. Формально это 2^18 состояний. Понятно, что 99% из них недостижимы или запрещены. Как с этим работать не перебирая все варианты? Как контролировать, что не попадешь в запрещенное состояние? Как контролировать, что не будешь описывать недостижимое состояние?

Graphviz - я этим пользовался в универе когда надо было графы рисовать.

Как любитель почитать книжку про Domain‑Driven Design тоже есть ощущение, что нужен специализированный язык для описание такой задачи. Но выдумывать нет ни сил не желания. Про Coq, Agda, Idris почитаю. Может голову прочистит.

С другой стороны АЭС автоматизировали на релейной логике и ничего, все работало. Хочется понять принцип вытягивания смысла из этой кучи состояний и входных сигналов.

Странные вопросы ты задаёшь. Программа поможет отобразить, но тебе всё-равно для этой программы придется описать возможные состояния. Значит ты должен это мочь сделать на бумаге.

В Verilog конечные автоматы (Finite State Machine, FSM) — это стандартный инструмент для описания логики управления: контроллеров, процессоров, обработчиков протоколов, декодеров и других устройств, которые работают в дискретных режимах.

https://habr.com/ru/articles/309162/

Значит ты должен это мочь сделать на бумаге.

Конечно. Вопрос в том как на бумаге описать все 2^18 состояний? Напрашиваются вложенные КА и система КА. И вот тут и нужно понять выбранная вложенность и система КА опишет все состояния? Как все это записать, чтобы потом можно было верифицировать на полноту и непротиворечивость?

У всех КА обычно не больше десятка состояний. Можно и в голове это прокрутить. А если 10тыс состояний?

А если 10тыс состояний?

Очевидно, разбить задачу на более мелкие. 10к состояний и визуально будут плохо смотреться.

Вопрос в том как на бумаге описать все 2^18 состояний?

Понятно, что 99% из них недостижимы или запрещены

Предлагаю описать только 1% )))

Очевидно, разбить задачу на более мелкие

Простой, очевидный и бесполезный ответ.

Пока решение выглядит как набор условий для изменения отдельных бит всего слова состояния. И это работает. Но это не дает уверенности в полноте и непротиворечивости.

Всегда думал, что это описывается интерфейсами. Ну. т.е. ты описываешь все возможные переходы и в реализации уже их же прописываешь.

(Надо бы паттерны проектирования перечитать.)

Как контролировать, что не попадешь в запрещенное состояние? Как контролировать, что не будешь описывать недостижимое состояние?

В принципе, при таком уточнении (ограничиваемся КА) тяжёлые матанские йобы( Coq, Agda, Idris) будут избыточны, достаточно чтобы язык поддерживал линейные/аффинные типы, первые есть в Хаскеле из коробки, вторые в Расте и без дополнительных верифицирующих инструментов. Если закодировать состояния такими типами, компилятор статически заблокирует переходы в неправильные состояния

Если закодировать состояния такими типами, компилятор статически заблокирует переходы в неправильные состояния

Стратегически вроде понятно, а вот тактически нет.

Другого я дать не могу.

Тут либо проектировать все переходы, либо формальные доказательства. В последнем не силён, но как Вам уже сказали, на то есть специализированные языки.

С ЛабВью осторожным надо быть. Был тут парнишка один на ЛОР, так вот, он его использовал. И до того прошаренный был в этой программе, что стал какие-то странные посты строчить. Как будто рехнулся, ей богу.

Я слышал, что при большом желании и целеустремлённости можно и … сломать. А с лабвью или без него роли не играет.

Вопрос в том как на бумаге описать все 2^18 состояний?

Не на бумаге, а в голограмме, все состояния проверяются за 1 такт оптическим процессором © (habr.com).

Возможно не совсем то, но может поможет https://plantuml.com/ru-dark/state-diagram

Не на бумаге, а в голограмме, все состояния проверяются за 1 такт оптическим процессором

А что в оптическом процессоре понимается под «один такт»? В тексте скорее концепция, давно существуют реализации. LightSolver, например, одна из моих последних оценок, неделю назад к нам приезжали.

А что в оптическом процессоре понимается под «один такт»?

1 импульс лазера.

Да, спасибо. Не совсем то, но познакомиться синтаксисом всегда полезно.

Не годится. Слишком медленно.

ну Можно с принсипия матататика Уйтхеда Рассела кнч начать ежель релюху АЭС эталон

проблема реальных инструментов именно в том что как только вы решаете проблему(а не упражнение по меткому выражению чела на которуго Кнут в предисловии ссылается) то очень быстро проще свой инструмент точить

ибо цвм онеж реально универсальны - вам же не hmi оператора тех процесса

вам буквально анализ состояний в полноте

вам буквально анализ состояний в полноте

вода мокрая, кнут велик.

Да, это все известно. Свой тулинг писать мне лень.

Пробуй, но готовься к тому, что придётся писать.

О, вспомнилась моя дипломная работа «Редукция автоматных отображений». Прям навеяло. Эх. Было там много всего интересного. Можно было в интерфейсе накидать конечный автомат (прям мышкой, легко, переход-выход прям там мышкой делался и отображался в таблице). Про сохранение и загрузку автоматов говорить не буду. Рутина. Можно было задать любой алфавит. Ну а далее - смачные алгоритмы на графах. Выявлялись несвязанные графы, циклы, хвосты. Графы - автоматные отображения. И при этом в цикле увеличивалась длина входного слова. Числодробилка должна работать при чудовищно длинных словах и размерах алфавита. Цель - выявить автоматные отображения по типам. Эргодические, совместимые и сохраняющие меру. Ну и упростить конкретный автомат уменьшив число состояний. Почитай В.С. Анашина про критерии и прочее. Очень занимательно. Всё это крутилось вокруг р-адических систем. «Автоматы можно рассматривать как р-адические динамические системы, для которых применим р-адический подход, когда детерминированная функция, соответствующая автомату, рассматривается как непрерывная относительно р- адической метрики». О как было весело.