LTL: всегда, когда-нибудь, до тех пор, пока

Нина Аркадьевна Ветлугина · старший диспетчер

Самописец перегона пишет ленту: каждую минуту отмечает, какие лампы горят. Устав говорит, какие ленты допустимы. Мне нужно, чтобы машина брала ленту и устав и сама говорила, где нарушение. Для этого устав надо переписать на язык, который машина читает.

Ветлугина разворачивает ленту за 3 мая. Каждая клетка это минута, в клетке отмечены горящие лампы: req (дежурный запросил отправление), ok (разрешение выдано), east (поезд из Сольска на перегоне), west (поезд из Кривой Балки на перегоне).

Минута	14:00	14:01	14:02	14:03	14:04
Лампы		req	req, ok	east	east, west

Пункт 1 устава: «на перегоне никогда не бывает двух поездов». На ленте он нарушен в 14:04, это видно глазами. Пункт 2: «на каждый запрос когда-нибудь выдают разрешение». Нарушен ли он на ленте, которая кончилась в 14:04? А на ленте, которая будет крутиться вечно? Чтобы машина отвечала на такие вопросы, нужна логика, в которой есть слова «никогда», «каждый раз» и «когда-нибудь».