From 200ca4dd45c9d01c5faa1ac532bdef66f9345918 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 12:41:46 +0100 Subject: [PATCH] encode_screen updated --- modelchecker/coord.c | 30 +++++++++--------------------- modelchecker/coord.h | 19 ++++++++++++++++++- 2 files changed, 27 insertions(+), 22 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 0d293b4..9d8b2fa 100644 --- 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 --- 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); -- 2.20.1