From 2a66deb4c5209c348286448afa42ebc247c70bbd Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 20:23:08 +0100 Subject: [PATCH] relations skeleton --- modelchecker/coord.c | 155 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 131 insertions(+), 24 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index f5774a6..3c14e56 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -197,7 +197,7 @@ state *encode_screen(sokoban_screen *screen) BDDVAR vars[HASH_COUNT(screen) * 3]; for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){ - vars[i] = i; + vars[i] = i * 2; } uint8_t st_enc[HASH_COUNT(screen) * 3]; @@ -270,39 +270,146 @@ state *encode_screen(sokoban_screen *screen) break; } } - /* some testing... - xy_bddvar_map *map = NULL; - map = create_xy_bddvar_map(screen); - xy_bddvar_map *m = getxy(1, 1, map); - bddvar_xy_map *map2 = NULL; - map2 = create_bddvar_xy_map(screen); - bddvar_xy_map *m2 = getbdd(2, map2); - printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]); - printf("Test2: %d %d\n", m2->value.x, m2->value.y); - */ - /* some more testing... - bimap *bm = NULL; - bm = create_bimap_helper(screen); - xy_bddvar_map *m = getxy(1, 1, bm->f); - bddvar_xy_map *m2 = getbdd(2, bm->t); - printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]); - printf("Test2: %d %d\n", m2->value.x, m2->value.y); - printf("%d tiles were encoded\n", tile_index); - if (bm != NULL) printf ("WORKS!\n"); - */ s = sylvan_cube(varset, st_enc); fullState->bdd = s; printf("Initial state encoded\n"); return fullState; } +int +test_relprod() +{ + LACE_ME; + + BDDVAR vars[] = {0,2,4}; + BDDVAR all_vars[] = {4,5}; + + BDDSET vars_set = sylvan_set_fromarray(vars, 3); + BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 2); + + 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_set, ((uint8_t[]){0,1,0,1,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_set, ((uint8_t[]){2,0,1,0,2,0})); + t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0})); + + s = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); + zeroes = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); + ones = sylvan_cube(vars_set, (uint8_t[]){0,0,1}); + + 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 || prev == zeroes) printf("Pass 2\n"); + + return 0; +} + BDD encode_rel(sokoban_screen *screen) { - int num_tiles; - num_tiles = HASH_COUNT(screen); - printf("Number of tiles: %d\n", num_tiles); + int tile_count = 0; + BDD t = sylvan_false; + BDDVAR *relvars; + 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++){ + printf("i:%d\n", i); + bddxy = getbdd(i*3, bm->t); + x = bddxy->value.x; + y = bddxy->value.y; + if (check_space(x, y, LEFT, 1, bm) == 0){ + tmp_scr = get_coord(x, y, screen); + if (tmp_scr->tile == AGENT){ + + } + if (tmp_scr->tile == TARGAGENT){ + + } + } + 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); + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ + //can move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){ + //can move + } + if (tmp_scr->tile == AGENT && (tmp_scr_d->tile == BOX || tmp_scr_d->tile == TARGBOX)){ + //can't move + } + if (tmp_scr->tile == TARGAGENT && (tmp_scr_d->tile == BOX || tmp_scr_d->tile == TARGBOX)){ + //can't move + } + } + 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); + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ + //can move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){ + //can move + } + 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)){ + //can't move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g == TARGBOX)){ + //can't move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ + //can move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ + //can move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ + //can move + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ + //can move + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ + //can move + } + } + printf("x:%d y:%d\n", x, y); + } //up relation -- 2.20.1