From 509bd1dfaca9df4125e648a96e0c47ef2cf054ae Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Tue, 12 Apr 2016 01:07:14 +0100 Subject: [PATCH] transitions are finished --- modelchecker/coord.c | 282 ++++++++++++++++++++++++++++++++++++++++--- modelchecker/coord.h | 9 +- modelchecker/main.c | 3 +- 3 files changed, 277 insertions(+), 17 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 5a6c90a..85b1867 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -50,13 +50,6 @@ typedef struct { bddvar_xy_map *t; } bimap; -typedef struct { - BDD *rell; - BDD *relu; - BDD *relr; - BDD *reld; -} rels; - xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map) { xy_bddvar_map k, *r = NULL; @@ -309,21 +302,270 @@ test_relprod() return 0; } -BDD encode_rel(sokoban_screen *screen) +BDD create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; - // int tile_count = 0; BDD t = sylvan_false; - //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; + int xdelta = 0; + int ydelta = 0; + int xgamma = 0; + int ygamma = 0; + switch(dir){ + case LEFT: + xdelta = -1; + ydelta = 0; + xgamma = -2; + ygamma = 0; + break; + case UP: + xdelta = 0; + ydelta = -1; + xgamma = 0; + ygamma = -2; + break; + case RIGHT: + xdelta = 1; + ydelta = 0; + xgamma = 2; + ygamma = 0; + break; + case DOWN: + xdelta = 0; + ydelta = 1; + xgamma = 0; + ygamma = 2; + break; + } + + for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ + bddxy = getbdd(i*3, bm->t); + x = bddxy->value.x; + y = bddxy->value.y; + if (check_space(x, y, dir, 1, bm) == 0){ + 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) + 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, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){ + sokoban_screen *tmp_scr = get_coord(x, y, screen); + sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen); + xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); + int deltai = bddvar->value.var[0]; + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ + //(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){ + //(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){ + //(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){ + //(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){ + //(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 == 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, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){ + sokoban_screen *tmp_scr = get_coord(x, y, screen); + sokoban_screen *tmp_scr_d = get_coord(x + xdelta, y + ydelta, screen); + sokoban_screen *tmp_scr_g = get_coord(x + xgamma, y + ygamma, screen); + xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); + int deltai = bddvar->value.var[0]; + bddvar = getxy(x + xgamma, y + ygamma, bm->f); + int gammai = bddvar->value.var[0]; + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){ + //(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){ + //(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){ + //(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){ + //(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){ + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){ + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 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_g->tile == BOX){ + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 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 == BOX && tmp_scr_g->tile == TARGBOX){ + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ + //free box agent -> box agent free + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ + //(free targbox agent -> box targagent free) + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ + //(target box agent -> targbox agent free) + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ + //(target targbox agent -> targbox targagent free) + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){ + //(free box targagent -> box agent target) + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){ + //(free targbox targagent -> box targagent target) + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){ + //(target box targagent -> targbox agent target) + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){ + //(target targbox targagent -> targbox targagent target) + //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18); + uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1}; + t = sylvan_union_cube(t, relvarset, rel_enc); + } + } + } + return t; +} + +rels *encode_rel(sokoban_screen *screen) +{ + LACE_ME; + + BDD tl = sylvan_false; //left relation + tl = create_single_rel(screen, LEFT); + /* for (unsigned int i = 0; i < HASH_COUNT(screen); i++){ printf("i:%d\n", i); bddxy = getbdd(i*3, bm->t); @@ -537,14 +779,24 @@ BDD encode_rel(sokoban_screen *screen) t = sylvan_union_cube(t, relvarset, rel_enc); } } - printf("x:%d y:%d\n", x, y); } + */ //up relation + BDD tu = create_single_rel(screen, UP); //right relation + BDD tr = create_single_rel(screen, RIGHT); //down relation + BDD td = create_single_rel(screen, DOWN); + + rels *rls = NULL; + rls = (rels *)malloc(sizeof(rels)); + rls->rell = &tl; + rls->relu = &tu; + rls->relr = &tr; + rls->reld = &td; - return sylvan_true; + return rls; } diff --git a/modelchecker/coord.h b/modelchecker/coord.h index bcab498..4ac7442 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -20,11 +20,18 @@ typedef struct variables varset; } trans; +typedef struct { + BDD *rell; + BDD *relu; + BDD *relr; + BDD *reld; +} rels; + typedef enum { LEFT, UP, RIGHT, DOWN } direction; state *encode_screen(sokoban_screen *screen); -BDD encode_rel(sokoban_screen *screen); +rels *encode_rel(sokoban_screen *screen); //int test_relprod(); diff --git a/modelchecker/main.c b/modelchecker/main.c index 7940dc9..6b1c0d4 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -61,8 +61,9 @@ void solve(FILE *inputstream) switch(strat){ case COORD: DPRINT("Encoding coordinate based\n"); - encode_screen(screen); + //encode_screen(screen); //test_relprod(); + encode_rel(screen); break; case OBJECT: DPRINT("Encoding object based\n"); -- 2.20.1