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

[woronin]

А разве после красного не может быть желтый перед зеленым? И как тогда будет выглядеть наш автомат про который идет речь в статье?
Он же усложнится и станет при этом похож на модель Харелла, или я не прав?

[lws0954]

Все может быть. Может быть любой цвет. Например, переход из состояния 1 в 2 (см. рис.2) может происходить через промежуточное состояние, в котором можно будет включить на какое-то время желтый.

Но это будет уже другой светофор. У рассматриваемого светофора даже не предусмотрен желтый.

А по поводу модели Харелла. Конечно, нет.

Но главная цель статьи в другом. В демонстрации теоретических возможностей автоматов. Есть даже результат, на который следовало бы обратить внимание. Возможностей, которых фактически нет у других моделей. У модели блок-схем (типичной модели для любого языка программирования) так точно. Правда, любую блок-схему можно обратить в автомат и далее продолжить... И, может, если постараться, получить такой же результат. Но можно доказать и обратное. Т.е. у автоматов есть теория, которой можно пользоваться и на формальном уровне делать формальный анализ созданной модели.А это намного эффективнее, чем обычное тестирование.