/* loading storing */

#ifndef N
  #define N 3
#endif

byte x;
byte flag[N];

active [N] proctype p()
{  
  byte k,r;
  k = 1;
  do :: k <= 6 -> 
       k++;
       r = x;
       r++;
       x = r
     :: k > 6 -> 
       flag[_pid] = 1
   od
}