Согласно верификатору, у модели - 92 достижимых состояния
В LTS для программы - 89 достижимых состояний
Верификатор выдает больше состояний т.к. для программы на промеле init { atomic{ skip; } } он выдает именно эти три состояния. Т.е. это занимает init.