Исходная модель из третьего задания была неверна и исправлена. В канал передавался pid процесса, равный 2 или 3, а поле было типа bit - происходило сужение диапазона и, как следствие, модель вылетала с ошибкой. Тип поля был заменен на int.
Также конструкция вида:
  do
    :: skip;
    :: break;
  od;
была заменена на:
  forever_lbl:
  if
    :: skip;
    :: goto forever_lbl;
  fi;
так как spin ругался на присутствие явного self-loop.

В модифицированной модели добавлены:
1) добавлены необходимые метки progress
2) добавлены метки для применения формул ltl при помощи конструкций never
3) в некоторых местах добавлены skip; т.к. spin неприемлет метки в самом начале блока {}

Данная модель адекватна, поскольку любая трасса этой модели моделирует некоторую трассу исходной программы. Из того, что некоторое свойство не выполняется на данной модели следует, что он не выполняется и на исходной программе.