Доказательство недоказуемого или о светофоре Ангера замолвите слово

Исполним обещанное в [1], где упомянута задача о светофоре Ангера [2]. Она интересна формулировкой, которая заметно отличается от аналогичных задач, и утверждением, что более компактного решения, чем предложенное автором монографии, не существует.

Обычно светофоры моргают, «тупо» реализуя фиксированную временную последовательность. В светофоре С..Ангера есть динамизм. Он определяется датчиками, фиксирующими ситуацию на перекрестке. И это само по себе интересно. А утверждение формальным путем, сомневаться в справедливости которого оснований, казалось бы, нет.

Но нет исследователя, который не ставил бы перед собой задачу доказать недоказуемое или опровергнуть неопровергаемое. И один из способов достичь желаемого – создать решение, подтверждающее вашу правоту. Как настоящие исследователи, мы именно это и попытаемся сделать, опровергнув, если удастся, тем самым утверждение С.Ангера.

А начнем мы с реализации светофора в исходной формулировке, хотя и в рамках другой формальной модели [3].

Задача Ангера о светофоре

Пусть автостраду пересекает сельская дорога [2]. На перекрестке установлен светофор, который останавливает движение по автостраде, когда у переезда со стороны сельской дороги появляется автомобиль. Требуется создать систему управления, которая получает сигналы от реле времени и параллельно соединенных датчиков давления, вмонтированных в полотно сельской дороги.  Сигнал x1 от реле времени отсутствует в течение 60 сек и появляется на 30 сек. Светофор  включает красный сигнал на всем 30-ти секундном интервале (x1=1), если только на сельской дороге есть автомобили (x2=1). 

С.Ангер описал работу системы управления светофором последовательностной функцией (ПФ), табличная форма которой представлена таблицей 1. При этом он утверждает, что «не существует таблицы с меньшим числом строк, удовлетворяющей заданным требованиям». Далее мы с этим и поспорим.

Таблица 1

Минимизированная

таблица переходов

x1x2

От последовательностной функции к конечному автомату

Последовательностная функция это фактически тот же последовательностный или конечный автомат (КА). Как говорится, «тот же вид, только сбоку». У ПФ те же состояния, что и у КА, те же условия переходов между ними и ровно такие же сигналы на входах/выходах. А потому эквивалентный полностью определенный структурный конечный автомат строится достаточно просто. Такой автомат приведен на рис. 1a. На нем входные сигналы заменены на имена логических переменных, а действия y1, y2 устанавливают сигнал z, соответственно,  в 1 и в 0.

Графы на рис. 1 демонстрируют также последовательность перехода к более компактной и наглядной модели автомата в форме модели ДНФ СКА (дизъюнктивная нормальная форма структурных конечных автоматов), предложенной в [3]. Здесь автомат G1.1 эквивалентен автомату G1.0  (в форме совмещенного автомата Мили-Мура), а автомат G1.2 соответствует модели автомата в форме ДНФ СКА. Подобные формализованные преобразования описаны в [3].  

Упрощенно переход к модели ДНФ СКА (далее просто автомат) можно описать и так. Сначала выявляются одинаковые сигналы на переходах в то или иное состояние. Они должны быть на всех переходах, ведущих в это состояние. Они удаляются с переходов и приписываются к состоянию. Это будут сигналы автомата Мура. Затем, как бесполезные, удаляются петли, которые не имеют выходных сигналов. Выполнению этих шагов соответствует автомат G1.1. После этого делаем «склейку» переходов, соединяющих  одинаковые состояния и имеющие одинаковыми наборами действий. Так получаются автоматы вида G1.2.

Минимизация конечного автомата Ангера

Автомат на рис. 1с представляет минимизированную форму модели автомата Ангера.  Он подсказывает и путь дальнейшей минимизации модели. Подобные действия часто называют «склейкой состояний» - совмещение нескольких состояний автомата, не изменяющих его поведение. В данном случае мы можем «склеить»  состояния 4 и 2. Склейка возможна в силу эквивалентности последовательности переходов 1->4->2 переходу 1->2.  Результат операции представлен графом КА на рис. 2.

Итак, мы опровергли утверждение С.Ангера о минимальной форме системы управления светофора. Таблица ПФ, построенная по автомату G2, будет содержать на одну строку меньше, чем таблица 1, т.к. число ее строк равно числу состояний последовательностной функции.

В порядке эксперимента можно «склеить» попробовать состояния 1 и 2. Хотя бы потому, по выходным сигналам они не отличаются друг от друга. В результате мы получим еще одну компактную модель G3. Она показана на рис. 3.  Но будет ли ее поведение эквивалентно поведению модели Ангера G1.0 покажут результаты тестирования.

Тестирование моделей светофора Ангера

По форме, конструкциям предикатов и действий рассмотренные модели просты и для их реализации достаточно  визуальных средств среды ВКПа. На рис. 4 демонстрируется создание переменных и формирование предикатов и действий, а на рис. 5  показаны блоки типа FAutomaton, реализующие автоматные модели.

Для сравнительного тестирования модели нужно запустить параллельно, отобразив одновременно в графической форме изменение их входных и выходных сигналов.   Результаты подобного тестирования показаны на рис. 6. Здесь входные сигналы подаются на все блоки, выходными сигналами которых являются переменные z, z-II и z-III для соответственно автоматов G1.2, G2 и G3.

На диаграммах выделенные области отражают варианты ситуаций значения сигнала x2 по отношению к временному сигналу x1. Область I демонстрирует появление автомобиля на сельской дороге до установки сигнала x1. Все модели отрабатывают правильно, зажигая красный сигнал на автостраде. Область II соответствует появлению автомобиля во время действия сигнала x1. В этой ситуации светофоры G1.2 и G2 работают правильно, а модель G3 спешит зажечь красный цвет. Она тем самым нарушает требование к длительности выходного сигнала светофора.

Интересно поведение светофоров в области IV. Здесь сигнал от датчиков кратковременно устанавливается до установки сигнала x1. Это  можно трактовать как их ложное срабатывание, а можно и как разворот (не исчезновение же?!) автомобиля на сельской дороге.  И если модель G3 игнорирует подобную ситуацию, то светофоры Ангера включают красный свет. Перестраховка? Но нужна ли она? Может, логичнее было бы дождаться надежного срабатывания датчиков и лишь затем перекрывать автостраду, не пытаясь реагировать «на каждый чих».

Да, работа временного сигнала x1 моделируется параллельным процессом, который через заданные интервалы времени устанавливает переменную X1 (см. переменные на рис. 3), а значение переменной X2 устанавливается вручную с помощью диалога управления переменными среды.

Cветофор от Engee

Для тех, кто после светофоров Ангера хотел бы расслабиться, их вниманию в разделе «Документация Engee» на сайте Engee в подразделе «Конечные автоматы» предлагается проект «Моделирование управляющей логики светофора».  Принцип его работы здесь представлен графом конечного автомата на рис. 6.

Цитируем: «Светофор имеет три цвета и все время переключается между ними. Момент, когда горит какой-то из цветов, называется состоянием системы. Соответственно, наша модель будет иметь три состояния: Red, Yellow и Green. Red будет являться состоянием по умолчанию, то есть каждый цикл будет начинаться с него».

Повторим данную модель в ВКПа. Благо это займет немного времени. Но смоделируем подобный светофор двумя автоматами, где первый будет реализовать собственно светофор, а второй устанавливать значение переменной light в зависимости от его текущего состояния. Рис. 7 демонстрирует работу модели. Он отражает состав переменных модели, реализацию автоматов и диаграммы сигналов текущих состояний светофора и выходного сигнала light. Графы самих автоматных моделей приведены на рис. 8.

Конечно, можно было бы подобно сайту Engee обойтись одним автоматов. Но мы осознанно создали второй автомат, чтобы, во-первых, продемонстрировать работу с состояниями автоматов в ВКПа, а, во-вторых, показать гибкость параллельного подхода. К примеру, в нашем варианте модель установки выходного сигнала светофора может быть изменена независимо от модели светофора.  

А в чем «фишка» работы с состояниями в ВКПа? Здесь для этого введен тип переменных, названный fsa(state). Он принимает булевское значение в зависимости от значения текущего состояния процесса с именем «fsa» и именем состояния «state». На рис. 7 предикат x1 автомата с именем SetLights использует данный тип подобно типу переменной булевского типа.

Заключение

Выше мы рассмотрели различные аспекты автоматного проектирования вообще и автоматного программирования в частности.  На примере светофора Ангера были рассмотрены формальные приемы преобразования и минимизации модели КА. А на примере светофора с сайта Engee показано, как можно распараллелить решение, чтобы добиться нужной гибкости проектирования. Показаны приемы доступа к значению текущего состояния на базе встроенных в вычислительную модель механизмов доступа к состоянию модели. Механизма, отсутствующего не только у других вычислительных моделей, но, порой, и у других реализаций модели КА. 

И не считаете ли вы теперь, друзья, после столь подробного анализа «светофорной темы»,  что автоматная модель ВКПа не только проще, нагляднее, но и мощнее, чем модель Харелла, которую использует Engee? Замечу также, а это очень и очень важно, в отличие от модели Харелла она в  точности соответствует классической модели конечного автомата, а потому к ней применимы наработки теории конечных автоматов (ТКА). Про модель Харелла это сказать нельзя.

Хотя, в утешение поклонников модели Харелла, признание этого факта совсем не означает умаление качеств или достоинств последней. «Каждый дышит, как он слышит». Но дышится в такой ситуации много легче, когда есть теория. С последним у последней явные проблемы. Учтите это, если захотите высказаться на выше заданный вопрос.

Литература

1.       Но почему, почему, почему был светофор зеленый? https://habr.com/ru/articles/1044514/

2.     Ангер С. Асинхронные последовательностные схемы. – М.: Наука. Гл. ред. физ.-мат. лит., 1977. - 400 с.

3.       Автоматное программирование: определение, модель, реализация. https://habr.com/ru/articles/682422/