X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=f5774a6b66ec6f3dbc07771696fd46f82e9ef133;hb=03c6e2f515f6516448ec39aa40a439b9fc20c4c8;hp=af3cebe40bce9c03dd0b1e1de0603d3a3761cfe6;hpb=5b3e2d9fac13d73c002c412ca39ae3aa4de1950a;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index af3cebe..f5774a6 100644
--- 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)