Merge branch 'master' of github.com:dopefishh/mc1516pa

diff --git a/modelchecker/Makefile b/modelchecker/Makefile
index 0de3de3..e284a57 100644 (file)
--- 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.c b/modelchecker/coord.c
index fa815f0..c59f66c 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -6,6 +6,7 @@
 
 #include "coord.h"
 #include "sokoban.h"
+#include "deque.h"
 
 
 typedef struct {
@@ -209,6 +210,193 @@ state *encode_screen(sokoban_screen *screen)
        return fullState;
 }
 
+lurd_t *lappend(lurd_t *l, char c){
+    lurd_t *temp_lrd = NULL;
+    if (l == NULL){
+        temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
+        temp_lrd->c = c;
+        temp_lrd->next = NULL;
+        l = temp_lrd;
+    }
+    else {
+        temp_lrd = l;
+        while (temp_lrd->next != NULL){
+            temp_lrd = temp_lrd->next;
+        }
+        temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
+        temp_lrd->next->c = c;
+        temp_lrd->next->next = NULL;
+    }
+    return l;
+}
+
+int check_goal(BDD s, BDD g, BDDSET vars){
+    LACE_ME;
+    if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
+    else return 0;
+}
+
+int check_visited(BDD s, BDD v, BDDSET vars){
+    LACE_ME;
+    if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
+    else return 0;
+}
+
+state_t *explstate(state *init, rels *rls, state *g){
+    LACE_ME;
+    deque *state_queue = create();
+    trans_t *t = NULL;
+    state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
+    BDD visited = init->bdd;
+    BDD new;
+    tmp_state->bdd = init->bdd;
+    tmp_state->vars = init->vars;
+    tmp_state->lrd = NULL;
+    state_queue = enq(tmp_state, state_queue);
+
+    while (isEmpty(state_queue) == 0){
+        tmp_state = get_front(state_queue);
+        state_queue = deq(state_queue);
+        new = tmp_state->bdd;
+        t = rls->rell;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    lrd = tmp_state->lrd;
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'l');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'l');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+        t = rls->relu;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    lrd = tmp_state->lrd;
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'u');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'u');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+        t = rls->relr;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    lrd = tmp_state->lrd;
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'r');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'r');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+
+        t = rls->reld;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    lrd = tmp_state->lrd;
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'd');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = tmp_state->lrd;
+                    state_t *new_state = NULL;
+                    new_state = (state_t*)malloc(sizeof(state_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'd');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+
+    }
+
+    return NULL;
+}
+
 state *encode_goal(sokoban_screen *screen){
     int boxes = 0;
     int targets = 0;

diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index e289045..014579f 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -13,6 +13,17 @@ typedef struct {
     variables vars;
 } state;
 
+typedef struct lurd {
+    char c;
+    struct lurd *next;
+} lurd_t;
+
+typedef struct {
+    BDD bdd;
+    variables vars;
+    lurd_t *lrd;
+} state_t;
+
 typedef struct trans {
     BDD bdd;
     variables varset;
@@ -36,6 +47,14 @@ int test_trans(state *s, trans_t *t);
 
 state *encode_goal(sokoban_screen *screen);
 
+int check_goal(BDD s, BDD g, BDDSET vars);
+
+int check_visited(BDD s, BDD v, BDDSET vars);
+
+lurd_t *lappend(lurd_t *l, char c);
+
+state_t *explstate(state *init, rels *rls, state *g);
+
 int test_relprod();
 
 #endif

diff --git a/modelchecker/deque.c b/modelchecker/deque.c
new file mode 100644 (file)
index 0000000..12ad6fc
--- /dev/null
+++ b/modelchecker/deque.c
@@ -0,0 +1,71 @@
+#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){
+        return d;
+    }
+    else if (front_tmp->ptr != NULL){
+        front_tmp = front_tmp->ptr;
+        free(d->front);
+        d->front = front_tmp;
+    }
+    else {
+        free(d->front);
+        d->front = NULL;
+        d->rear = NULL;
+    }
+    d->count--;
+    return d;
+}
+
+int isEmpty(deque *d)
+{
+    if (d->front != NULL && d->rear != NULL) return 0;
+    else return 1;
+}
+
+state_t *get_front(deque *d)
+{
+    if (isEmpty(d) == 0) return d->front->s;
+    else return NULL;
+}

diff --git a/modelchecker/deque.h b/modelchecker/deque.h
new file mode 100644 (file)
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

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 1f518eb..0b0067b 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -77,10 +77,9 @@ int solve(FILE *inputstream, char *lurd)
        rels *rls = encode_rel(screen);
        time_end_rel = clock();
 
-
        //Actually solve
        time_start_solve = clock();
-       BDD old = sylvan_false;
+       //BDD old = sylvan_false;
        BDD new = init->bdd;
        //Do lurd
        while(*lurd != '\0'){
@@ -98,13 +97,15 @@ int solve(FILE *inputstream, char *lurd)
                        new = subsolve(rls->reld, new);
                        break;
                default:
-                       printf("Unknown character in lucd: '%c'\n", *lurd);
+                       printf("Unknown character in lurd: '%c'\n", *lurd);
                        exit(2);
                }
                lurd++;
        }
-       int iteration = 0;
+       //int iteration = 0;
+
        bool found = false;
+    /*
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
                old = new;
@@ -119,6 +120,23 @@ int solve(FILE *inputstream, char *lurd)
                new = subsolve(rls->relr, new);
                new = subsolve(rls->reld, new);
        }
+    */
+    state_t *res = NULL;
+    state *cont = (state *)malloc(sizeof(cont));
+    cont->bdd = new;
+    cont->vars = init->vars;
+    res = explstate(cont, rls, goal);
+    if (res != NULL){
+        if (res->lrd == NULL) printf("wrong\n");
+        lurd_t *l = res->lrd;
+        while (l != NULL){
+            printf("%c", l->c);
+            l = l->next;
+        }
+        printf("\n");
+    } else found = 0;
+
+
        time_end_solve = clock();
 
        //Free and print stats

diff --git a/modelchecker/sokoban.c b/modelchecker/sokoban.c
index fd268c0..e5dfd9c 100644 (file)
--- a/modelchecker/sokoban.c
+++ b/modelchecker/sokoban.c
@@ -126,6 +126,11 @@ sokoban_screen *parse_screen(FILE *stream, bool safe)
                        x++;
                }
        }
+       if(safe == true && boxes == 0){
+               fprintf(stderr, 
+                       "Invalid screen. You need at least 1 box\n");
+               exit(1);
+       }
        if(safe == true && boxes != targets){
                fprintf(stderr, 
                        "Invalid screen. Boxes: %d, Targets: %d\n", boxes, targets);