From: Alexander Fedotov Date: Mon, 11 Apr 2016 21:19:29 +0000 (+0100) Subject: transitions update X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=19b23adb5ef3b7c6e380fe52f3535c625c117457;p=mc1516pa.git transitions update --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 4bb4910..34bcb24 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -340,25 +340,44 @@ BDD encode_rel(sokoban_screen *screen) } if (tmp_scr->tile == TARGAGENT){ //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - //relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; - //rel_enc[6] = {1, 1, 1, 1, 0, 0}; - //relvarset = sylvan_union_cube(t, relvarset, rel_enc); + 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); } } else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){ sokoban_screen *tmp_scr = get_coord(x, y, screen); sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); + xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); + int deltai = bddvar->value.var[0]; if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ - //can move + //(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){ - //can move + //(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){ - //can move + //(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){ - //can move + //(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_d->tile == TARGBOX)){ //can't move