X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=63250915d82f2f3f651f497666b84bae949be66f;hb=6dc70f7da8631fd09dea07b36d582c3812beca86;hp=fa815f0a50b617e052805c579fc2abf286bd92fb;hpb=ade8a4923d9f24713f5a84691b3ecbda6c5e7fad;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index fa815f0..6325091 100644 --- 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,200 @@ 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)); + lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t)); + //state_t *new_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 = lrd; + 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)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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 = (lurd_t *)malloc(sizeof(lurd_t)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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 = (lurd_t *)malloc(sizeof(lurd_t)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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 = (lurd_t *)malloc(sizeof(lurd_t)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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 = (lurd_t *)malloc(sizeof(lurd_t)); + state_t *new_state = (state_t *)malloc(sizeof(state_t)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_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;