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

Исполним обещанное в [1], где упомянута задача о светофоре Ангера [2]. Она интересна формулировкой, которая заметно отличается от аналогичных задач, и утверждением, что более компактного решения, чем предложенное автором монографии, не существует. Обычно светофоры моргают, «тупо» реализуя фиксированную временную последовательность. В светофоре С..Ангера есть динамизм. Он определяется датчиками, фиксирующими ситуацию на перекрестке. И это само по себе интересно. А утверждение формальным путем, сомневаться в справедливости которого оснований, казалось бы, нет. Но нет исследователя, который не ставил бы перед собой задачу доказать недоказуемое или опровергнуть неопровергаемое. И один из способов достичь желаемого – создать решение, подтверждающее вашу правоту. Как настоящие исследователи, мы именно это и попытаемся сделать, опровергнув, если удастся, тем самым утверждение С.Ангера. А начнем мы с реализации светофора в исходной формулировке, хотя и в рамках другой формальной модели [3]. Читать далее