From 2b563274d5be82064d132314c31775119fdeeb9c Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 21:16:52 +0100 Subject: [PATCH] transitions update --- modelchecker/coord.c | 38 ++++++++++++++++++++++---------------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 3c14e56..4bb4910 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -311,18 +311,17 @@ test_relprod() BDD encode_rel(sokoban_screen *screen) { - int tile_count = 0; + LACE_ME; + // int tile_count = 0; BDD t = sylvan_false; - BDDVAR *relvars; - uint8_t *rel_enc; + //BDDVAR relvars[]; + //BDDSET relvarset; + //uint8_t rel_enc[]; bimap *bm = create_bimap_helper(screen); int x = 0; int y = 0; bddvar_xy_map *bddxy = NULL; - tmp_scr *screen = NULL; - tmp_scr_d *screen = NULL; - tmp_scr_g *screen = NULL; //left relation for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ @@ -331,17 +330,24 @@ BDD encode_rel(sokoban_screen *screen) x = bddxy->value.x; y = bddxy->value.y; if (check_space(x, y, LEFT, 1, bm) == 0){ - tmp_scr = get_coord(x, y, screen); + 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) + //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); } } else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){ - tmp_scr = get_coord(x, y, screen); - tmp_scr_d = get_coord(x - 1, y, screen); + sokoban_screen *tmp_scr = get_coord(x, y, screen); + sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen); if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ //can move } @@ -362,9 +368,9 @@ BDD encode_rel(sokoban_screen *screen) } } else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){ - tmp_scr = get_coord(x, y, screen); - tmp_scr_d = get_coord(x - 1, y, screen); - tmp_scr_g = get_coord(x - 2, y, 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); if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ //can move } @@ -377,10 +383,10 @@ BDD encode_rel(sokoban_screen *screen) if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ //can move } - if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g == TARGBOX)){ + if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){ //can't move } - if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g == TARGBOX)){ + if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->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