From b0c2a1115da8abd4dc9008658a902c43bf8ba7d3 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 22:42:43 +0100 Subject: [PATCH] trans upd --- modelchecker/coord.c | 38 ++++++++++++++++++++++++++++++++------ 1 file changed, 32 insertions(+), 6 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index a79254b..ca75a14 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -412,22 +412,48 @@ BDD encode_rel(sokoban_screen *screen) sokoban_screen *tmp_scr = get_coord(x, y, screen); sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen); + xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f); + int deltai = bddvar->value.var[0]; + // bddvar = getxy(x - 2, y, bm->f); + // int gammai = 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_g->tile == BOX){ + //can't move + } + if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ + //can't move } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){ + if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){ //can't move } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){ + if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ //can't move } if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ -- 2.20.1