// peterson TSO -> peterson SC   (ESBMC)


//#include "locks.h"

#include <stdio.h>
#include <pthread.h>

//#define TRUE 1
//#define FALSE 0


typedef enum boolean {FALSE,TRUE} bool;


   // shared vars
int flag0;
int flag1;
int turn;
int cs0;
int cs1;

void __ESBMC_atomic_begin();
void __ESBMC_atomic_end();

_Bool nondet_bool();


void* thread0(void* arg)
{
  // var declarations
//  round ROUND;
  
  int sim, roundTSO, roundSC; 

  
  
//  mask MASK[2];   // masks for each round  
  int MASK0flag0, MASK0flag1, MASK0turn;
  int MASK1flag0, MASK1flag1, MASK1turn;
    
  
//  shared VIEW, QUEUE[2];       // view of the thread

  int VIEWflag0, VIEWflag1, VIEWturn;
  int QUEUE0flag0, QUEUE0flag1, QUEUE0turn;
  int QUEUE1flag0, QUEUE1flag1, QUEUE1turn;

   //BEGIN init_thread


   __ESBMC_atomic_begin();
//   AcquireSpinLock(lock);

   sim = 1;
   roundTSO = roundSC =0;
      // set the view to the shared vars
   VIEWflag0 = flag0;
   VIEWflag1 = flag1;
   VIEWturn  = turn;
      // initialize MASK0 and MASK1
   MASK0flag0 = MASK1flag0 = 0;  
   MASK0flag1 = MASK1flag1 = 0;  
   MASK0turn  = MASK1turn  = 0;

   if ( nondet_bool()) 
   {sim = FALSE;  
   __ESBMC_atomic_end();} //is_end_round
   

   //END init_thread
//NEVER CHANGE

   // flag[0] = 1;

  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);

      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1) roundTSO=0; else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
          MASK1flag1 = 0;
      if  (roundSC==0) 
          MASK0turn  = 0; 
      if  (roundSC==1) 
          MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )   
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )   
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )   
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END

//   memory_update_flag0( &ROUND, &VIEW, MASK, QUEUE, 1);
   VIEWflag0 = 1;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)  
            roundTSO=0; 
          else roundTSO++; } 
   }
   if (roundSC == roundTSO) 
      flag0 = 1;
   else{   // updating mask + queue
          if (roundTSO==0) 
          {  MASK0flag0 = 1; 
             QUEUE0flag0 = 1;} 
          if (roundTSO==1) 
          {MASK1flag0 = 1; QUEUE1flag0 = 1;} 
        }
//END memory_update_flag0

   if ( nondet_bool()) 
   {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   //turn = 1;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)  
            roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )   
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )   
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )   
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
  //   memory_update_turn( &ROUND, &VIEW, MASK, QUEUE, 1);
   VIEWturn = 1;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)  
            roundTSO=0; 
          else roundTSO++; } 
   }
   if (roundSC == roundTSO) 
      turn = 1;
   else{   // updating mask + queue
          if (roundTSO==0) 
             {MASK0turn = 1; QUEUE0turn = 1;} 
          if (roundTSO==1) 
             {MASK1turn = 1; QUEUE1turn = 1;} 
        }
//END memory_update_turn
   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   //fence   
   __ESBMC_assume(roundTSO == roundSC);


   //while (flag[1] == 1 && turn == 1)
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)  
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )   
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )   
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )  
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END


__ESBMC_assume ( !(VIEWflag1 && VIEWturn) );

/*
   while (VIEWflag1 && VIEWturn){

      // busy wait
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)  
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
        flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
        flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
        turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
        flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
        flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
        turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   }

*/

   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   // CRITICAL SECTION
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   /*__ESBMC_atomic_begin();*/
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
              roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
        MASK0flag0 = 0; 
      if  (roundSC==1)
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
        flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
        flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
        turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
        flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
        flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
        turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   cs0 = 1;
   if ( nondet_bool())
    {sim = 0;  /*__ESBMC_atomic_end();*/} //is_end_round
   
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
              roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
        flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
        flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
        turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
        flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
        flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
        turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   cs0 = 0;
   if ( nondet_bool())
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   //flag[0] = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
        flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
        flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
        turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
        flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
        flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
        turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
//   memory_update_flag0( &ROUND, &VIEW, MASK, QUEUE, 0);
   VIEWflag0 = 0;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)
             roundTSO=0;
          else roundTSO++; } 
   }
   if (roundSC == roundTSO)
    flag0 = 0;
   else{   // updating mask + queue
          if (roundTSO==0) 
             {MASK0flag0 = 1; QUEUE0flag0 = 0;} 
          if (roundTSO==1) 
             {MASK1flag0 = 1; QUEUE1flag0 = 0;} 
        }
//END memory_update_flag
   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round
 
__ESBMC_assume ( 0 );
  
}


void* thread1(void* arg)
{
  // var declarations
//  round ROUND;
  
  int sim, roundTSO, roundSC; 

  
  
//  mask MASK[2];   // masks for each round  
  int MASK0flag0, MASK0flag1, MASK0turn;
  int MASK1flag0, MASK1flag1, MASK1turn;
    
  
//  shared VIEW, QUEUE[2];       // view of the thread

  int VIEWflag0, VIEWflag1, VIEWturn;


  int QUEUE0flag0, QUEUE0flag1, QUEUE0turn;
  int QUEUE1flag0, QUEUE1flag1, QUEUE1turn;

   //BEGIN init_thread
   __ESBMC_atomic_begin();
//   AcquireSpinLock(lock);

   sim = 1;
   roundTSO = roundSC =0;
      // set the view to the shared vars
   VIEWflag0 = flag0;
   VIEWflag1 = flag1;
   VIEWturn  = turn;
      // initialize MASK0 and MASK1
   MASK0flag0 = MASK1flag0 = 0;  
   MASK0flag1 = MASK1flag1 = 0;  
   MASK0turn  = MASK1turn  = 0;

   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   //END init_thread
//NEVER CHANGE

   //flag[1] = 1;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)  
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )   
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )   
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )   
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
      
//   memory_update_flag1( &ROUND, &VIEW, MASK, QUEUE, 1);
   VIEWflag1 = 1;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)  
            roundTSO=0; 
          else roundTSO++; } 
   }
   if (roundSC == roundTSO) 
      flag1 = 1;
   else{   // updating mask + queue
          if (roundTSO==0) 
             {MASK0flag1 = 1; QUEUE0flag1 = 1;} 
          if (roundTSO==1) 
             {MASK1flag1 = 1; QUEUE1flag1 = 1;} 
        }
//END memory_update_flag

   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   // turn = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)  
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0) 
         MASK0flag0 = 0; 
      if  (roundSC==1) 
         MASK1flag0 = 0;
      if  (roundSC==0) 
         MASK0flag1 = 0; 
      if  (roundSC==1) 
         MASK1flag1 = 0;
      if  (roundSC==0) 
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
//   memory_update_turn( &ROUND, &VIEW, MASK, QUEUE, 0);
   VIEWturn = 0;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)
            roundTSO=0; 
          else roundTSO++; } 
   }
   if (roundSC == roundTSO)
     turn = 0;
   else{   // updating mask + queue
          if (roundTSO==0)
             {MASK0turn = 1; QUEUE0turn = 0;} 
          if (roundTSO==1)
             {MASK1turn = 1; QUEUE1turn = 0;} 
        }
//END memory_update_turn
   if ( nondet_bool())
     {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   //fence
   __ESBMC_assume(roundTSO == roundSC);


   //while (flag[0] == 1 && turn == 0)
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
         MASK0flag0 = 0; 
      if  (roundSC==1)
         MASK1flag0 = 0;
      if  (roundSC==0)
         MASK0flag1 = 0; 
      if  (roundSC==1)
         MASK1flag1 = 0;
      if  (roundSC==0)
         MASK0turn  = 0;
      if  (roundSC==1)
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
          roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
          VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
          VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
          VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END


__ESBMC_assume ( !((VIEWflag0==1) && (VIEWturn == 0)) );


/*
   while ((VIEWflag0) && (VIEWturn == 0)){
         
      // busy wait
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
              roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
         MASK0flag0 = 0; 
      if  (roundSC==1)
         MASK1flag0 = 0;
      if  (roundSC==0)
         MASK0flag1 = 0; 
      if  (roundSC==1)
         MASK1flag1 = 0;
      if  (roundSC==0)
         MASK0turn  = 0;
      if  (roundSC==1)
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   if ( nondet_bool())
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round
      
   }
*/   
   if ( nondet_bool())
     {sim = 0;  __ESBMC_atomic_end();} //is_end_round

   // CRITICAL SECTION
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   /*__ESBMC_atomic_begin();*/
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
             roundTSO=0;
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
         MASK0flag0 = 0;
      if  (roundSC==1)
         MASK1flag0 = 0;
      if  (roundSC==0)
         MASK0flag1 = 0; 
      if  (roundSC==1)
         MASK1flag1 = 0;
      if  (roundSC==0)
         MASK0turn  = 0; 
      if  (roundSC==1)
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
          VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   cs1 = 1;
   if ( nondet_bool())
     {sim = 0;  /*__ESBMC_atomic_end();*/} //is_end_round

  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
        MASK0flag0 = 0; 
      if  (roundSC==1) 
        MASK1flag0 = 0;
      if  (roundSC==0) 
        MASK0flag1 = 0; 
      if  (roundSC==1) 
        MASK1flag1 = 0;
      if  (roundSC==0) 
        MASK0turn  = 0; 
      if  (roundSC==1) 
        MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)  
        roundSC=0; else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))
        flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))
        flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))
        turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))
        flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))
        flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))
        turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
   cs1 = 0;
   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round


   // flag[1] = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   __ESBMC_atomic_begin();
      //AcquireSpinLock(lock);
      sim = 1;
         // increment roundTSO if needed
      if ( roundTSO == roundSC ) 
	      {if (roundTSO == 1)
             roundTSO=0; 
           else roundTSO++; }
         // reset the mask for the current round (roundSC)
      if  (roundSC==0)
         MASK0flag0 = 0; 
      if  (roundSC==1)
         MASK1flag0 = 0;
      if  (roundSC==0)
         MASK0flag1 = 0; 
      if  (roundSC==1)
         MASK1flag1 = 0;
      if  (roundSC==0)
         MASK0turn  = 0; 
      if  (roundSC==1) 
         MASK1turn  = 0;
         // increment roundSC
      if (roundSC == 1)
         roundSC=0; 
      else  roundSC++; 
         // updating the shared memory
      if  ((roundSC==0) && (MASK0flag0))  
         flag0 = QUEUE0flag0;
      if  ((roundSC==0) && (MASK0flag1))  
         flag1 = QUEUE0flag1;
      if  ((roundSC==0) && (MASK0turn ))  
         turn  = QUEUE0turn;
      if  ((roundSC==1) && (MASK1flag0))  
         flag0 = QUEUE1flag0;
      if  ((roundSC==1) && (MASK1flag1))  
         flag1 = QUEUE1flag1;
      if  ((roundSC==1) && (MASK1turn ))  
         turn  = QUEUE1turn;
      // rebuild the view
      if ( (!MASK0flag0)  &&  (!MASK1flag0)  )
         VIEWflag0 = flag0;
      if ( (!MASK0flag1)  &&  (!MASK1flag1)  )
         VIEWflag1 = flag1;
      if ( (!MASK0turn )  &&  (!MASK1turn )  )
         VIEWturn  = turn;
  }
  // IS_INIT_ROUND  END
//   memory_update_flag1( &ROUND, &VIEW, MASK, QUEUE, 0);
   VIEWflag1 = 0;
   while ( nondet_bool() ){ //non-deterministically increase roundTSO
       if  (!(   ( (roundTSO == 1) && (roundSC == 0) )  || ( (roundTSO+1) == roundSC )  ) )
	     {if (roundTSO == 1)
            roundTSO=0; 
          else roundTSO++; } 
   }
   if (roundSC == roundTSO)
     flag1 = 0;
   else{   // updating mask + queue
          if (roundTSO==0) 
             {MASK0flag1 = 1; QUEUE0flag1 = 0;} 
          if (roundTSO==1) 
             {MASK1flag1 = 1; QUEUE1flag1 = 0;} 
        }
//END memory_update_flag
   if ( nondet_bool()) 
      {sim = 0;  __ESBMC_atomic_end();} //is_end_round

__ESBMC_assume( 0 );

}



void* checkThread(void* arg)
{
  int t0, t1;

  /*pthread_mutex_lock(&lock);*/
   __ESBMC_atomic_begin();
   t0 = cs0;
   t1 = cs1;
   __ESBMC_atomic_end();
  /*pthread_mutex_unlock(&lock);*/

  assert( !(t0 && t1) );

  pthread_exit(NULL);
}

void main()
{
//   InitializeSpinLock(lock);
    pthread_t id0, id1, id2;
   flag0 = flag1 = cs0  = cs1  = 0;
 
//   __async_call thread0();
//   __async_call  thread1();
   pthread_create(&id0, NULL, thread0, NULL);
   pthread_create(&id1, NULL, thread1, NULL);
   pthread_create(&id2, NULL, checkThread, NULL);

}