From 7164b83e001ad19d43ad5a94f8995b2d93c19abc Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Thu, 21 Apr 2016 17:52:20 +0200 Subject: [PATCH] update --- modelchecker/coord.c | 45 +++++++++++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 17 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index c59f66c..9f179c6 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,10 @@ 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)); + printf("here1\n"); + memcpy(lrd, tmp_state->lrd, sizeof(lurd_t)); + printf("here2\n"); new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'l'); @@ -279,9 +283,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 +305,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 +316,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'); @@ -333,9 +337,12 @@ 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){ + printf("Here1\n"); 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)); + printf("Here2\n"); + new_state->bdd = new; new_state->vars = init->vars; lrd = lappend(lrd, 'r'); @@ -345,9 +352,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 +375,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 +389,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'); -- 2.20.1