X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=0f5a507747889a7a792c134b077afcf8656368d8;hb=0212b386d85354399a194538538c0da541e987ea;hp=9d8b2fac508d2f74b7f2a1ac833ad5e9fb0138b3;hpb=200ca4dd45c9d01c5faa1ac532bdef66f9345918;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 9d8b2fa..0f5a507 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -1,28 +1,12 @@ #include -#include -#include #include #include -#include -#include - -#ifdef HAVE_PROFILER -#include -#endif - #include -#include #include #include "coord.h" #include "sokoban.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 +34,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 +53,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 +66,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); @@ -157,6 +89,24 @@ bimap *create_bimap_helper(sokoban_screen *screen) return bm; } +int check_xy_exists(int x, int y, bimap *bm) +{ + 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 check_xy_exists(x, y, bm); +} + /* * Each coordinate has three related boolean variables. The combination of those boolean variables * defines tiles: @@ -179,7 +129,7 @@ state *encode_screen(sokoban_screen *screen) BDDVAR vars[HASH_COUNT(screen) * 3]; for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ - vars[i] = i; + vars[i] = i * 2; } uint8_t st_enc[HASH_COUNT(screen) * 3]; @@ -231,6 +181,7 @@ state *encode_screen(sokoban_screen *screen) tile_index++; st_enc[tile_index] = 0; tile_index++; + st_enc[tile_index] = 1; tile_index++; break; @@ -252,45 +203,953 @@ state *encode_screen(sokoban_screen *screen) break; } } - /* some testing... - 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); - */ - /* some more testing... - bimap *bm = NULL; - bm = create_bimap_helper(screen); - xy_bddvar_map *m = getxy(1, 1, bm->f); - bddvar_xy_map *m2 = getbdd(2, bm->t); - 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); - if (bm != NULL) printf ("WORKS!\n"); - */ 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) +{ + 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; +} + +//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) { - int num_tiles; - num_tiles = HASH_COUNT(screen); - printf("Number of tiles: %d\n", num_tiles); + 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); + + rels *rls = NULL; + rls = (rels *)malloc(sizeof(rels)); + rls->rell = tl; + rls->relu = tu; + rls->relr = tr; + rls->reld = td; - return sylvan_true; + 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; }