X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=63250915d82f2f3f651f497666b84bae949be66f;hb=6dc70f7da8631fd09dea07b36d582c3812beca86;hp=5a6c90a6b6355516adde96419227a2595d5f505c;hpb=37c3344e7c8daf73cbcf72e7152dc2aeac6b5691;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5a6c90a..6325091 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -1,28 +1,13 @@ #include -#include -#include #include #include -#include -#include - -#ifdef HAVE_PROFILER -#include -#endif - #include -#include #include #include "coord.h" #include "sokoban.h" +#include "deque.h" -/* - * Global TODOs for now: - * - update the helper maps so it is a single bimap - * - make a data structure for relations - * - encode relations as a set of four relations for each move - */ typedef struct { int x; @@ -50,13 +35,6 @@ typedef struct { bddvar_xy_map *t; } bimap; -typedef struct { - BDD *rell; - BDD *relu; - BDD *relr; - BDD *reld; -} rels; - xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map) { xy_bddvar_map k, *r = NULL; @@ -76,51 +54,6 @@ bddvar_xy_map *getbdd(int key, bddvar_xy_map *map) return r; } -/* -xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen) -{ - int varcount = 0; - sokoban_screen *r; - xy_bddvar_map *xybdd = NULL; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ - xy_bddvar_map *f = NULL; - //bddvar_xy_map *t = NULL; - - f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map)); - memset(f, 0, sizeof(xy_bddvar_map)); - f->key.x = r->coord.x; - f->key.y = r->coord.y; - f->value.var[0] = varcount; - f->value.var[1] = varcount + 1; - f->value.var[2] = varcount + 2; - HASH_ADD(hh, xybdd, key, sizeof(xy), f); - varcount = varcount + 3; - } - return xybdd; -} - -bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) -{ - int varcount = 0; - sokoban_screen *r; - bddvar_xy_map *bddxy = NULL; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ - for (int i = 0; i <3; i++){ - bddvar_xy_map *f = NULL; - //bddvar_xy_map *t = NULL; - - f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map)); - memset(f, 0, sizeof(bddvar_xy_map)); - f->key = varcount + i; - f->value.x = r->coord.x; - f->value.y = r->coord.y; - HASH_ADD(hh, bddxy, key, sizeof(int), f); - } - varcount = varcount + 3; - } - return bddxy; -} -*/ bimap *create_bimap_helper(sokoban_screen *screen) { @@ -134,16 +67,16 @@ bimap *create_bimap_helper(sokoban_screen *screen) memset(f, 0, sizeof(xy_bddvar_map)); f->key.x = r->coord.x; f->key.y = r->coord.y; - f->value.var[0] = varcount; - f->value.var[1] = varcount + 1; - f->value.var[2] = varcount + 2; + f->value.var[0] = varcount * 2; + f->value.var[1] = (varcount + 1) * 2; + f->value.var[2] = (varcount + 2) * 2; HASH_ADD(hh, xybdd, key, sizeof(xy), f); for (int i = 0; i <3; i++){ bddvar_xy_map *t = NULL; t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map)); memset(t, 0, sizeof(bddvar_xy_map)); - t->key = varcount + i; + t->key = (varcount + i) * 2; t->value.x = r->coord.x; t->value.y = r->coord.y; HASH_ADD(hh, bddxy, key, sizeof(int), t); @@ -249,6 +182,7 @@ state *encode_screen(sokoban_screen *screen) tile_index++; st_enc[tile_index] = 0; tile_index++; + st_enc[tile_index] = 1; tile_index++; break; @@ -276,275 +210,1242 @@ state *encode_screen(sokoban_screen *screen) return fullState; } -int -test_relprod() -{ +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); - BDDVAR vars[] = {0,2,4}; - BDDVAR all_vars[] = {4,5}; + 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; + } + } + } - BDDSET vars_set = sylvan_set_fromarray(vars, 3); - BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 2); + 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; + } + } + } - BDD s, t, next, prev; - BDD zeroes, ones; + 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)); - // transition relation: 000 --> 111 and !000 --> 000 - t = sylvan_false; - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1,0,1,0,1})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){2,0,1,0,2,0})); - t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0})); + 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)); - s = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); - zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - ones = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); + new_state->bdd = new; + new_state->vars = init->vars; + lrd = lappend(lrd, 'r'); + new_state->lrd = lrd; + return new_state; + } + } + } - next = sylvan_relnext(s, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - if (next == zeroes) printf("Pass 1\n"); - if (prev == ones || prev == zeroes) printf("Pass 2\n"); - return 0; + 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; + + LACE_ME; + + BDDVAR vars[HASH_COUNT(screen) * 3]; + for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ + vars[i] = i * 2; + } + + uint8_t st_enc[HASH_COUNT(screen) * 3]; + + BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3); + BDD s; + state *fullState = NULL; + fullState = (state *)malloc(sizeof(state)); + fullState->vars.varset = varset; + fullState->vars.size = HASH_COUNT(screen) * 3; + int tile_index = 0; + sokoban_screen *r; + for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + switch(r->tile){ + case FREE: //001 -> any + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case WALL: //000 -> stays the same + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case BOX: //010 -> any + boxes++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case TARGET: //011 -> targbox + targets++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case AGENT: //101 -> any + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case TARGAGENT: //110 -> targbox + targets++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case TARGBOX: //100 -> stays the same + targets++; + boxes++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + } + } + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + printf("Goal state encoded\n"); + if (targets == 0 || (boxes != targets)) return NULL; + else return fullState; + } -BDD encode_rel(sokoban_screen *screen) +//test +//int countTrans(trans_t *trs); + +trans_t *create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; - // int tile_count = 0; - BDD t = sylvan_false; - //BDDVAR relvars[]; - //BDDSET relvarset; - //uint8_t rel_enc[]; - + trans_t *trs, *trs_current; bimap *bm = create_bimap_helper(screen); int x = 0; int y = 0; bddvar_xy_map *bddxy = NULL; + int xdelta = 0; + int ydelta = 0; + int xgamma = 0; + int ygamma = 0; + trs = NULL; + switch(dir){ + case LEFT: + xdelta = -1; + ydelta = 0; + xgamma = -2; + ygamma = 0; + break; + case UP: + xdelta = 0; + ydelta = -1; + xgamma = 0; + ygamma = -2; + break; + case RIGHT: + xdelta = 1; + ydelta = 0; + xgamma = 2; + ygamma = 0; + break; + case DOWN: + xdelta = 0; + ydelta = 1; + xgamma = 0; + ygamma = 2; + break; + } - //left relation for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ - printf("i:%d\n", i); - bddxy = getbdd(i*3, bm->t); + bddxy = getbdd(i*6, bm->t); x = bddxy->value.x; y = bddxy->value.y; - if (check_space(x, y, LEFT, 1, bm) == 0){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - if (tmp_scr->tile == AGENT){ - //1 1 0 0 1 1 (1 0 1 -> 1 0 1) - BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 6); - uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT){ - //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 6); - uint8_t rel_enc[6] = {1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + if (check_space(x, y, dir, 1, bm) == 0){ + //Agent -> Agent + //1 1 0 0 1 1 (1 0 1 -> 1 0 1) + BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 6); + uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 6; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent -> Targagent + //1 1 1 1 0 0 (1 1 0 -> 1 1 0) + relvarset = sylvan_set_fromarray(relvars, 6); + uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t)); + + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 6; + trs_current->next_rel = trs; + trs = trs_current; + } - else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); - xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); - int deltai = bddvar->value.var[0]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 1 1 0 0) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + + else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ + xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); + unsigned int deltai = bddvar->value.var[0]; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 12); + uint8_t rel_enc[12]; + if (i*6 < deltai){ + uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 0 0 1 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Free -> Target Agent + //(1 0 1 1 0 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 1 1 0 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Target -> Target Targagent + //(1 0 1 1 0 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 1 1 0 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Box -> Agent Box + //(1 1 0 0 1 1 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Targbox -> Agent Targbox + //(1 1 0 0 1 1 1 1 0 0 0 0) + // + //(1 1 0 0 0 0 1 1 0 0 1 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Box -> Targagent Box + //(1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Targbox -> Targagent Targbox + //(1 1 1 1 0 0 1 1 0 0 0 0) + //or + //(1 1 0 0 0 0 1 1 1 1 0 0) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + } - else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); - sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen); - xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); - int deltai = bddvar->value.var[0]; - bddvar = getxy(x - 2, y, bm->f); - int gammai = bddvar->value.var[0]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 1 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 1) - BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //free box agent -> box agent free - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox agent -> box targagent free) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box agent -> targbox agent free) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox agent -> targbox targagent free) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //(free box targagent -> box agent target) - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox targagent -> box targagent target) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box targagent -> targbox agent target) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox targagent -> targbox targagent target) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + + else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ + xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); + unsigned int deltai = bddvar->value.var[0]; + bddvar = getxy(x + xgamma, y + ygamma, bm->f); + unsigned int gammai = bddvar->value.var[0]; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 12); + uint8_t rel_enc[12]; + if (i*6 < deltai){ + uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 0 0 1 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Free -> Target Agent (LEFT || UP) + //(1 0 1 1 0 1 0 1 0 0 1 1) + //or + //(0 1 0 0 1 1 1 0 1 1 0 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; + memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Target -> Target Targagent (LEFT || UP) + //(1 0 1 1 0 1 0 1 1 1 1 0) + //or + //(0 1 1 1 1 0 1 0 1 1 0 1) + relvarset = sylvan_set_fromarray(relvars, 12); + if (i*6 < deltai){ + uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; + memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t)); + } + else { + uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset, rel_enc); + trs_current->varset.varset = relvarset; + trs_current->varset.size = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Box Box -> Agent Box Box + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) + //or + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) + BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5, gammai, gammai+1, gammai+2, gammai+3, gammai+4, gammai+5}; + BDD relvarset1 = sylvan_set_fromarray(relvars1, 18); + uint8_t rel_enc1[18]; + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Box Targbox -> Agent Box Targbox (LEFT || UP) + //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma) + //or + //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i) + //or + //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) + //or + //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta) + //or + //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma) + //or + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Box Box -> Targagent Box Box + //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP) + //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0) + //or + //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0) + //or + //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0) + //or + //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0) + //or + //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0) + //or + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Box Free -> Free Agent Box + //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) + //or + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1) + //or + //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //or + //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + + trs_current = (trans_t *)malloc(sizeof(trans_t)); + + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Targbox Free -> Free Targagent Box + //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0) + //or + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1) + //or + //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0) + //or + //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Box Target -> Free Agent Targbox + //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1) + //or + //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //or + //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Agent Targbox Target -> Free Targagent Targbox + //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1) + //or + //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0) + //or + //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Box Free -> Target Agent Box + //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0) + //or + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1) + //or + //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1) + //or + //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Targbox Free -> Target Targagent Box + //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0) + //or + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1) + //or + //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0) + //or + //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0) + //or + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Box Target -> Target Agent Targbox + //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1) + //or + //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1) + //or + //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1) + //or + //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0) + //or + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; + + //Targagent Targbox Target -> Target Targagent Targbox + //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1) + //or + //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0) + //or + //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) + //or + //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0) + relvarset1 = sylvan_set_fromarray(relvars1, 18); + if (i*6 < deltai && deltai < gammai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < gammai && gammai < i*6){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (gammai < i*6 && i*6 < deltai){ + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (i*6 < gammai && gammai < deltai){ + uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + else { + uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); + } + trs_current = (trans_t *)malloc(sizeof(trans_t)); + trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); + trs_current->varset.varset = relvarset1; + trs_current->varset.size = 18; + trs_current->next_rel = trs; + trs = trs_current; } - printf("x:%d y:%d\n", x, y); + } + trs_current = trs; + + //test + /* + switch(dir){ + case LEFT: + if (trs_current != NULL) printf("LEFT ok!\n"); + else printf ("LEFT is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case UP: + if (trs_current != NULL) printf("UP ok!\n"); + else printf ("UP is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case RIGHT: + if (trs_current != NULL) printf("RIGHT ok!\n"); + else printf ("RIGHT is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case DOWN: + if (trs_current != NULL) printf("DOWN ok!\n"); + else printf ("DOWN is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + } + */ + return trs; +} + +//test +/* +int countTrans(trans_t *trs) +{ + int counter = 0; + while (trs != NULL){ + counter++; + trs = trs->next_rel; + } + return counter; +} +*/ +rels *encode_rel(sokoban_screen *screen) +{ + LACE_ME; + + trans_t *tl = sylvan_false; + + //left relation + tl = create_single_rel(screen, LEFT); //up relation + trans_t *tu = create_single_rel(screen, UP); //right relation + trans_t *tr = create_single_rel(screen, RIGHT); //down relation + trans_t *td = create_single_rel(screen, DOWN); - return sylvan_true; + rels *rls = NULL; + rls = (rels *)malloc(sizeof(rels)); + rls->rell = tl; + rls->relu = tu; + rls->relr = tr; + rls->reld = td; + + return rls; +} + +int test_trans(state *s, trans_t *t) +{ + LACE_ME; + BDD next = sylvan_false; + while (t != NULL){ + next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset); + if (next == s->bdd) printf("Same\n"); + if (next != s->bdd && next != sylvan_false) printf("Different\n"); + if (next == sylvan_false) printf("False\n"); + t = t->next_rel; + } + return 1; }