X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=63250915d82f2f3f651f497666b84bae949be66f;hb=6dc70f7da8631fd09dea07b36d582c3812beca86;hp=c59f66c1b5fce749f4330ff8784b089023a1ce29;hpb=cbf15c012aa6fd764ec9ea20772b6aff6457351b;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index c59f66c..6325091 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -247,11 +247,13 @@ state_t *explstate(state *init, rels *rls, state *g){ 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 = NULL; + tmp_state->lrd = lrd; state_queue = enq(tmp_state, state_queue); while (isEmpty(state_queue) == 0){ @@ -268,8 +270,8 @@ state_t *explstate(state *init, rels *rls, state *g){ 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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'l'); @@ -279,9 +281,9 @@ state_t *explstate(state *init, rels *rls, state *g){ } else { printf("GOAL\n"); - lurd_t *lrd = tmp_state->lrd; - state_t *new_state = NULL; - new_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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'l'); @@ -301,8 +303,8 @@ state_t *explstate(state *init, rels *rls, state *g){ 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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'u'); @@ -312,9 +314,9 @@ state_t *explstate(state *init, rels *rls, state *g){ } else { printf("GOAL\n"); - lurd_t *lrd = tmp_state->lrd; - state_t *new_state = NULL; - new_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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'u'); @@ -334,8 +336,9 @@ state_t *explstate(state *init, rels *rls, state *g){ 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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); + new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'r'); @@ -345,9 +348,10 @@ state_t *explstate(state *init, rels *rls, state *g){ } else { printf("GOAL\n"); - lurd_t *lrd = tmp_state->lrd; - state_t *new_state = NULL; - new_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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); + new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'r'); @@ -367,9 +371,11 @@ state_t *explstate(state *init, rels *rls, state *g){ 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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); + new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'd'); @@ -379,9 +385,10 @@ state_t *explstate(state *init, rels *rls, state *g){ } else { printf("GOAL\n"); - lurd_t *lrd = tmp_state->lrd; - state_t *new_state = NULL; - new_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)); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); + new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'd');