Aqui,http://spinroot.com/spin/Man/Manual.html, está escrito que:

Em Promela, há também outra maneira de evitar o teste e definir o problema: sequências atômicas. Ao prefixar uma sequência de instruções entre chaves com a palavra-chave atômica, o usuário pode indicar que a sequência deve ser executada como uma unidade indivisível, não intercalada com outros processos.Causa um erro em tempo de execução se alguma instrução, exceto a primeira, bloquear em uma sequência atômica. É assim que podemos usar sequências atômicas para proteger o acesso simultâneo ao estado da variável global no exemplo anterior.

E aqui,http://spinroot.com/spin/Man/atomic.html, está escrito que:

Se alguma instrução dentro da sequência atômica bloquear, a atomicidade será perdida. Se alguma instrução dentro da sequência atômica bloquear, a atomicidade será perdida e outros processos terão permissão para iniciar a execução das instruções. Quando a instrução bloqueada se torna executável novamente, a execução da sequência atômica pode ser retomada a qualquer momento, mas não necessariamente imediatamente. Antes que o processo possa retomar a execução atômica do restante da sequência, o processo deve primeiro competir com todos os outros processos ativos no sistema para recuperar o controle, ou seja, deve ser agendado para execução.

Então, qual é a verdade? Desde a primeira citação, podemos aprender que não é permitido bloquear atômica (não a primeira declaração)

A partir da segunda citação, aprendemos que não há problema em bloquear atômica. Você acabou de perder a atomicidade e é isso.