X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=3cd3a9a7e5a3c6bf1d3e69eac7ba2b79a0b283c7;hb=d5d879b4e6dff962b6d31be06b8e555e72819963;hp=0d293b440c76fe54d4a11265441f47118da187d8;hpb=25b40ed8ebcfd9296476bb28d33a1eee064f8d91;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 0d293b4..3cd3a9a 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -17,12 +17,6 @@ #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,30 +44,6 @@ typedef struct { bddvar_xy_map *t; } bimap; -typedef struct { - BDD *rell; - BDD *relu; - BDD *relr; - BDD *reld; -} rels; - -typedef struct { - BDDSET varset; - int size; -} variables; - -typedef struct -{ - BDD bdd; - variables vars; -} *state; - -typedef struct -{ - BDD bdd; - variables varset; -} *trans; - xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map) { xy_bddvar_map k, *r = NULL; @@ -93,51 +63,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) { @@ -174,6 +99,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: @@ -190,19 +133,23 @@ bimap *create_bimap_helper(sokoban_screen *screen) * directly in transition relations. */ -BDD encode_screen(sokoban_screen *screen) +state *encode_screen(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; + vars[i] = i * 2; } uint8_t st_enc[HASH_COUNT(screen) * 3]; BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3); - BDD state; + BDD s; + state *fullState = NULL; + fullState = (state *)malloc(sizeof(state)); + fullState->vars.varset = varset; + fullState->vars.size = HASH_COUNT(screen) * 3; int tile_index = 0; sokoban_screen *r; for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ @@ -265,44 +212,1110 @@ BDD 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"); - */ - state = sylvan_cube(varset, st_enc); + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; printf("Initial state encoded\n"); - return state; + return fullState; +} + +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*3, 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 * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 6); + uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; + + 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) + relvars[0] = i * 3; + relvars[1] = i * 3 + 1; + relvars[2] = i * 3 + 2; + relvars[3] = i * 3 + 3; + relvars[4] = i * 3 + 4; + relvars[5] = i * 3 + 5; + relvarset = sylvan_set_fromarray(relvars, 6); + rel_enc[0] = 1; + rel_enc[1] = 1; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 0; + rel_enc[5] = 0; + + 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); + int deltai = bddvar->value.var[0]; + + //Free Agent -> Agent Free + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 12); + uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + 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; + + //Target Agent -> Targagent Free + //(0 1 1 1 1 0 1 0 0 0 1 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Must be: Free Targagent -> Agent Target + //(0 1 0 0 1 1 1 0 1 1 0 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 0; + rel_enc[3] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Target Targagent -> Targagent Target + //(0 1 1 1 1 0 1 0 1 1 0 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Box Agent -> Box Agent + //(0 0 1 1 0 0 1 1 0 0 1 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 0; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 0; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 1; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Targbox Agent -> Targbox Agent + //(1 1 0 0 0 0 1 1 0 0 1 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 1; + rel_enc[1] = 1; + rel_enc[2] = 0; + rel_enc[3] = 0; + rel_enc[4] = 0; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 1; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Box Targagent -> Box Targagent + //(0 0 1 1 0 0 1 1 1 1 0 0) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 0; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 0; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 1; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 0; + 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; + + //Targbox Targagent -> Targbox Targagent + //(1 1 0 0 0 0 1 1 1 1 0 0) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 1; + rel_enc[1] = 1; + rel_enc[2] = 0; + rel_enc[3] = 0; + rel_enc[4] = 0; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 1; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 0; + 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); + int deltai = bddvar->value.var[0]; + bddvar = getxy(x + xgamma, y + ygamma, bm->f); + int gammai = bddvar->value.var[0]; + + //Free Agent -> 1 0 1 0 0 1 Agent Free + //(0 1 0 0 1 1 1 0 0 0 1 1) + BDDVAR relvars[12] = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; + BDDSET relvarset = sylvan_set_fromarray(relvars, 12); + uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + 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; + + //Target Agent -> Targagent Free + //(0 1 1 1 1 0 1 0 0 0 1 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Free Targagent -> Agent Target + //(0 1 0 0 1 1 1 0 1 1 0 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 0; + rel_enc[3] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Target Targagent -> Targagent Target + //(0 1 1 1 1 0 1 0 1 1 0 1) + relvars[0] = deltai*3; + relvars[1] = deltai*3+1; + relvars[2] = deltai*3+2; + relvars[3] = deltai*3+3; + relvars[4] = deltai*3+4; + relvars[5] = deltai*3+5; + relvars[6] = i*3; + relvars[7] = i*3+1; + relvars[8] = i*3+2; + relvars[9] = i*3+3; + relvars[10] = i*3+4; + relvars[11] = i*3+5; + relvarset = sylvan_set_fromarray(relvars, 12); + rel_enc[0] = 0; + rel_enc[1] = 1; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 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 = 12; + trs_current->next_rel = trs; + trs = trs_current; + + //Box Box Agent -> Box Box Agent + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + BDDVAR relvars1[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5}; + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + BDD relvarset1 = sylvan_set_fromarray(relvars1, 18); + uint8_t rel_enc1[18]; + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 1; + rel_enc1[3] = 1; + rel_enc1[4] = 0; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 0; + rel_enc1[8] = 1; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 1; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Targbox Box Agent -> Targbox Box Agent + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + rel_enc1[0] = 1; + rel_enc1[1] = 1; + rel_enc1[2] = 0; + rel_enc1[3] = 0; + rel_enc1[4] = 0; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 0; + rel_enc1[8] = 1; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 1; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Box Box Targagent -> Box Box Targagent + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 1; + rel_enc1[3] = 1; + rel_enc1[4] = 0; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 0; + rel_enc1[8] = 1; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 1; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 0; + 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; + + //Targbox Box Targagent -> Targbox Box Targagent + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + rel_enc1[0] = 1; + rel_enc1[1] = 1; + rel_enc1[2] = 0; + rel_enc1[3] = 0; + rel_enc1[4] = 0; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 0; + rel_enc1[8] = 1; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 1; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 0; + 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; + + //Free Box Agent -> Box Agent Free + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 1; + rel_enc1[8] = 1; + rel_enc1[9] = 0; + rel_enc1[10] = 0; + rel_enc1[11] = 1; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Free Targbox Agent -> Box Targagent Free + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 1; + rel_enc1[7] = 1; + rel_enc1[8] = 0; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Target Box Agent -> Targbox Agent Free + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + rel_enc1[0] = 0; + rel_enc1[1] = 1; + rel_enc1[2] = 1; + rel_enc1[3] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 1; + rel_enc1[8] = 1; + rel_enc1[9] = 0; + rel_enc1[10] = 0; + rel_enc1[11] = 1; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Target Targbox Agent -> Targbox Targagent Free + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + rel_enc1[0] = 0; + rel_enc1[1] = 1; + rel_enc1[2] = 1; + rel_enc1[3] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 1; + rel_enc1[7] = 1; + rel_enc1[8] = 0; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 0; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 1; + 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; + + //Free Box Targagent -> Box Agent Target + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 1; + rel_enc1[8] = 1; + rel_enc1[9] = 0; + rel_enc1[10] = 0; + rel_enc1[11] = 1; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 1; + 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; + + //Free Targbox Targagent -> Box Targagent Target + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + rel_enc1[0] = 0; + rel_enc1[1] = 0; + rel_enc1[2] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 1; + rel_enc1[7] = 1; + rel_enc1[8] = 0; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 1; + 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; + + //Target Box Targagent -> Targbox Agent Target + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + rel_enc1[0] = 0; + rel_enc1[1] = 1; + rel_enc1[2] = 1; + rel_enc1[3] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 0; + rel_enc1[7] = 1; + rel_enc1[8] = 1; + rel_enc1[9] = 0; + rel_enc1[10] = 0; + rel_enc1[11] = 1; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 1; + 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; + + //Target Targbox Targagent -> Targbox Targagent Target + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + relvars1[0] = gammai*3; + relvars1[1] = gammai*3+1; + relvars1[2] = gammai*3+2; + relvars1[3] = gammai*3+3; + relvars1[4] = gammai*3+4; + relvars1[5] = gammai*3+5; + relvars1[6] = deltai*3; + relvars1[7] = deltai*3+1; + relvars1[8] = deltai*3+2; + relvars1[9] = deltai*3+3; + relvars1[10] = deltai*3+4; + relvars1[11] = deltai*3+5; + relvars1[12] = i*3; + relvars1[13] = i*3+1; + relvars1[14] = i*3+2; + relvars1[15] = i*3+3; + relvars1[16] = i*3+4; + relvars1[17] = i*3+5; + relvarset1 = sylvan_set_fromarray(relvars1, 18); + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + rel_enc1[0] = 0; + rel_enc1[1] = 1; + rel_enc1[2] = 1; + rel_enc1[3] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 0; + rel_enc1[6] = 1; + rel_enc1[7] = 1; + rel_enc1[8] = 0; + rel_enc1[9] = 1; + rel_enc1[10] = 0; + rel_enc1[11] = 0; + rel_enc1[12] = 1; + rel_enc1[13] = 0; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 1; + 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; + return trs; } -BDD encode_rel(sokoban_screen *screen) +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 rls; +} + +int +test_relprod() +{ + LACE_ME; + + BDDVAR vars[] = {0,2,4}; + BDDVAR all_vars[] = {0,1,2,3,4,5}; + BDDVAR all_vars2[] = {0,1}; + //BDDVAR short_vars[] = {0,1}; + /*BDDVAR short_vars2[] = {2,3}; + BDDVAR short_vars3[] = {0,1,2,3};*/ + + BDDSET vars_set = sylvan_set_fromarray(vars, 3); + BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6); + BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2); + //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2); + /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2); + BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/ + + BDD s, t, next, prev; + BDD zeroes, ones; + + // transition relation: 000 --> 111 and !000 --> 000 + t = sylvan_false; + t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1})); + //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); + t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0})); + // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1})); + + s = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); + zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0}); + ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); + + next = sylvan_relnext(s, t, all_vars_set); + prev = sylvan_relprev(t, next, all_vars_set); + if (next == zeroes) printf("Pass 1\n"); + if (prev == ones) printf("Pass 2\n"); + //trans *ts; + //ts = NULL; - return sylvan_true; + return 0; }