/*****************************************************************************
* 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: fib_bench_false.cvl
* DESCRIPTION: 
*   Simple program of threads interacting which causes an error when
*   their total reaches a certain value. The fix simply involves changing the output
*   for which an error will be caused; specifically, here error is caused when i or j
*   >=144, the fix has i or j > 144.
* Command line execution:
* civl verify -inputSIZE=5 queue_false.cvl
******************************************************************************/

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

$input int SIZE;
#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 mutex;
QType queue;

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

int empty(QType *q) 
{
  if (q->head == q->tail) 
  { 
    printf("queue is empty\n");
    return EMPTY;
  }
  else 
    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;

  pthread_mutex_lock(&mutex);
  value = 0;
  int tmp = enqueue(&queue,value);
  printf("0");
  if (tmp) {
    $assert($false);
  }

  stored_elements[0]=value;
  int tmp1 = empty(&queue); 
  if (tmp1) {
    $assert($false);
  }

  pthread_mutex_unlock(&mutex);

  for(i=0; i<(SIZE-1); i++)  
  {
    pthread_mutex_lock(&mutex);
    printf("1");
    if (enqueue_flag)
    {
      value = 1;
      enqueue(&queue,value);
      stored_elements[i+1]=value;
      enqueue_flag=FALSE;
      dequeue_flag=TRUE;
    }
    pthread_mutex_unlock(&mutex);
  }	
}

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

  for(i=0; i<SIZE; i++)  
  {
    pthread_mutex_lock(&mutex);
    if (dequeue_flag)
    printf("2");
    {
      int tmp = dequeue(&queue);
      if (!tmp==stored_elements[i]) {
        $assert($false);
      }
      dequeue_flag=FALSE;
      enqueue_flag=TRUE;
    }
    pthread_mutex_unlock(&mutex);
  }

}

void main() 
{
  $proc id1, id2;

  enqueue_flag=TRUE;
  dequeue_flag=FALSE;
  
  pthread_mutex_init(&mutex, PTHREAD_MUTEX_DEFAULT);
  init(&queue);
  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);
}