on the way to path extracting

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index fa815f0..d5aceb5 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,179 @@ 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;
+    lurd_t *lrd = NULL;
+    deque *state_queue = create();
+    trans_t *t = NULL;
+    state_t *tmp_state = NULL;
+    BDD visited = init->bdd;
+    BDD new;
+    tmp_state->bdd = init->bdd;
+    tmp_state->vars = init->vars;
+    tmp_state->lrd = lrd;
+    state_queue = enq(tmp_state, state_queue);
+
+    while (isEmpty(state_queue) == 1){
+        tmp_state = get_front(state_queue);
+        state_queue = deq(state_queue);
+        t = rls->rell;
+        new = sylvan_false;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        if (check_visited(new, visited, init->vars.varset) == 0){
+            if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                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;
+                state_queue = enq(new_state, state_queue);
+                visited = sylvan_or(new, visited);
+            }
+            else {
+                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;
+        new = sylvan_false;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        if (check_visited(new, visited, init->vars.varset) == 0){
+            if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                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;
+                state_queue = enq(new_state, state_queue);
+                visited = sylvan_or(new, visited);
+            }
+            else {
+                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;
+        new = sylvan_false;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        if (check_visited(new, visited, init->vars.varset) == 0){
+            if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                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;
+                state_queue = enq(new_state, state_queue);
+                visited = sylvan_or(new, visited);
+            }
+            else {
+                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;
+        new = sylvan_false;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        if (check_visited(new, visited, init->vars.varset) == 0){
+            if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                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;
+                state_queue = enq(new_state, state_queue);
+                visited = sylvan_or(new, visited);
+            }
+            else {
+                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 092bdb4..fb4a08b 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -13,12 +13,15 @@ typedef struct {
     variables vars;
 } state;
 
-typedef enum { ROOT, L, U, R, D } path_elt;
+typedef struct lurd {
+    char c;
+    struct lurd *next;
+} lurd_t;
 
 typedef struct {
     BDD bdd;
     variables vars;
-    path_elt origin;
+    lurd_t *lrd;
 } state_t;
 
 typedef struct trans {
@@ -44,6 +47,12 @@ 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);
+
 int test_relprod();
 
 #endif

diff --git a/modelchecker/deque.c b/modelchecker/deque.c
index f7546f1..bff77ed 100644 (file)
--- a/modelchecker/deque.c
+++ b/modelchecker/deque.c
@@ -41,11 +41,16 @@ deque *deq(deque *d)
 {
     node_t *front_tmp = d->front;
 
-    if (front_tmp != NULL){
+    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 if (front_tmp != NULL) {
+    else {
+        free(d->front);
         d->front = NULL;
         d->rear = NULL;
     }
@@ -55,8 +60,8 @@ deque *deq(deque *d)
 
 int isEmpty(deque *d)
 {
-    if (d->front != NULL && d->rear != NULL) return 1;
-    else return 0;
+    if (d->front != NULL && d->rear != NULL) return 0;
+    else return 1;
 }
 
 state_t *get_front(deque *d)

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 06729b1..b262660 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -28,7 +28,7 @@ void usage(char *prg)
                "\n"
                "Positional arguments:\n"
                "\tFILE  zero or one sokoban screens\n"
-               "\t      when no file is specified stdin will be used\n", prg);
+               "\t              when no file is specified stdin will be used\n", prg);
 }
 
 BDD subsolve(trans_t *t, BDD new){
@@ -48,7 +48,7 @@ int solve(FILE *inputstream, char *lurd)
 
        //Read screen
        time_start_read = clock();
-       sokoban_screen *screen = parse_screen(inputstream, true);
+       sokoban_screen *screen = parse_screen(inputstream, false);
        if (screen == NULL) {
                printf("Something went wrong encoding the screen\n");
                return 2;
@@ -83,8 +83,8 @@ int solve(FILE *inputstream, char *lurd)
        BDD old = sylvan_false;
        BDD new = init->bdd;
        //Do lurd
-       for(unsigned int i = 0; i<strlen(lurd); i++){
-               switch(lurd[i]){
+       while(*lurd != '\0'){
+               switch(*lurd){
                case 'l':
                        new = subsolve(rls->rell, new);
                        break;
@@ -98,9 +98,10 @@ int solve(FILE *inputstream, char *lurd)
                        new = subsolve(rls->reld, new);
                        break;
                default:
-                       printf("Unknown character in lucd: '%c'\n", lurd[i]);
+                       printf("Unknown character in lurd: '%c'\n", *lurd);
                        exit(2);
                }
+               lurd++;
        }
        int iteration = 0;
        bool found = false;
@@ -171,10 +172,6 @@ int main(int argc, char **argv)
        } else {
                DPRINT("Processing: %s\n", argv[optind]);
                FILE *currentfile = fopen(argv[optind], "r");
-               if(currentfile == NULL){
-                       printf("File could not be opened\n");
-                       return 2;
-               }
                DPRINT("Opening file\n");
                return solve(currentfile, lurd);
                DPRINT("Closing file\n");