title: Lock between N Processes in Promela
body: <p>I am trying to model one of my project in promela for model checking. In that, i have N no of nodes in network. So, for each node I am making a process. Something like this:</p>
  
  <pre><code>init {
  byte proc;
  atomic {
      proc = 0;
      do
      :: proc &lt; N -&gt;
          run node (q[proc],proc);
          proc++
      :: proc &gt;= N -&gt;
          break
      od
  }
  }
  </code></pre>
  
  <p>So, basically, here each 'node' is process that will simulate each node in my network. Now, Node Process has 3 threads which run parallelly in my original implementation and within these three threads i have lock at some part so that three threads don't access Critical Section at the same time. So, for this in promela, i have done something  like this:</p>
  
  <pre><code>proctype node (chan inp;byte ppid)
  {
     run recv_A()
     run send_B()
     run do_C()
  }
  </code></pre>
  
  <p>So here recv_A, send_B and do_C are the three threads running parallelly at each node in the network. Now, the problem is, if i put lock in recv_A, send_B, do_C using atomic then it will put lock lock over all 3*N processes whereas i want a lock such that the lock is applied over groups of three. That is, if process1's(main node process from which recv_A is made to run) recv_A is in its CS then only process1's send_B and do_C should be prohibited to enter into CS and not process2's recv_A, send_B, do_C. Is there a way to do this?</p>