transitions are finished

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 5a6c90a..85b1867 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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");