ここhttp://spinroot.com/spin/Man/Manual.htmlに、次のように書かれています。
Promela には、テストとセットの問題を回避する別の方法もあります: アトミック シーケンスです。中かっこで囲まれたステートメントのシーケンスの前にキーワードatomicを付けることで、ユーザーは、シーケンスが他のプロセスとインターリーブされずに、分割できない1つの単位として実行されることを示すことができます。最初のステートメント以外のステートメントがアトミック シーケンスでブロックされると、実行時エラーが発生します。これは、アトミック シーケンスを使用して、前の例でグローバル変数状態への同時アクセスを保護する方法です。
そして、ここhttp://spinroot.com/spin/Man/atomic.htmlには、次のように書かれています。
アトミック シーケンス ブロック内のいずれかのステートメントが失われると、原子性が失われます。ブロックされたステートメントが再び実行可能になると、アトミック シーケンスの実行はいつでも再開できますが、すぐに再開できるとは限りません。プロセスがシーケンスの残りのアトミックな実行を再開する前に、プロセスはまずシステム内の他のすべてのアクティブなプロセスと競合して制御を取り戻す必要があります。つまり、最初に実行をスケジュールする必要があります。
それで、本当は何ですか？最初の引用から、atomic でブロックすることは許可されていないことがわかります (最初のステートメントではありません)。
2 番目の引用から、atomic でブロックしても問題ないことがわかります。原子性を失うだけで、それだけです。