問題タブ [uppaal]

私は5つのプロセスを持つシステムを持っています。プロセスの 1 つが signal1! を送信します。3つのプロセスに（つまり、3つのプロセスがsignal1を受信しますか？）。しかし、3 つの受信プロセスのうちの 1 つだけをシミュレートすると、signal1 を受信しました。3つすべてがこのsignal1を同時に受信するようにするにはどうすればよいですか?

CSP のような同期メカニズムを使用しようとしていますが、次のモデルの初期状態がデッドロックになる理由がわかりません。

私の意見では、2 つのプロセスはチャネル「a」で同期されており、少なくとも 1 つのステップを実行する必要があります。

私は次の構造体を持っています:

そして、この配列を次のように初期化します。

ただし、最初の要素については、次のエラーが発生します。

無効な初期化子

2 番目の要素については、次のようになります。

初期化子の要素が多すぎる

私が使用している Uppaal のバージョンは4.1.19. では、問題はどこに問題があるのか​​ということです。