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 }