В чем разница между пропуском и разрывом в PROMELA? - PullRequest
Новая
       55

В чем разница между пропуском и разрывом в PROMELA?

0 голосов
/ 03 декабря 2018

Допустим, у меня есть этот фрагмент кода PROMELA 

active proctype A(){

   do
      :: !x -> break
      :: else -> skip
   od

   … //more code
}

Что именно break и skip делают в этом случае?Разбивает ли break весь процесс A(), чтобы не было достигнуто «больше кода» или просто цикл?

1 Ответ

0 голосов
/ 04 декабря 2018

TLDR:

  • break : (всегда исполняемая) инструкция, которая заставляет выполнение перейти в конец самого внутреннего цикла вкоторый он содержится.Этот тип инструкций универсален практически для любого языка программирования.

  • skip : пустая (всегда исполняемая) инструкция, которая не имеет никакого эффекта.Существует множество no-op примеров из других языков, таких как pass в python, ; (и других) в C, jQuery.noop() в jQuery и т. Д. 

active proctype A(){

   do
      :: !x -> break
      :: else -> skip
   od

   … //more code
}

В этом случае, как только x становится ложным, тогда break заставляет цикл завершиться, тогда как skip является просто пустой инструкцией для явного указанияпредставляют тот факт, что в другом случае цикл продолжает ничего не делать.

С документы break

NAME

break - перейти к концу внутреннего цикла do.

[...]

ПРИМЕРЫ 

L1: do
    :: t1 -> t2
    :: t3 -> break
    :: break
    od;
L2: ...

В этом примере элемент управления достигает метки L1 сразу после выполнения инструкции t2.Элемент управления также может достигать метки L2 сразу после выполнения инструкции t3, и, необязательно, за один шаг выполнения элемент управления также может переходить от метки L1 к метке L2.

Из документы skip

NAME

skip - сокращение для фиктивного, нулевого выражения.

[...]

ПРИМЕРЫ 

proctype A()
{
L0:   if
      :: cond1 -> goto L1 /* jump to end */
      :: else -> skip     /* skip redundant */
      fi;
      ...

L1:   skip
}

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

L0:   if 
      :: cond1 -> goto L1
      :: else
      fi;

Поскольку Promela является асинхронным языком, пропуск никогда не нужен и не эффективен, чтобы вводить задержку в выполнении процесса.В Promela по определению всегда может быть произвольная и непостижимая задержка между любыми двумя последующими выполнениями операторов в теле прототипа.Эта семантика соответствует золотому правилу проектирования параллельных систем, которое запрещает предположения об относительной скорости выполнения асинхронных процессов в параллельной системе.

...