X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=42ad6cee7c9e787d2b7c2ee5a5f7349e90a69f47;hb=313c58c1cd85852f33ff7ca7c638ccb3066d5069;hp=7a4f545ddad1891b9f0b71164ffb072071fe84cb;hpb=9ed47a4e560dafeb43f6302bdc5fbc50665720b9;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 7a4f545..42ad6ce 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -122,7 +122,6 @@ int check_space(int x, int y, direction d, int delta, bimap *bm) * It seems that the move variable is not necessary since non-deterministic moves can be emvedded * directly in transition relations. */ - state *encode_screen(sokoban_screen *screen) { LACE_ME; @@ -141,76 +140,110 @@ state *encode_screen(sokoban_screen *screen) 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)){ + for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){ switch(r->tile){ case FREE: //001 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case WALL: //000 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; case BOX: //010 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGET: //011 - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; break; case AGENT: //101 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - - st_enc[tile_index] = 1; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 1; break; case TARGAGENT: //110 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; break; case TARGBOX: //100 - st_enc[tile_index] = 1; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; - st_enc[tile_index] = 0; - tile_index++; + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; break; } } s = sylvan_cube(varset, st_enc); fullState->bdd = s; - printf("Initial state encoded\n"); return fullState; } -//test -int countTrans(trans_t *trs); +state *encode_goal(sokoban_screen *screen){ + LACE_ME; + + BDDVAR vars[HASH_COUNT(screen) * 3]; + for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ + vars[i] = i * 2; + } + + uint8_t st_enc[HASH_COUNT(screen) * 3]; + + BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3); + BDD s; + state *fullState = NULL; + fullState = (state *)malloc(sizeof(state)); + fullState->vars.varset = varset; + fullState->vars.size = HASH_COUNT(screen) * 3; + int tile_index = 0; + for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){ + switch(r->tile){ + case FREE: //001 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case WALL: //000 -> stays the same + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case BOX: //010 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGET: //011 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case AGENT: //101 -> any + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + st_enc[tile_index++] = 2; + break; + case TARGAGENT: //110 -> targbox + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + case TARGBOX: //100 -> stays the same + st_enc[tile_index++] = 1; + st_enc[tile_index++] = 0; + st_enc[tile_index++] = 0; + break; + } + } + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + return fullState; +} trans_t *create_single_rel(sokoban_screen *screen, direction dir) { @@ -262,7 +295,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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; @@ -283,8 +315,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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){ + } 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 @@ -294,7 +325,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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){ + if (i*6 < deltai){ uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t)); } @@ -314,7 +345,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 1 1 0 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); } @@ -334,7 +365,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 0 0 1 1 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t)); } @@ -354,7 +385,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 1 1 0 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t)); } @@ -374,7 +405,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 0 1 1 0 0 1 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t)); } @@ -394,7 +425,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) // //(1 1 0 0 0 0 1 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t)); } @@ -414,7 +445,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 0 1 1 0 0 1 1 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t)); } @@ -434,7 +465,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(1 1 0 0 0 0 1 1 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t)); } @@ -448,9 +479,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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){ + } 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); @@ -462,7 +491,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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){ + if (i*6 < deltai){ uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t)); } @@ -482,7 +511,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 1 1 0 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t)); } @@ -502,7 +531,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 0 0 1 1 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t)); } @@ -522,7 +551,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //or //(0 1 1 1 1 0 1 0 1 1 0 1) relvarset = sylvan_set_fromarray(relvars, 12); - if (i < deltai){ + if (i*6 < deltai){ uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t)); } @@ -538,7 +567,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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) //(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) @@ -553,23 +581,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -598,23 +626,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -642,23 +670,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -686,23 +714,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -719,40 +747,37 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Free -> Free Agent Box //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) - //(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) - //(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) - //(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) - //(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) - //(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) - //(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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -760,7 +785,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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; @@ -769,40 +796,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Targbox Free -> Free Targagent Box //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0) - //(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) - //(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) - //(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) - //(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) - //(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) - //(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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -819,40 +840,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Target -> Free Agent Targbox //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0) - //(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) - //(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) - //(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) - //(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) - //(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) - //(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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -869,7 +884,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Targbox Target -> Free Targagent Targbox //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0) - //(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 @@ -881,23 +895,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -914,40 +928,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent Box Free -> Target Agent Box //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0) - //(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) - //(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) - //(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) - //(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) - //(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) - //(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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -964,40 +972,34 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent Targbox Free -> Target Targagent Box //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0) - //(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) - //(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) - //(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) - //(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) - //(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) - //(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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -1025,23 +1027,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -1069,28 +1071,28 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < gammai){ + if (i*6 < deltai && deltai < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < gammai) < i){ + else if (deltai < gammai && gammai < i*6){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((gammai < i) < deltai){ + else if (gammai < i*6 && i*6 < deltai){ uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((i < gammai) < deltai){ + else if (i*6 < gammai && gammai < deltai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } - else if ((deltai < i) < gammai){ + else if (deltai < i*6 && i*6 < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { - uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0}; + 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)); @@ -1100,48 +1102,12 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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) { LACE_ME; @@ -1150,14 +1116,8 @@ rels *encode_rel(sokoban_screen *screen) //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; @@ -1169,19 +1129,3 @@ rels *encode_rel(sokoban_screen *screen) 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; -}