promela - PROMELA でメッセージのサイズを宣言する方法は?

Question

メッセージのサイズを指定する方法はありますか? たとえば、チャネル AB を介してメッセージ データを送信したい場合、PROMELA 言語でデータのサイズを指定するにはどうすればよいですか?

Answer 1

チャネルを宣言するための構文は、たとえば次のとおりです。

chan ab = [16] of { short }

abチャネルにバインドされた識別子です。16チャネル内のメッセージ数です。 short各メッセージのデータ型です。

メッセージ タイプを指定する場合、いくつかの追加オプションがあります。

char ab = [16] of { byte, short, bit }

これにより、各メッセージがバイト、ショート、ビットのチャネルが作成されます。このような場合は、多くの場合、次のように新しいタイプを作成することをお勧めします:

typedef message {
  byte operator;
  short data;
  bit what;
};

その後

chan ab = [16] of { message }