/* This is a barrier program in Promela*/
#define numProcs 2
#define maxCycles 3
byte arrive1 =0, arrive2 =0, k=0, j=0;

proctype client1()
{
  do
  :: (k<=maxCycles)->
  barrier: atomic{
     arrive1==0->arrive1=1;
     arrive2==1-> arrive2=0;
     k=k+1}
  :: (k>maxCycles) -> break
  od
}
proctype client2()
{
  do
  :: (j<=maxCycles)->
    barrier: atomic{
      arrive2==0->arrive2=1;
      arrive1==1->
      arrive1=0;
     j=j+1}	
  :: (j>maxCycles) -> break
  od
}
active proctype monitor() { 
    assert(k==j || k==j+1 || j==k+1);}
init{
  atomic{
	  run client1(); run client2();	
  }
}