deque structure for paths added

[mc1516pa.git] / modelchecker / deque.c

diff --git a/modelchecker/deque.c b/modelchecker/deque.c
new file mode 100644 (file)
index 0000000..f7546f1
--- /dev/null
+++ b/modelchecker/deque.c
@@ -0,0 +1,66 @@
+#include <argp.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <sylvan.h>
+#include <lace.h>
+
+#include "deque.h"
+
+deque *create()
+{
+    deque *d;
+    d = (deque *)malloc(sizeof(deque));
+    d->front = NULL;
+    d->rear = NULL;
+    d->count = 0;
+
+    return d;
+}
+
+deque *enq(state_t *s, deque *d)
+{
+    if (d->rear == NULL){
+        d->rear = (node_t *)malloc(sizeof(node_t));
+        d->rear->ptr = NULL;
+        d->rear->s = s;
+        d->front = d->rear;
+    }
+    else {
+        node_t *temp = (node_t *)malloc(sizeof(node_t));
+        d->rear->ptr = temp;
+        temp->s = s;
+        temp->ptr = NULL;
+        d->rear = temp;
+    }
+    d->count++;
+
+    return d;
+}
+
+deque *deq(deque *d)
+{
+    node_t *front_tmp = d->front;
+
+    if (front_tmp != NULL){
+        front_tmp = front_tmp->ptr;
+        d->front = front_tmp;
+    }
+    else if (front_tmp != NULL) {
+        d->front = NULL;
+        d->rear = NULL;
+    }
+    d->count--;
+    return d;
+}
+
+int isEmpty(deque *d)
+{
+    if (d->front != NULL && d->rear != NULL) return 1;
+    else return 0;
+}
+
+state_t *get_front(deque *d)
+{
+    if (isEmpty(d) == 1) return d->front->s;
+    else return NULL;
+}