From 556ee691ae8364a29c299b37e5709e8fd3ecc3b1 Mon Sep 17 00:00:00 2001
From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 21 Apr 2016 12:10:45 +0200
Subject: [PATCH] deque structure for paths added

---
 modelchecker/Makefile |  2 +-
 modelchecker/coord.h  |  8 ++++++
 modelchecker/deque.c  | 66 +++++++++++++++++++++++++++++++++++++++++++
 modelchecker/deque.h  | 28 ++++++++++++++++++
 4 files changed, 103 insertions(+), 1 deletion(-)
 create mode 100644 modelchecker/deque.c
 create mode 100644 modelchecker/deque.h

diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index 0de3de3..e284a57 100644
--- a/modelchecker/Makefile
+++ b/modelchecker/Makefile
@@ -1,5 +1,5 @@
 PROGRAM:=main
-OBJS:=sokoban.o coord.o object.o
+OBJS:=sokoban.o coord.o object.o deque.o
 
 CFLAGS:=-O3 -Wextra -Wall -Werror -fno-strict-aliasing -std=gnu11\
 	-I./sylvan/src
diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index e289045..092bdb4 100644
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -13,6 +13,14 @@ typedef struct {
     variables vars;
 } state;
 
+typedef enum { ROOT, L, U, R, D } path_elt;
+
+typedef struct {
+    BDD bdd;
+    variables vars;
+    path_elt origin;
+} state_t;
+
 typedef struct trans {
     BDD bdd;
     variables varset;
diff --git a/modelchecker/deque.c b/modelchecker/deque.c
new file mode 100644
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;
+}
diff --git a/modelchecker/deque.h b/modelchecker/deque.h
new file mode 100644
index 0000000..16125ea
--- /dev/null
+++ b/modelchecker/deque.h
@@ -0,0 +1,28 @@
+#ifndef DEQUE_H
+#define DEQUE_H
+#include <stdio.h>
+#include <stdbool.h>
+#include "coord.h"
+
+typedef struct node {
+    state_t *s;
+    struct node *ptr;
+} node_t;
+
+typedef struct {
+    node_t *front;
+    node_t *rear;
+    int count;
+} deque;
+
+deque *create();
+
+deque *enq(state_t *s, deque *d);
+
+deque *deq(deque *d);
+
+int isEmpty(deque *d);
+
+state_t *get_front(deque *d);
+
+#endif
-- 
2.20.1