如何在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 }