trans upd

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index a79254b..ca75a14 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -412,22 +412,48 @@ BDD encode_rel(sokoban_screen *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);
+                       xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
+                       int deltai = bddvar->value.var[0];
+                       //                      bddvar = getxy(x - 2, y, bm->f);
+                       //                      int gammai = bddvar->value.var[0];
                        if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
-                               //can move
+                               //(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){
-                               //can move
+                               //(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){
-                               //can move
+                               //(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){
-                               //can move
+                               //(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){
+                               //can't move
+                       }
+                       if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
+                               //can't move
                        }
-                       if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){
+                       if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
                                //can't move
                        }
-                       if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){
+                       if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> 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){