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

   Implementation of oracle.h using standard nonblocking set
   semantics.  None of the functions can block, so it never deadlocks.

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

/* sequence of values sorted */
typedef struct SimpleSet {
  T data[];
} * SimpleSet;

void * oracle_create() {
  SimpleSet oracle = malloc(sizeof(struct SimpleSet));
  $seq_init(&oracle->data, 0, NULL);
  return oracle;
}

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

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

/* inserts a0 in the right spot. a1 is ignored. */
bool oracle_add(void * o, T a0, int a1) {
  SimpleSet oracle = (SimpleSet)o;
  int i=0, n = $seq_length(&oracle->data);
  while (i<n && oracle->data[i] < a0) i++;
  if (i<n && oracle->data[i] == a0) return false;
  $seq_insert(&oracle->data, i, &a0, 1);
  return true;
}

bool oracle_contains(void * o, T a) {
  SimpleSet oracle = (SimpleSet)o;
  int i=0, n = $seq_length(&oracle->data);
  while (i<n && oracle->data[i] < a) i++;
  if (i<n && oracle->data[i] == a) return true;
  return false;
}

/* Removes a if present. expect is ignored. returns 0 (if a was not
   present) or 1 (if a was present). */
int oracle_remove(void * o, T a, int expect) {
  SimpleSet oracle = (SimpleSet)o;
  int i=0, n = $seq_length(&oracle->data);
  while (i<n && oracle->data[i] < a) i++;
  if (i<n && oracle->data[i] == a) {
    $seq_remove(&oracle->data, i, NULL, 1);
    return 1;
  }
  return 0;
}

void oracle_print(void * o) {
  SimpleSet oracle = (SimpleSet)o;
  int n = $seq_length(&oracle->data);
  $print("{ ");
  for (int i=0; i<n; i++)
    $print(oracle->data[i], " ");
  $print("}");
}

bool oracle_trapped(void * o, bool stuck) {
  return stuck;
}

/* If you are expecting a stuck execution, answer is "no", since this
   oracle never gets stuck.  If you are expecting a normal (non-stuck)
   execution, answer is always "yes". */
bool oracle_accepting(void * o, bool stuck) {
  return !stuck;
}

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