/*****************************************************************************
* SOURCE: This is a translation of a Pthread program from 
* the Pthread benchmarks of SV-COMP 2014.
* https://svn.sosy-lab.org/software/sv-benchmarks/tags/svcomp14/
* FILE: queue_ok_true.cvl
* DESCRIPTION:
*
* Command line execution:
* civl verify queue_ok_true.cvl
******************************************************************************/

#include <civlc.h>
#include <stdio.h>
#include <assert.h>
#include <stdlib.h>
#include "pthread.cvh"

#define SIZE	(4)
#define EMPTY	(-1)
#define FULL	(-2)
#define FALSE	(0)
#define TRUE	(1)

typedef struct {
  int element[SIZE];
  int head;
  int tail;
  int amount;
} QType;

int stored_elements[SIZE];
_Bool enqueue_flag, dequeue_flag;
pthread_mutex_t m;
QType queue;

int init(QType *q) 
{
  q->head=0;
  q->tail=0;
  q->amount=0;
}

int nondet() 
{
  return $choose_int(2);
}

int empty(QType *q) 
{
  if (q->head == q->tail) 
  { 
    printf("queue is empty\n");
    return EMPTY;
  }
  return 0;
}

int full(QType *q) 
{
  if (q->amount == SIZE) 
  {  
    printf("queue is full\n");
    return FULL;
  } 
  else
    return 0;
}

int enqueue(QType *q, int x) 
{
  q->element[q->tail] = x;
  q->amount++;
  if (q->tail == SIZE) 
  {
    q->tail = 1;
  } 
  else 
  {
    q->tail++;
  }

  return 0;
}

int dequeue(QType *q) 
{
  int x;

  x = q->element[q->head];
  q->amount--;
  if (q->head == SIZE) 
  {
    q->head = 1;
  } 
  else 
    q->head++;

  return x;
}

void *t1(void *arg) 
{
  int value, i;
  printf("1");
  pthread_mutex_lock(&m);
  if (enqueue_flag)
  {
    for(i=0; i<SIZE; i++)  
    {
      value = nondet();
      enqueue(&queue,value);
      stored_elements[i]=value;
    }
    enqueue_flag=FALSE;
    dequeue_flag=TRUE;
  }	
  pthread_mutex_unlock(&m);

  return NULL;
}

void *t2(void *arg) 
{
  int i;

  pthread_mutex_lock(&m);
  if (dequeue_flag)
  {
    for(i=0; i<SIZE; i++)  
    {
      int tmp0 = empty(&queue);
      
      if (tmp0 != EMPTY){
        int tmp1 = dequeue(&queue);
        
        if (tmp1 != stored_elements[i]) {
          $assert($false);
        }
      }
    }
    dequeue_flag=FALSE;
    enqueue_flag=TRUE;
  }
  pthread_mutex_unlock(&m);

  return NULL;
}

void main() 
{
  pthread_t id1, id2;
  
  enqueue_flag=TRUE;
  dequeue_flag=FALSE;

  init(&queue);
  pthread_mutex_init(&m, PTHREAD_MUTEX_DEFAULT);
  
  int tmp = empty(&queue);
  if (tmp != EMPTY) {
    $assert($false);
  }
  
  pthread_create(&id1, NULL, t1, &queue);
  pthread_create(&id2, NULL, t2, &queue);

  pthread_join(id1, NULL);
  pthread_join(id2, NULL);

}