Модель на Promela , выраженные на входном языке SPIN

Пересечения: 34 39 15 Выдается индивидуально несколько пересечений на перекрестке. Необходимо составить модель контроллера светофора, управляющего движением автомобилей по...