From dc778bf3e3ff6ddfd4d3a86ee6838bf8dcf703d5 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 22:35:12 +0100 Subject: [PATCH] again, transitions update --- modelchecker/coord.c | 30 ++++++++++++++++++++++++++---- 1 file changed, 26 insertions(+), 4 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 34bcb24..a79254b 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -379,11 +379,33 @@ BDD encode_rel(sokoban_screen *screen) 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 + 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 == TARGAGENT && (tmp_scr_d->tile == BOX || tmp_scr_d->tile == TARGBOX)){ - //can't move + 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); } } else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){ -- 2.20.1