check space helper added

[mc1516pa.git] / modelchecker / coord.c

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index af3cebe..f5774a6 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -57,23 +57,6 @@ typedef struct {
        BDD *reld;
 } rels;
 
-typedef struct {
-       uint8_t *vars;
-       int size;
-} variables;
-
-typedef struct
-{
-    BDD bdd;
-    BDD variables;
-} *state;
-
-typedef struct
-{
-    BDD bdd;
-    BDD variables;
-} *trans;
-
 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
 {
        xy_bddvar_map k, *r = NULL;
@@ -174,6 +157,24 @@ bimap *create_bimap_helper(sokoban_screen *screen)
        return bm;
 }
 
+int check_xy_exists(int x, int y, bimap *bm)
+{
+       int res = 0;
+       if (getxy(x, y, bm->f) != NULL) res = 1;
+       return res;
+}
+
+int check_space(int x, int y, direction d, int delta, bimap *bm)
+{
+       switch(d){
+       case LEFT: x = x - delta; break;
+       case UP: y = y - delta; break;
+       case RIGHT: x = x + delta; break;
+       case DOWN: y = y + delta; break;
+       }
+       return check_xy_exists(x, y, bm);
+}
+
 /*
  * Each coordinate has three related boolean variables. The combination of those boolean variables
  * defines tiles:
@@ -190,7 +191,7 @@ bimap *create_bimap_helper(sokoban_screen *screen)
  * directly in transition relations.
  */
 
-BDD encode_screen(sokoban_screen *screen)
+state *encode_screen(sokoban_screen *screen)
 {
        LACE_ME;
 
@@ -202,7 +203,11 @@ BDD encode_screen(sokoban_screen *screen)
        uint8_t st_enc[HASH_COUNT(screen) * 3];
 
        BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
-       BDD state;
+       BDD s;
+       state *fullState = NULL;
+       fullState = (state *)malloc(sizeof(state));
+       fullState->vars.varset = varset;
+       fullState->vars.size = HASH_COUNT(screen) * 3;
        int tile_index = 0;
        sokoban_screen *r;
        for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
@@ -285,9 +290,10 @@ BDD encode_screen(sokoban_screen *screen)
        printf("%d tiles were encoded\n", tile_index);
        if (bm != NULL) printf ("WORKS!\n");
        */
-       state = sylvan_cube(varset, st_enc);
+       s = sylvan_cube(varset, st_enc);
+       fullState->bdd = s;
        printf("Initial state encoded\n");
-       return state;
+       return fullState;
 }
 
 BDD encode_rel(sokoban_screen *screen)