encode_screen updated

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 0d293b4..9d8b2fa 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -57,23 +57,6 @@ typedef struct {
        BDD *reld;
 } rels;
 
-typedef struct {
-       BDDSET varset;
-       int size;
-} variables;
-
-typedef struct
-{
-    BDD bdd;
-    variables vars;
-} *state;
-
-typedef struct
-{
-    BDD bdd;
-    variables varset;
-} *trans;
-
 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
 {
        xy_bddvar_map k, *r = NULL;
@@ -190,7 +173,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 +185,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 +272,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)

diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index 599b91b..bcab498 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -3,9 +3,26 @@
 
 #include "sokoban.h"
 
+typedef struct {
+       BDDSET varset;
+       int size;
+} variables;
+
+typedef struct
+{
+    BDD bdd;
+    variables vars;
+} state;
+
+typedef struct
+{
+    BDD bdd;
+    variables varset;
+} trans;
+
 typedef enum { LEFT, UP, RIGHT, DOWN } direction;
 
-BDD encode_screen(sokoban_screen *screen);
+state *encode_screen(sokoban_screen *screen);
 
 BDD encode_rel(sokoban_screen *screen);