+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;
+}
+