X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=42ad6cee7c9e787d2b7c2ee5a5f7349e90a69f47;hb=313c58c1cd85852f33ff7ca7c638ccb3066d5069;hp=5ff92e1bdf8962641c452bb91f28cde9423c1818;hpb=f20e4641f467d5e4fdf761592f2e2af8daf28509;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5ff92e1..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)); } @@ -310,11 +341,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs = trs_current; //Agent Target -> Free Targagent - //(1 0 0 0 1 1 - 0 1 1 1 1 0) + //(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) + //(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,42 +567,42 @@ 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) + //(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) + //(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) + //(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) + //(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) + //(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) < 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){ - uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { - uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + 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)); } @@ -585,35 +614,35 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) 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) + //(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) + //(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) + //(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) + //(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) + //(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) + //(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)); } @@ -641,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)); } @@ -685,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)); } @@ -729,23 +758,26 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < 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)); } @@ -753,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; @@ -773,23 +807,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < 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)); } @@ -817,23 +851,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 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)); } @@ -861,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)); } @@ -905,23 +939,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < 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)); } @@ -949,24 +983,24 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //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) < 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){ - uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; + else if (deltai < i*6 && i*6 < gammai){ + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { @@ -993,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)); } @@ -1037,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)); @@ -1068,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; @@ -1118,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; @@ -1137,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; -}