X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=0f5a507747889a7a792c134b077afcf8656368d8;hb=0212b386d85354399a194538538c0da541e987ea;hp=12b428d8d62b0fd92781ed8d2683d35938ab1350;hpb=b18ff9447389e6879994f90d458b5a0e993755f3;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 12b428d..0f5a507 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); } /* @@ -123,177 +123,1033 @@ bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen) * directly in transition relations. */ -BDD encode_screen(sokoban_screen *screen) +state *encode_screen(sokoban_screen *screen) { - BDD state = sylvan_false; + 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; - LACE_ME; for(r=screen; r != NULL; r = (sokoban_screen *)(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; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 1; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 1; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + + st_enc[tile_index] = 1; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; 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; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; 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; + printf("Initial state encoded\n"); + return fullState; } -BDD encode_rel(sokoban_screen *screen) +//test +int countTrans(trans_t *trs); + +trans_t *create_single_rel(sokoban_screen *screen, direction dir) { - int num_tiles; - num_tiles = HASH_COUNT(screen); - printf("Number of tiles: %d\n", num_tiles); - return sylvan_true; + 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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 < 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){ + 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 && i < 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 < 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 && i < 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; + } + } + 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; } -void test() +//test +int countTrans(trans_t *trs) { + int counter = 0; + while (trs != NULL){ + counter++; + trs = trs->next_rel; + } + return counter; +} - 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"); - } +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); + + //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); + + 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; + int counter = 0; + 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; + } + printf("Trans:%d\n", counter); + return 1; }