verification - Promela の N プロセス間のロック

Question

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

init {
byte proc;
atomic {
    proc = 0;
    do
    :: proc < N ->
        run node (q[proc],proc);
        proc++
    :: proc >= N ->
        break
    od
}
}

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

proctype node (chan inp;byte ppid)
{
   run recv_A()
   run send_B()
   run do_C()
}

ここで、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 は禁止されません。これを行う方法はありますか？