Member 14075527 Ответов: 2

В чем именно разница между skip и break в PROMELA?

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

active proctype A(){

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

   … //more code
}


А что именно делает break и skip сделать в данном случае? Делает break разбейте весь процесс A() так что "больше кода" не будет достигнуто или только цикл?

Что я уже пробовал:

Исследовал сеть, но она все еще не очень ясна для меня.

2 Ответов

Рейтинг:
2

Patrice T

Цитата:
В чем именно разница между skip и break в PROMELA?

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

Member 14075527

Я исследовал, но это все еще не ясно для меня. Форум пользователей не принимает новых участников.

Рейтинг:
1

Richard MacCutchan

Как же это вы не смогли найти Краткий Справочник Promela[^Оба (и все остальные утверждения) ясно объяснены.

Member 14075527

Спасибо. Я читал это, но, как я уже сказал, это было не на 100% ясно для меня, так как мой родной язык не английский. Правильно ли я понимаю, если скажу, что оператор break может вырваться только из цикла или в данном случае из do-repitation, а не из всего проктипа? И Скип на самом деле ничего не делает?

Richard MacCutchan

Да, это верно.

0x01AA

+5. Какой смешной язык: "пропуск: не имеет никакого эффекта и в основном используется для удовлетворения синтаксических требований". Так что "НОП высокого уровня" :-)

Member 14075527

Что они подразумевают под синтаксическими требованиями?

0x01AA

Может быть, это поможет: Promela Reference -- skip(1)[^]

а это: Обзор PROMELA | типы объектов | InformIT[^]

Взгляните на то, что while(a!=b) пример во второй ссылке. Это должно объяснить использование skip. Похоже также, что в основном вы можете переписать код, чтобы избежать skip

Member 14075527

Спасибо за вторую ссылку. Я думаю, что знаю, что делает скип. Единственное, что мне все еще нужно знать, - это то, что именно делает break. Не только вырваться из не-повторения, так что код ниже не-повторения будут выполнены/достигнуты или это блок/ждать кода ниже?

0x01AA

Имейте в виду, я не знаком с PROMELA. Но что здесь написано Promela Reference -- break(3)[^] особенно в "записках"

ЗАПИСИ
Было бы ошибкой помещать оператор break там, где нет окружающей структуры повторения. Эффект оператора break всегда можно воспроизвести с помощью оператора goto и метки.

Я бы предположил, что это неблокирующее заявление.