http://spinroot.com/spin/Man/Manual.htmlнаписано что:В Promela есть также другой способ избежать теста и установить проблему: атомные последовательности. Префикс префикса последовательности операторов, заключенных в фигурные скобки, с ключевым словом atomic, пользователь может указать, что последовательность должна быть выполнена как одна неделимая единица, не чередуемая с любыми другими процессами.

Это вызывает ошибку во время выполнения, если какой-либо оператор, кроме первого, блокирует атомарную последовательность, Вот как мы можем использовать атомарные последовательности для защиты одновременного доступа к состоянию глобальной переменной в предыдущем примере.И здесь,

http://spinroot.com/spin/Man/atomic.htmlнаписано что:Если какой-либо оператор внутри атомарной последовательности блокируется, атомарность теряется. Если какой-либо оператор внутри атомарной последовательности блокируется, атомарность теряется, и тогда другим процессам разрешается начинать выполнение операторов. Когда заблокированный оператор снова становится исполняемым, выполнение атомарной последовательности может быть возобновлено в любое время, но не обязательно сразу. Прежде чем процесс сможет возобновить атомарное выполнение оставшейся части последовательности, процесс должен сначала конкурировать со всеми другими активными процессами в системе, чтобы восстановить контроль, то есть сначала он должен быть запланирован для выполнения.

Итак, что является правдой? Из первой цитаты мы можем узнать, что в атомарной блокировке запрещено (не первая инструкция)

Из второй цитаты мы узнаем, что в атомарном блоке все нормально. Вы просто теряете атомарность и все.

Противоречивая документация: