From: Alexander Fedotov Date: Wed, 20 Apr 2016 13:15:50 +0000 (+0200) Subject: goal state encoder added X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ade8a4923d9f24713f5a84691b3ecbda6c5e7fad;p=mc1516pa.git goal state encoder added --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 0f5a507..fa815f0 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -209,8 +209,102 @@ state *encode_screen(sokoban_screen *screen) return fullState; } +state *encode_goal(sokoban_screen *screen){ + int boxes = 0; + int targets = 0; + + LACE_ME; + + BDDVAR vars[HASH_COUNT(screen) * 3]; + for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ + vars[i] = i * 2; + } + + uint8_t st_enc[HASH_COUNT(screen) * 3]; + + BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3); + BDD s; + state *fullState = NULL; + fullState = (state *)malloc(sizeof(state)); + fullState->vars.varset = varset; + fullState->vars.size = HASH_COUNT(screen) * 3; + int tile_index = 0; + sokoban_screen *r; + for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + switch(r->tile){ + case FREE: //001 -> any + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case WALL: //000 -> stays the same + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case BOX: //010 -> any + boxes++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case TARGET: //011 -> targbox + targets++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case AGENT: //101 -> any + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + st_enc[tile_index] = 2; + tile_index++; + break; + case TARGAGENT: //110 -> targbox + targets++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + case TARGBOX: //100 -> stays the same + targets++; + boxes++; + st_enc[tile_index] = 1; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + st_enc[tile_index] = 0; + tile_index++; + break; + } + } + s = sylvan_cube(varset, st_enc); + fullState->bdd = s; + printf("Goal state encoded\n"); + if (targets == 0 || (boxes != targets)) return NULL; + else return fullState; + +} + //test -int countTrans(trans_t *trs); +//int countTrans(trans_t *trs); trans_t *create_single_rel(sokoban_screen *screen, direction dir) { @@ -283,6 +377,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs = trs_current; } + else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); unsigned int deltai = bddvar->value.var[0]; @@ -293,7 +388,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)); } @@ -313,7 +408,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)); } @@ -333,7 +428,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)); } @@ -353,7 +448,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)); } @@ -373,7 +468,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)); } @@ -393,7 +488,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)); } @@ -413,7 +508,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)); } @@ -433,7 +528,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)); } @@ -450,6 +545,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) } + 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]; @@ -462,7 +558,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 +578,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 +598,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 +618,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)); } @@ -552,23 +648,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 && 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 && 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 && 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 && 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 && 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)); } @@ -597,23 +693,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 && 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 && 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 && 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 && 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 && 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 +737,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 && 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 && 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 && 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 && 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 && 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 +781,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 && 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 && 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 && 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 && 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 && 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 +825,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 && 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 && 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 && 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 && 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 && 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 +852,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 +874,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 && 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 && 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 && 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 && 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 && 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 +918,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 && 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 && 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 && 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 && 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 && 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 +962,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 && 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 && 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 && 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 && 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 && 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 +1006,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 && 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 && 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 && 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 && 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 && 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,23 +1050,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 1 1 0 1) relvarset1 = sylvan_set_fromarray(relvars1, 18); - if (i < deltai && 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 && 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 && 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 && 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 && 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)); } @@ -993,23 +1094,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 && 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 && 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 && 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 && 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 && 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,23 +1138,23 @@ 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 && 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 && 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 && 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 && 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 && 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)); } @@ -1068,6 +1169,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; } + } trs_current = trs; @@ -1100,6 +1202,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) } //test +/* int countTrans(trans_t *trs) { int counter = 0; @@ -1109,7 +1212,7 @@ int countTrans(trans_t *trs) } return counter; } - +*/ rels *encode_rel(sokoban_screen *screen) { LACE_ME; @@ -1141,7 +1244,6 @@ rels *encode_rel(sokoban_screen *screen) 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); @@ -1150,6 +1252,5 @@ int test_trans(state *s, trans_t *t) if (next == sylvan_false) printf("False\n"); t = t->next_rel; } - printf("Trans:%d\n", counter); return 1; } diff --git a/modelchecker/coord.h b/modelchecker/coord.h index 56f770f..e289045 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -34,6 +34,8 @@ rels *encode_rel(sokoban_screen *screen); int test_trans(state *s, trans_t *t); +state *encode_goal(sokoban_screen *screen); + int test_relprod(); #endif diff --git a/modelchecker/main.c b/modelchecker/main.c index 5ca9c87..38597f6 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -61,7 +61,16 @@ void solve(FILE *inputstream) state *init = encode_screen(screen); rels *rls = encode_rel(screen); - //test_trans(init, rls->reld); + /* + printf("Doing left\n"); + test_trans(init, rls->rell); + printf("Doing up\n"); + test_trans(init, rls->relu); + printf("Doing right\n"); + test_trans(init, rls->relr); + printf("Doing down\n"); + test_trans(init, rls->reld); + */ BDD old = sylvan_false; BDD new = init->bdd; @@ -71,25 +80,43 @@ void solve(FILE *inputstream) ERRPRINT("Iteration %d\n", iteration++); trans_t *t = rls->rell; + //for testing + /* + BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9); + BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0}); + BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0})); + BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1})); + if (new == teststate2) printf("Wrong!\n"); + */ while (t != NULL){ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); } + t = rls->relu; while (t != NULL){ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); } + + t = rls->relr; while (t != NULL){ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); } + + t = rls->reld; while (t != NULL){ new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); } + } ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset)); // sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);