/* Filename : sync_queue_oracle.cvl
   Author   : XXX
   Created  : 2024-12-12
   Modified : 2025-01-17

   Implementation of oracle.h using a synchronous FIFO queue semantics.
   To be acceptable, all of the following must hold:

     - each enqueue operation, if not the last operation,
       must be immediately followed by a dequeue
     - for a non-stuck execution, the first operation must be enqueue
       and the number of dequeues must equal the number of enqueues
     - for a stuck execution, either the first (and only) operation
       is dequeue, or the first operation is enqueue and the last
       operation is enqueue.

   We model the behavior as an automaton with 4 states:
   start state: 0.
   state 0 is accepting for unstuck executions.
   states 1 and 2 are accepting for stuck executions.
   state 3 is a trap state and is non-accepting for stuck or unstuck.
   edges: 
     enq: 0->1
     deq: 0->2
     enq: 1->3
     deq: 1->0
     enq: 2->3
     deq: 2->3
     enq: 3->3
     deq: 3->3

   some Lab
   some division
   some institution
*/
#include "oracle.h"
#include <stdbool.h>
#include <stdlib.h>

/* The queue.  The capacity is 1.   data is -1 if empty. */
typedef struct SimpleQueue {
  T data;
  int state;
} * SimpleQueue;

void * oracle_create() {
  SimpleQueue sq = malloc(sizeof(struct SimpleQueue));
  sq->data = (int)(-1);
  sq->state = 0;
  return sq;
}

void oracle_destroy(void * o) {
  free(o);
}

void * oracle_duplicate(void * obj) {
  SimpleQueue this = (SimpleQueue)obj;
  SimpleQueue that = malloc(sizeof(struct SimpleQueue));
  that->data = this->data;
  that->state = this->state;
  return that;  
}

/* Enqueues a0.  a1 ignored.  If the queue is full, this will return
   false and set the stuck bit. */
bool oracle_add(void * o, T a0, int a1) {
  SimpleQueue sq = (SimpleQueue)o;
  if (sq->state == 0) {
    sq->data = a0;
    sq->state = 1;
    return true;
  }
  sq->state = 3; // the trap state
  return false;
}

bool oracle_contains(void * o, T a) {
  $assert(false);
}

/* Dequeues. Argument a and expect are both ignored. */
int oracle_remove(void * o, T a, int expect) {
  SimpleQueue sq = (SimpleQueue)o;
  if (sq->state == 0) {
    sq->state = 2;
    return -1;
  }
  if (sq->state == 1) {
    int result = (int)sq->data;
    sq->data = -1;
    sq->state = 0;
    return result;
  }
  sq->state = 3;
  return -1;
}

void oracle_print(void * o) {
  SimpleQueue sq = (SimpleQueue)o;
  int state = sq->state, data = sq->data;
  $print("{ ");
  if (data >= 0) $print(data, " ");
  $print("}");
  if (state == 1) $print(" [waiting for deq]");
  else if (state == 2) $print(" [stuck in deq]");
  else if (state == 3) $print(" [trapped in illegal state]");
}

bool oracle_trapped(void * o, bool stuck) {
  int state = ((SimpleQueue)o)->state;
  if (stuck)
    return state == 3;
  else
    return state >= 2;
}

/* State is accepting iff stuck == stuckStatus. */
bool oracle_accepting(void * o, bool stuck) {
  int state = ((SimpleQueue)o)->state;
  return stuck ? state==1 || state==2 : state==0;
}

#ifdef _S_QUEUE_ORACLE_TEST
#include "pointer.cvh"
int main(void) {
  void * this = oracle_create();
  oracle_add(this, 1, 10);
  oracle_print(this);
  $print("\n");
  void * that = oracle_duplicate(this);
  oracle_print(that);
  $print("\n");
  $assert($equals(this, that));
  oracle_add(this, 2, 30);
  oracle_print(this);
  $print("\n");
  oracle_print(that);
  $print("\n");
  $assert(!$equals(this, that));
  oracle_destroy(this);
  oracle_destroy(that);
}
#endif