X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=42ad6cee7c9e787d2b7c2ee5a5f7349e90a69f47;hb=313c58c1cd85852f33ff7ca7c638ccb3066d5069;hp=12b428d8d62b0fd92781ed8d2683d35938ab1350;hpb=b18ff9447389e6879994f90d458b5a0e993755f3;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 12b428d..42ad6ce 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -1,22 +1,13 @@ #include -#include -#include #include #include -#include -#include - -#ifdef HAVE_PROFILER -#include -#endif - #include -#include #include #include "coord.h" #include "sokoban.h" + typedef struct { int x; int y; @@ -39,8 +30,8 @@ typedef struct { } bddvar_xy_map; typedef struct { - xy_bddvar_map f; - bddvar_xy_map t; + xy_bddvar_map *f; + bddvar_xy_map *t; } bimap; xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map) @@ -62,49 +53,58 @@ bddvar_xy_map *getbdd(int key, bddvar_xy_map *map) return r; } -xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen) + +bimap *create_bimap_helper(sokoban_screen *screen) { int varcount = 0; sokoban_screen *r; xy_bddvar_map *xybdd = NULL; + bddvar_xy_map *bddxy = 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; - printf("test!: %d %d\n", r->coord.x, 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) * 2; + t->value.x = r->coord.x; + t->value.y = r->coord.y; + HASH_ADD(hh, bddxy, key, sizeof(int), t); + } varcount = varcount + 3; } - return xybdd; + bimap *bm = NULL; + bm = (bimap *)malloc(sizeof(bimap)); + bm->f = xybdd; + bm->t = bddxy; + return bm; } -bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) +int check_xy_exists(int x, int y, bimap *bm) { - 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; + int res = 0; + if (getxy(x, y, bm->f) != NULL) res = 1; + return res; +} + +int check_space(int x, int y, direction d, int delta, bimap *bm) +{ + switch(d){ + case LEFT: x = x - delta; break; + case UP: y = y - delta; break; + case RIGHT: x = x + delta; break; + case DOWN: y = y + delta; break; } - return bddxy; + return check_xy_exists(x, y, bm); } /* @@ -122,178 +122,1010 @@ bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) * It seems that the move variable is not necessary since non-deterministic moves can be emvedded * directly in transition relations. */ - -BDD encode_screen(sokoban_screen *screen) +state *encode_screen(sokoban_screen *screen) { - BDD state = sylvan_false; - int tile_index = 0; - sokoban_screen *r; LACE_ME; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + + 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; + for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){ switch(r->tile){ - case FREE: - if (state == sylvan_false){ - state = sylvan_not(sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } + case FREE: //001 + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; - case WALL: - if (state == sylvan_false){ - state = sylvan_not(sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } + case WALL: //000 + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; - case BOX: - if (state == sylvan_false){ - state = sylvan_not(sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } + case BOX: //010 + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; - case TARGET: - if (state == sylvan_false){ - state = sylvan_not(sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } + case TARGET: //011 + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; break; - case AGENT: - if (state == sylvan_false){ - state = sylvan_ithvar(tile_index); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - } + case AGENT: //101 + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; - case TARGAGENT: - if (state == sylvan_false){ - state = sylvan_ithvar(tile_index); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } + case TARGAGENT: //110 + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; - case TARGBOX: - if (state == sylvan_false){ - state = sylvan_ithvar(tile_index); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } - else { - state = sylvan_and(state, sylvan_ithvar(tile_index)); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index))); - tile_index++; - } + case TARGBOX: //100 + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; } } - /* - xy_bddvar_map *map = NULL; - map = create_xy_bddvar_map(screen); - xy_bddvar_map *m = getxy(1, 1, map); - bddvar_xy_map *map2 = NULL; - map2 = create_bddvar_xy_map(screen); - bddvar_xy_map *m2 = getbdd(2, map2); - printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]); - printf("Test2: %d %d\n", m2->value.x, m2->value.y); - */ - printf("%d tiles were encoded\n", tile_index); - return state; + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + return fullState; } -BDD encode_rel(sokoban_screen *screen) -{ - int num_tiles; - num_tiles = HASH_COUNT(screen); - printf("Number of tiles: %d\n", num_tiles); - return sylvan_true; +state *encode_goal(sokoban_screen *screen){ + 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; + for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){ + switch(r->tile){ + case FREE: //001 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case WALL: //000 -> stays the same + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case BOX: //010 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGET: //011 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case AGENT: //101 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGAGENT: //110 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case TARGBOX: //100 -> stays the same + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + } + } + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + return fullState; } -void test() +trans_t *create_single_rel(sokoban_screen *screen, direction dir) { + LACE_ME; + 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; + } + + for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ + bddxy = getbdd(i*6, bm->t); + x = bddxy->value.x; + y = bddxy->value.y; + 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, 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, 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("Test!\n"); - BDD a = sylvan_true; - BDD b = sylvan_not(a); - if (b == sylvan_false){ - printf("BDD works!\n"); - } else { - printf("BDD does not work!\n"); } + trs_current = trs; + return trs; +} + +rels *encode_rel(sokoban_screen *screen) +{ LACE_ME; - BDD c = sylvan_ithvar(1); - if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n"); - if (sylvan_var(c) == 1) printf("Var works 2\n"); + + trans_t *tl = sylvan_false; + + //left relation + tl = create_single_rel(screen, LEFT); + trans_t *tu = create_single_rel(screen, UP); + trans_t *tr = create_single_rel(screen, RIGHT); + trans_t *td = create_single_rel(screen, DOWN); + + rels *rls = NULL; + rls = (rels *)malloc(sizeof(rels)); + rls->rell = tl; + rls->relu = tu; + rls->relr = tr; + rls->reld = td; + + return rls; }