Допустим, у меня есть этот фрагмент кода PROMELA.
active proctype A(){
do
:: !x -> break
:: else -> skip
od
… //more code
}
Что именно делают break и skip в данном случае? Разрывает ли break весь процесс A(), чтобы не было достигнуто «больше кода», или только цикл?
TLDR:
break: (всегда выполняемая) инструкция, которая переводит выполнение в конец самого внутреннего цикла, в котором она содержится. Этот тип инструкций в значительной степени универсален практически для любого языка программирования.
skip: пустая (всегда выполняемая) инструкция, не имеющая никакого эффекта. Существует множество примеров нет операции из других языков, например pass в python, ; (и другие) в C, jQuery.noop() в jQuery и т. д.
active proctype A(){
do
:: !x -> break
:: else -> skip
od
… //more code
}
В этом случае, как только x становится ложным, тогда break заставляет цикл завершиться, тогда как skip — это просто пустая инструкция, явно представляющая тот факт, что в другом случае цикл продолжает ничего не делать.
ИМЯ
break — перейти в конец самого внутреннего цикла do.
[...]
ПРИМЕРЫ
L1: do :: t1 -> t2 :: t3 -> break :: break od; L2: ...В этом примере управление достигает метки L1 сразу после выполнения инструкции t2. Управление также может достигать метки L2 сразу после выполнения оператора t3, и, опционально, за один шаг выполнения управление также может перейти с метки L1 на метку L2.
ИМЯ
skip - сокращение для фиктивного, нулевого оператора.
[...]
ПРИМЕРЫ
proctype A() { L0: if :: cond1 -> goto L1 /* jump to end */ :: else -> skip /* skip redundant */ fi; ... L1: skip }В этом примере требуется оператор пропуска, следующий за меткой L1. Использование оператора skip, следующего за защитой else в приведенной выше структуре выбора, является излишним. Приведенный выше выбор можно записать более кратко:
L0: if :: cond1 -> goto L1 :: else fi;Поскольку Promela является асинхронным языком, пропуск никогда не нужен и неэффективен для задержки выполнения процессов. В Promela по определению всегда может быть произвольная и неизвестная задержка между любыми двумя последующими выполнениями оператора в теле proctype. Эта семантика соответствует золотому правилу проектирования параллельных систем, которое запрещает предположения об относительной скорости выполнения асинхронных процессов в параллельной системе.
