// peterson TSO -> peterson SC   (POIROT)


#include "locks.h"
#include <stdio.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 thread0()
{
  // 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


   corral_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 ( poirot_nondet()) 
   {sim = FALSE;  
   corral_atomic_end();} //is_end_round
   

   //END init_thread
//NEVER CHANGE

   // flag[0] = 1;

  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet()) 
   {sim = 0;  corral_atomic_end();} //is_end_round

   //turn = 1;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

   //fence   
   __hv_assume(roundTSO == roundSC);


   //while (flag[1] == 1 && turn == 1)
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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


__hv_assume ( !(VIEWflag1 && VIEWturn) );

/*
   while (VIEWflag1 && VIEWturn){

      // busy wait
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

   }

*/

   if ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

   // CRITICAL SECTION
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet())
    {sim = 0;  corral_atomic_end();} //is_end_round
   
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet())
      {sim = 0;  corral_atomic_end();} //is_end_round

   //flag[0] = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round
 
__hv_assume ( 0 );
  
}


void thread1()
{
  // 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
   corral_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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

   //END init_thread
//NEVER CHANGE

   //flag[1] = 1;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

   // turn = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet())
     {sim = 0;  corral_atomic_end();} //is_end_round

   //fence
   __hv_assume(roundTSO == roundSC);


   //while (flag[0] == 1 && turn == 0)
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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


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


/*
   while ((VIEWflag0) && (VIEWturn == 0)){
         
      // busy wait
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet())
      {sim = 0;  corral_atomic_end();} //is_end_round
      
   }
*/   
   if ( poirot_nondet())
     {sim = 0;  corral_atomic_end();} //is_end_round

   // CRITICAL SECTION
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet())
     {sim = 0;  corral_atomic_end();} //is_end_round

  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round


   // flag[1] = 0;
  // IS_INIT_ROUND  BEGIN
  if ( !sim )
  {   corral_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 ( poirot_nondet() ){ //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 ( poirot_nondet()) 
      {sim = 0;  corral_atomic_end();} //is_end_round

__hv_assume ( 0 );

}


/*

void poirot_main()
{
//   InitializeSpinLock(lock);

   flag0 = flag1 = cs0  = cs1  = 0; 

   __async_call thread0();
   __async_call  thread1();
   
   corral_atomic_begin();   
   POIROT_ASSERT( !(cs0 && cs1) );
   corral_atomic_end();
}

*/

void poirot_main()
{
//   InitializeSpinLock(lock);
   int t0, t1;
 
   flag0 = flag1 = cs0  = cs1  = 0;
 
   __async_call thread0();
   __async_call  thread1();
 
   corral_atomic_begin();
   t0 = cs0;
   t1 = cs1;
   corral_atomic_end();
 
   POIROT_ASSERT( !(t0 && t1) );
}
 



void main() {}