From: Alexander Fedotov Date: Tue, 12 Apr 2016 21:09:15 +0000 (+0100) Subject: transitions reworked X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=6a8c26fdf4e143d9009c3288659ed00bc7d88043;p=mc1516pa.git transitions reworked --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index b96eef0..e54fe56 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -218,10 +218,10 @@ state *encode_screen(sokoban_screen *screen) return fullState; } -BDD create_single_rel(sokoban_screen *screen, direction dir) +trans_t *create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; - BDD t = sylvan_false; + trans_t *trs, *trs_current; bimap *bm = create_bimap_helper(screen); int x = 0; int y = 0; @@ -230,6 +230,7 @@ BDD create_single_rel(sokoban_screen *screen, direction dir) int ydelta = 0; int xgamma = 0; int ygamma = 0; + trs = NULL; switch(dir){ case LEFT: xdelta = -1; @@ -262,241 +263,1039 @@ BDD create_single_rel(sokoban_screen *screen, direction dir) x = bddxy->value.x; y = bddxy->value.y; if (check_space(x, y, dir, 1, bm) == 0){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - if (tmp_scr->tile == 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}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT){ - //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - 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, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + + //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; + + //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){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen); + xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); int deltai = bddvar->value.var[0]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == 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}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 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, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 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, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 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, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 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, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 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] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){ - //(0 0 1 1 0 0 1 1 1 1 0 0) - 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, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){ - //(1 1 0 0 0 0 1 1 1 1 0 0) - 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] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + + //(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; + + //(0 1 1 0 1 1 1 0 0 1 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] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 0; + rel_enc[9] = 1; + 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; + + //(0 1 0 1 1 0 1 0 1 0 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] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 0; + 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; + + //(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; + + //(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; + + //(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; + + //(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; + + //(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){ - sokoban_screen *tmp_scr = get_coord(x, y, screen); - sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen); - sokoban_screen *tmp_scr_g = get_coord(x + xgamma, y + ygamma, screen); + 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]; - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == 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}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 0 1 1 1 0 0 1 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, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ - //(0 1 0 1 1 0 1 0 1 0 0 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, 1, 1, 0, 1, 0, 1, 0, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ - //(0 1 1 1 1 0 1 0 1 1 0 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, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //free box agent -> box agent free - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox agent -> box targagent free) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box agent -> targbox agent free) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox agent -> targbox targagent free) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ - //(free box targagent -> box agent target) - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ - //(free targbox targagent -> box targagent target) - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ - //(target box targagent -> targbox agent target) - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ - //(target targbox targagent -> targbox targagent target) - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - BDDVAR relvars[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}; - BDDSET relvarset = sylvan_set_fromarray(relvars, 18); - uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; - t = sylvan_union_cube(t, relvarset, rel_enc); - } + + //(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; + + //(0 1 1 0 1 1 1 0 0 1 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] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 0; + rel_enc[9] = 1; + 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; + + //(0 1 0 1 1 0 1 0 1 0 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] = 1; + rel_enc[4] = 1; + rel_enc[5] = 0; + rel_enc[6] = 1; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 0; + 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; + + //(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; + + //(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]; + 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; + + //(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); + 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; + + //(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; + + //(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; } } - return t; + trs_current = trs; + return trs; } rels *encode_rel(sokoban_screen *screen) { LACE_ME; - BDD tl = sylvan_false; + trans_t *tl = sylvan_false; //left relation tl = create_single_rel(screen, LEFT); //up relation - BDD tu = create_single_rel(screen, UP); + trans_t *tu = create_single_rel(screen, UP); //right relation - BDD tr = create_single_rel(screen, RIGHT); + trans_t *tr = create_single_rel(screen, RIGHT); //down relation - BDD td = create_single_rel(screen, DOWN); + 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; + 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 0; +} diff --git a/modelchecker/coord.h b/modelchecker/coord.h index 4ac7442..33f7e91 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -8,23 +8,22 @@ typedef struct { int size; } variables; -typedef struct -{ +typedef struct { BDD bdd; variables vars; } state; -typedef struct -{ +typedef struct trans { BDD bdd; variables varset; -} trans; + struct trans *next_rel; +} trans_t; typedef struct { - BDD *rell; - BDD *relu; - BDD *relr; - BDD *reld; + trans_t *rell; + trans_t *relu; + trans_t *relr; + trans_t *reld; } rels; typedef enum { LEFT, UP, RIGHT, DOWN } direction;