modelchecker/coord.c

   1 #include <argp.h>
   2 #include <inttypes.h>
   3 #include <locale.h>
   4 #include <stdio.h>
   5 #include <stdlib.h>
   6 #include <string.h>
   7 #include <sys/time.h>
   8
   9 #ifdef HAVE_PROFILER
  10 #include <gperftools/profiler.h>
  11 #endif
  12
  13 #include <sylvan.h>
  14 #include <llmsset.h>
  15 #include <lace.h>
  16
  17 #include "coord.h"
  18 #include "sokoban.h"
  19
  20 /*
  21  * Global TODOs for now:
  22  * - update the helper maps so it is a single bimap
  23  * - make a data structure for relations
  24  * - encode relations as a set of four relations for each move
  25  */
  26
  27 typedef struct {
  28         int x;
  29         int y;
  30 } xy;
  31
  32 typedef struct {
  33         int var[3];
  34 } bddvar;
  35
  36 typedef struct {
  37         xy key;
  38         bddvar value;
  39         UT_hash_handle hh;
  40 } xy_bddvar_map;
  41
  42 typedef struct {
  43         int key;
  44         xy value;
  45         UT_hash_handle hh;
  46 } bddvar_xy_map;
  47
  48 typedef struct {
  49         xy_bddvar_map *f;
  50         bddvar_xy_map *t;
  51 } bimap;
  52
  53 typedef struct {
  54         BDD *rell;
  55         BDD *relu;
  56         BDD *relr;
  57         BDD *reld;
  58 } rels;
  59
  60 typedef struct {
  61         int *vars;
  62         int size;
  63 } variables;
  64
  65 typedef struct
  66 {
  67     BDD bdd;
  68     BDD variables;
  69 } *state;
  70
  71 typedef struct
  72 {
  73     BDD bdd;
  74     BDD variables;
  75 } *trans;
  76
  77 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
  78 {
  79         xy_bddvar_map k, *r = NULL;
  80         memset(&k, 0, sizeof(xy_bddvar_map));
  81         k.key.x = x;
  82         k.key.y = y;
  83         HASH_FIND(hh, map, &k.key, sizeof(xy), r);
  84         return r;
  85 }
  86
  87 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
  88 {
  89         bddvar_xy_map k, *r = NULL;
  90         memset(&k, 0, sizeof(bddvar_xy_map));
  91         k.key = key;
  92         HASH_FIND(hh, map, &k.key, sizeof(int), r);
  93         return r;
  94 }
  95
  96 /*
  97 xy_bddvar_map *create_xy_bddvar_map(sokoban_screen *screen)
  98 {
  99         int varcount = 0;
 100         sokoban_screen *r;
 101         xy_bddvar_map *xybdd = NULL;
 102         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 103                 xy_bddvar_map *f = NULL;
 104                 //bddvar_xy_map *t = NULL;
 105
 106                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
 107                 memset(f, 0, sizeof(xy_bddvar_map));
 108                 f->key.x = r->coord.x;
 109                 f->key.y = r->coord.y;
 110                 f->value.var[0] = varcount;
 111                 f->value.var[1] = varcount + 1;
 112                 f->value.var[2] = varcount + 2;
 113                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
 114                 varcount = varcount + 3;
 115         }
 116         return xybdd;
 117 }
 118
 119 bddvar_xy_map *create_bddvar_xy_map(sokoban_screen *screen)
 120 {
 121         int varcount = 0;
 122         sokoban_screen *r;
 123         bddvar_xy_map *bddxy = NULL;
 124         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 125                 for (int i = 0; i <3; i++){
 126                         bddvar_xy_map *f = NULL;
 127                         //bddvar_xy_map *t = NULL;
 128
 129                         f = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
 130                         memset(f, 0, sizeof(bddvar_xy_map));
 131                         f->key = varcount + i;
 132                         f->value.x = r->coord.x;
 133                         f->value.y = r->coord.y;
 134                         HASH_ADD(hh, bddxy, key, sizeof(int), f);
 135                 }
 136                 varcount = varcount + 3;
 137         }
 138         return bddxy;
 139 }
 140 */
 141
 142 bimap *create_bimap_helper(sokoban_screen *screen)
 143 {
 144         int varcount = 0;
 145         sokoban_screen *r;
 146         xy_bddvar_map *xybdd = NULL;
 147         bddvar_xy_map *bddxy = NULL;
 148         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 149                 xy_bddvar_map *f = NULL;
 150                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
 151                 memset(f, 0, sizeof(xy_bddvar_map));
 152                 f->key.x = r->coord.x;
 153                 f->key.y = r->coord.y;
 154                 f->value.var[0] = varcount;
 155                 f->value.var[1] = varcount + 1;
 156                 f->value.var[2] = varcount + 2;
 157                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
 158
 159                 for (int i = 0; i <3; i++){
 160                         bddvar_xy_map *t = NULL;
 161                         t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
 162                         memset(t, 0, sizeof(bddvar_xy_map));
 163                         t->key = varcount + i;
 164                         t->value.x = r->coord.x;
 165                         t->value.y = r->coord.y;
 166                         HASH_ADD(hh, bddxy, key, sizeof(int), t);
 167                 }
 168                 varcount = varcount + 3;
 169         }
 170         bimap *bm = NULL;
 171         bm = (bimap *)malloc(sizeof(bimap));
 172         bm->f = xybdd;
 173         bm->t = bddxy;
 174         return bm;
 175 }
 176
 177 /*
 178  * Each coordinate has three related boolean variables. The combination of those boolean variables
 179  * defines tiles:
 180  * 000: Wall
 181  * 001: Free
 182  * 010: Box
 183  * 100: Box on target
 184  * 011: Target
 185  * 101: Agent
 186  * 110: Agent on target
 187  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
 188  * tiles in the shrinked screen.
 189  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
 190  * directly in transition relations.
 191  */
 192
 193 BDD encode_screen(sokoban_screen *screen)
 194 {
 195         LACE_ME;
 196
 197         BDDVAR vars[HASH_COUNT(screen) * 3];
 198         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 199                 vars[i] = i;
 200         }
 201
 202         uint8_t st_enc[HASH_COUNT(screen) * 3];
 203
 204         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 205         BDD state;
 206         int tile_index = 0;
 207         sokoban_screen *r;
 208         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 209                 switch(r->tile){
 210                 case FREE: //001
 211                         st_enc[tile_index] = 0;
 212                         tile_index++;
 213                         st_enc[tile_index] = 0;
 214                         tile_index++;
 215                         st_enc[tile_index] = 1;
 216                         tile_index++;
 217                         break;
 218                 case WALL: //000
 219                         st_enc[tile_index] = 0;
 220                         tile_index++;
 221                         st_enc[tile_index] = 0;
 222                         tile_index++;
 223                         st_enc[tile_index] = 0;
 224                         tile_index++;
 225                         break;
 226                 case BOX: //010
 227                         st_enc[tile_index] = 0;
 228                         tile_index++;
 229                         st_enc[tile_index] = 1;
 230                         tile_index++;
 231                         st_enc[tile_index] = 0;
 232                         tile_index++;
 233                         break;
 234                 case TARGET: //011
 235                         st_enc[tile_index] = 0;
 236                         tile_index++;
 237                         st_enc[tile_index] = 1;
 238                         tile_index++;
 239                         st_enc[tile_index] = 1;
 240                         tile_index++;
 241                         break;
 242                 case AGENT: //101
 243                         st_enc[tile_index] = 1;
 244                         tile_index++;
 245                         st_enc[tile_index] = 0;
 246                         tile_index++;
 247                         st_enc[tile_index] = 1;
 248                         tile_index++;
 249                         break;
 250                 case TARGAGENT: //110
 251                         st_enc[tile_index] = 1;
 252                         tile_index++;
 253                         st_enc[tile_index] = 1;
 254                         tile_index++;
 255                         st_enc[tile_index] = 0;
 256                         tile_index++;
 257                         break;
 258                 case TARGBOX: //100
 259                         st_enc[tile_index] = 1;
 260                         tile_index++;
 261                         st_enc[tile_index] = 0;
 262                         tile_index++;
 263                         st_enc[tile_index] = 0;
 264                         tile_index++;
 265                         break;
 266                 }
 267         }
 268         /* some testing...
 269         xy_bddvar_map *map = NULL;
 270         map = create_xy_bddvar_map(screen);
 271         xy_bddvar_map *m = getxy(1, 1, map);
 272         bddvar_xy_map *map2 = NULL;
 273         map2 = create_bddvar_xy_map(screen);
 274         bddvar_xy_map *m2 = getbdd(2, map2);
 275         printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
 276         printf("Test2: %d %d\n", m2->value.x, m2->value.y);
 277         */
 278         /* some more testing...
 279         bimap *bm = NULL;
 280         bm = create_bimap_helper(screen);
 281         xy_bddvar_map *m = getxy(1, 1, bm->f);
 282         bddvar_xy_map *m2 = getbdd(2, bm->t);
 283         printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
 284         printf("Test2: %d %d\n", m2->value.x, m2->value.y);
 285         printf("%d tiles were encoded\n", tile_index);
 286         if (bm != NULL) printf ("WORKS!\n");
 287         */
 288         state = sylvan_cube(varset, st_enc);
 289         printf("Initial state encoded\n");
 290         return state;
 291 }
 292
 293 BDD encode_rel(sokoban_screen *screen)
 294 {
 295         int num_tiles;
 296         num_tiles = HASH_COUNT(screen);
 297         printf("Number of tiles: %d\n", num_tiles);
 298
 299         //left relation
 300
 301         //up relation
 302
 303         //right relation
 304
 305         //down relation
 306
 307         return sylvan_true;
 308 }