From: Alexander Fedotov Date: Thu, 21 Apr 2016 11:41:17 +0000 (+0200) Subject: on the way to path extracting X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=9e1a2f4a73174e25df74833a362c583b1020fa71;p=mc1516pa.git on the way to path extracting --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index fa815f0..d5aceb5 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,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 --- 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 --- 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 --- 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; irell, 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");