promela - 渠道设计：许多特定渠道与较少的一般渠道

Question

在 Promela 中设计模型时，当发送许多不同类型的消息时，通道的设计权衡是什么？

文档中的许多示例都使用类似这样的简单案例

mtype { M1, M2, M3 }
chan req = [0] of { mtype, chan, byte};

然而，在实践中，一些模型可能具有处理各种不同消息类型的进程，每个消息类型都有一组独特的参数。

所以通道之间似乎有一个设计决策，可以表示各种消息类型的参数：

mtype { M1, M2, M3 }
chan req = [0] of { mtype, chan, byte, int, byte, etc...};

以及特定于每种消息类型的通道

chan req1 = [0] of { chan, byte };
chan req2 = [0] of { chan, int };
chan req3 = [0] of { chan, byte, int};

我有兴趣了解一种设计相对于另一种设计的任何性能优势，以及什么被认为是最佳实践。