transitions update

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 3c14e56..4bb4910 100644 (file)
--- 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){