on the way to path extracting

[mc1516pa.git] / modelchecker / coord.c

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;