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};
ある設計が他の設計よりも優れているパフォーマンス上の利点と、ベスト プラクティスと見なされるものを理解したいと考えています。