問題タブ [promela]

モデルチェックのためにプロメラでプロジェクトの1つをモデル化しようとしています。その中で、私はネットワーク内にN個のノードを持っています。そのため、ノードごとにプロセスを作成しています。このようなもの：

したがって、基本的に、ここでの各「ノード」は、ネットワーク内の各ノードをシミュレートするプロセスです。現在、ノード プロセスには、元の実装で並列に実行される 3 つのスレッドがあり、これらの 3 つのスレッド内で、3 つのスレッドが同時にクリティカル セクションにアクセスしないように、一部をロックしています。だから、プロメラでこれのために、私はこのようなことをしました：

ここで、recv_A、send_B、および do_C は、ネットワーク内の各ノードで並行して実行される 3 つのスレッドです。さて、問題は、atomic を使用して recv_A、send_B、do_C にロックを設定すると、3*N プロセスすべてにロック ロックが設定されるのに対し、3 つのグループにロックが適用されるようなロックが必要になることです。つまり、プロセス 1 (recv_A が実行されるメイン ノード プロセス) の recv_A がその CS にある場合、プロセス 1 の send_B と do_C のみが CS に入るのを禁止する必要があり、プロセス 2 の recv_A、send_B、do_C は禁止されません。これを行う方法はありますか？