Раздел 44 · Логика и типы

Босс: две стрелки

senior~130 мин

без входаВойди, чтобы отмечать прогресс, вести заметки и решать задачи в редакторе. войти

Судья Гранович

Дорога хочет поставить на перегон Сольск · Кривая Балка автоматику «Две стрелки» и просит суд признать, что после этого за встречи поездов она не отвечает. Инженеры говорят, что схема прошла испытания. Я хочу знать три вещи: что схема обещает, держит ли она обещания и почему. Ответы на первые два вопроса пусть даст машина. На третий ответ даёте вы.

Ветлугина приносит в суд две схемы. Обе заменяют физический жезл флажками: у каждого поста лампа «хочу на перегон», которую видит сосед по телеграфу.

  • Схема A, «посмотрел, потом поднял». Пост смотрит на флажок соседа. Если тот опущен, пост готовится, поднимает свой флажок и выпускает поезд.
  • Схема B, «поднял, потом жду». Пост сначала поднимает свой флажок, потом ждёт, пока сосед опустит свой, и выпускает поезд.

Вельский, теперь поверенный поставщика автоматики, пожимает плечами: «Обе схемы испытаны на стенде, сто прогонов без единой встречи. Какая разница, какую ставить?»

Это босс блока «Диспетчерская». Ты пройдёшь весь путь, который проходит инженер формальных методов: запишешь требования формулами, найдёшь машиной ленты, на которых схемы ломаются, починишь схему и проверишь починку проверяльщиком, а потом докажешь судье, почему починка работает.

урок из курса

Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.

Оплата пока не подключена: премиум и курсы открываются промокодом.