modelchecker/coord.c

   1 #include <argp.h>
   2 #include <stdio.h>
   3 #include <stdlib.h>
   4 #include <sylvan.h>
   5 #include <lace.h>
   6
   7 #include "coord.h"
   8 #include "sokoban.h"
   9
  10
  11 typedef struct {
  12         int x;
  13         int y;
  14 } xy;
  15
  16 typedef struct {
  17         int var[3];
  18 } bddvar;
  19
  20 typedef struct {
  21         xy key;
  22         bddvar value;
  23         UT_hash_handle hh;
  24 } xy_bddvar_map;
  25
  26 typedef struct {
  27         int key;
  28         xy value;
  29         UT_hash_handle hh;
  30 } bddvar_xy_map;
  31
  32 typedef struct {
  33         xy_bddvar_map *f;
  34         bddvar_xy_map *t;
  35 } bimap;
  36
  37 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
  38 {
  39         xy_bddvar_map k, *r = NULL;
  40         memset(&k, 0, sizeof(xy_bddvar_map));
  41         k.key.x = x;
  42         k.key.y = y;
  43         HASH_FIND(hh, map, &k.key, sizeof(xy), r);
  44         return r;
  45 }
  46
  47 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
  48 {
  49         bddvar_xy_map k, *r = NULL;
  50         memset(&k, 0, sizeof(bddvar_xy_map));
  51         k.key = key;
  52         HASH_FIND(hh, map, &k.key, sizeof(int), r);
  53         return r;
  54 }
  55
  56
  57 bimap *create_bimap_helper(sokoban_screen *screen)
  58 {
  59         int varcount = 0;
  60         sokoban_screen *r;
  61         xy_bddvar_map *xybdd = NULL;
  62         bddvar_xy_map *bddxy = NULL;
  63         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  64                 xy_bddvar_map *f = NULL;
  65                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
  66                 memset(f, 0, sizeof(xy_bddvar_map));
  67                 f->key.x = r->coord.x;
  68                 f->key.y = r->coord.y;
  69                 f->value.var[0] = varcount * 2;
  70                 f->value.var[1] = (varcount + 1) * 2;
  71                 f->value.var[2] = (varcount + 2) * 2;
  72                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
  73
  74                 for (int i = 0; i <3; i++){
  75                         bddvar_xy_map *t = NULL;
  76                         t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
  77                         memset(t, 0, sizeof(bddvar_xy_map));
  78                         t->key = (varcount + i) * 2;
  79                         t->value.x = r->coord.x;
  80                         t->value.y = r->coord.y;
  81                         HASH_ADD(hh, bddxy, key, sizeof(int), t);
  82                 }
  83                 varcount = varcount + 3;
  84         }
  85         bimap *bm = NULL;
  86         bm = (bimap *)malloc(sizeof(bimap));
  87         bm->f = xybdd;
  88         bm->t = bddxy;
  89         return bm;
  90 }
  91
  92 int check_xy_exists(int x, int y, bimap *bm)
  93 {
  94         int res = 0;
  95         if (getxy(x, y, bm->f) != NULL) res = 1;
  96         return res;
  97 }
  98
  99 int check_space(int x, int y, direction d, int delta, bimap *bm)
 100 {
 101         switch(d){
 102         case LEFT: x = x - delta; break;
 103         case UP: y = y - delta; break;
 104         case RIGHT: x = x + delta; break;
 105         case DOWN: y = y + delta; break;
 106         }
 107         return check_xy_exists(x, y, bm);
 108 }
 109
 110 /*
 111  * Each coordinate has three related boolean variables. The combination of those boolean variables
 112  * defines tiles:
 113  * 000: Wall
 114  * 001: Free
 115  * 010: Box
 116  * 100: Box on target
 117  * 011: Target
 118  * 101: Agent
 119  * 110: Agent on target
 120  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
 121  * tiles in the shrinked screen.
 122  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
 123  * directly in transition relations.
 124  */
 125 state *encode_screen(sokoban_screen *screen)
 126 {
 127         LACE_ME;
 128
 129         BDDVAR vars[HASH_COUNT(screen) * 3];
 130         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 131                 vars[i] = i * 2;
 132         }
 133
 134         uint8_t st_enc[HASH_COUNT(screen) * 3];
 135
 136         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 137         BDD s;
 138         state *fullState = NULL;
 139         fullState = (state *)malloc(sizeof(state));
 140         fullState->vars.varset = varset;
 141         fullState->vars.size = HASH_COUNT(screen) * 3;
 142         int tile_index = 0;
 143         for(sokoban_screen *r=screen; r != NULL; r = r->hh.next){
 144                 switch(r->tile){
 145                 case FREE: //001
 146                         st_enc[tile_index++] = 0;
 147                         st_enc[tile_index++] = 0;
 148                         st_enc[tile_index++] = 1;
 149                         break;
 150                 case WALL: //000
 151                         st_enc[tile_index++] = 0;
 152                         st_enc[tile_index++] = 0;
 153                         st_enc[tile_index++] = 0;
 154                         break;
 155                 case BOX: //010
 156                         st_enc[tile_index++] = 0;
 157                         st_enc[tile_index++] = 1;
 158                         st_enc[tile_index++] = 0;
 159                         break;
 160                 case TARGET: //011
 161                         st_enc[tile_index++] = 0;
 162                         st_enc[tile_index++] = 1;
 163                         st_enc[tile_index++] = 1;
 164                         break;
 165                 case AGENT: //101
 166                         st_enc[tile_index++] = 1;
 167                         st_enc[tile_index++] = 0;
 168                         st_enc[tile_index++] = 1;
 169                         break;
 170                 case TARGAGENT: //110
 171                         st_enc[tile_index++] = 1;
 172                         st_enc[tile_index++] = 1;
 173                         st_enc[tile_index++] = 0;
 174                         break;
 175                 case TARGBOX: //100
 176                         st_enc[tile_index++] = 1;
 177                         st_enc[tile_index++] = 0;
 178                         st_enc[tile_index++] = 0;
 179                         break;
 180                 }
 181         }
 182         s = sylvan_cube(varset, st_enc);
 183         fullState->bdd = s;
 184         return fullState;
 185 }
 186
 187 state *encode_goal(sokoban_screen *screen){
 188     LACE_ME;
 189
 190         BDDVAR vars[HASH_COUNT(screen) * 3];
 191         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 192                 vars[i] = i * 2;
 193         }
 194
 195         uint8_t st_enc[HASH_COUNT(screen) * 3];
 196
 197         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 198         BDD s;
 199         state *fullState = NULL;
 200         fullState = (state *)malloc(sizeof(state));
 201         fullState->vars.varset = varset;
 202         fullState->vars.size = HASH_COUNT(screen) * 3;
 203         int tile_index = 0;
 204         for(sokoban_screen *r=screen; r != NULL; r=r->hh.next){
 205                 switch(r->tile){
 206                 case FREE: //001 -> any
 207                         st_enc[tile_index++] = 2;
 208                         st_enc[tile_index++] = 2;
 209                         st_enc[tile_index++] = 2;
 210                         break;
 211                 case WALL: //000 -> stays the same
 212                         st_enc[tile_index++] = 0;
 213                         st_enc[tile_index++] = 0;
 214                         st_enc[tile_index++] = 0;
 215                         break;
 216                 case BOX: //010 -> any
 217                         st_enc[tile_index++] = 2;
 218                         st_enc[tile_index++] = 2;
 219                         st_enc[tile_index++] = 2;
 220                         break;
 221                 case TARGET: //011 -> targbox
 222                         st_enc[tile_index++] = 1;
 223                         st_enc[tile_index++] = 0;
 224                         st_enc[tile_index++] = 0;
 225                         break;
 226                 case AGENT: //101 -> any
 227                         st_enc[tile_index++] = 2;
 228                         st_enc[tile_index++] = 2;
 229                         st_enc[tile_index++] = 2;
 230                         break;
 231                 case TARGAGENT: //110 -> targbox
 232                         st_enc[tile_index++] = 1;
 233                         st_enc[tile_index++] = 0;
 234                         st_enc[tile_index++] = 0;
 235                         break;
 236                 case TARGBOX: //100 -> stays the same
 237                         st_enc[tile_index++] = 1;
 238                         st_enc[tile_index++] = 0;
 239                         st_enc[tile_index++] = 0;
 240                         break;
 241                 }
 242         }
 243         s = sylvan_cube(varset, st_enc);
 244         fullState->bdd = s;
 245         return fullState;
 246 }
 247
 248 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 249 {
 250         LACE_ME;
 251         trans_t *trs, *trs_current;
 252         bimap *bm = create_bimap_helper(screen);
 253         int x = 0;
 254         int y = 0;
 255         bddvar_xy_map *bddxy = NULL;
 256         int xdelta = 0;
 257         int ydelta = 0;
 258         int xgamma = 0;
 259         int ygamma = 0;
 260         trs = NULL;
 261         switch(dir){
 262         case LEFT:
 263                 xdelta = -1;
 264                 ydelta = 0;
 265                 xgamma = -2;
 266                 ygamma = 0;
 267                 break;
 268         case UP:
 269                 xdelta = 0;
 270                 ydelta = -1;
 271                 xgamma = 0;
 272                 ygamma = -2;
 273                 break;
 274         case RIGHT:
 275                 xdelta = 1;
 276                 ydelta = 0;
 277                 xgamma = 2;
 278                 ygamma = 0;
 279                 break;
 280         case DOWN:
 281                 xdelta = 0;
 282                 ydelta = 1;
 283                 xgamma = 0;
 284                 ygamma = 2;
 285                 break;
 286         }
 287
 288         for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
 289                 bddxy = getbdd(i*6, bm->t);
 290                 x = bddxy->value.x;
 291                 y = bddxy->value.y;
 292                 if (check_space(x, y, dir, 1, bm) == 0){
 293             //Agent -> Agent
 294                         //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
 295                         BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
 296                         BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 297                         uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
 298                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 299                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 300                         trs_current->varset.varset = relvarset;
 301                         trs_current->varset.size = 6;
 302                         trs_current->next_rel = trs;
 303                         trs = trs_current;
 304
 305             //Targagent -> Targagent
 306                         //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
 307                         relvarset = sylvan_set_fromarray(relvars, 6);
 308             uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
 309             memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
 310
 311                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 312                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 313                         trs_current->varset.varset = relvarset;
 314                         trs_current->varset.size = 6;
 315                         trs_current->next_rel = trs;
 316                         trs = trs_current;
 317
 318                 } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
 319                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 320                         unsigned int deltai = bddvar->value.var[0];
 321             //Agent Free -> Free Agent
 322             //(1 0 0 0 1 1 0 1 0 0 1 1)
 323             //or
 324             //(0 1 0 0 1 1 1 0 0 0 1 1)
 325                         BDDVAR relvars[12]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5};
 326                         BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 327             uint8_t rel_enc[12];
 328             if (i*6 < deltai){
 329                 uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
 330                 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
 331             }
 332             else {
 333                 uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 334                 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
 335             }
 336                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 337                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 338                         trs_current->varset.varset = relvarset;
 339                         trs_current->varset.size = 12;
 340                         trs_current->next_rel = trs;
 341                         trs = trs_current;
 342
 343             //Agent Target -> Free Targagent
 344             //(1 0 0 0 1 1 0 1 1 1 1 0)
 345             //or
 346             //(0 1 1 1 1 0 1 0 0 0 1 1)
 347                         relvarset = sylvan_set_fromarray(relvars, 12);
 348             if (i*6 < deltai){
 349                 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
 350                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
 351             }
 352             else {
 353                 uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 354                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
 355             }
 356                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 357                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 358                         trs_current->varset.varset = relvarset;
 359                         trs_current->varset.size = 12;
 360                         trs_current->next_rel = trs;
 361                         trs = trs_current;
 362
 363             //Targagent Free -> Target Agent
 364             //(1 0 1 1 0 1 0 1 0 0 1 1)
 365             //or
 366             //(0 1 0 0 1 1 1 0 1 1 0 1)
 367                         relvarset = sylvan_set_fromarray(relvars, 12);
 368             if (i*6 < deltai){
 369                 uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
 370                 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
 371             }
 372             else {
 373                 uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
 374                 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
 375             }
 376                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 377                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 378                         trs_current->varset.varset = relvarset;
 379                         trs_current->varset.size = 12;
 380                         trs_current->next_rel = trs;
 381                         trs = trs_current;
 382
 383             //Targagent Target -> Target Targagent
 384             //(1 0 1 1 0 1 0 1 1 1 1 0)
 385             //or
 386             //(0 1 1 1 1 0 1 0 1 1 0 1)
 387                         relvarset = sylvan_set_fromarray(relvars, 12);
 388             if (i*6 < deltai){
 389                 uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
 390                 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
 391             }
 392             else {
 393                 uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 394                 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
 395             }
 396                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 397                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 398                         trs_current->varset.varset = relvarset;
 399                         trs_current->varset.size = 12;
 400                         trs_current->next_rel = trs;
 401                         trs = trs_current;
 402
 403             //Agent Box -> Agent Box
 404             //(1 1 0 0 1 1 0 0 1 1 0 0)
 405             //or
 406             //(0 0 1 1 0 0 1 1 0 0 1 1)
 407                         relvarset = sylvan_set_fromarray(relvars, 12);
 408             if (i*6 < deltai){
 409                 uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 410                 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
 411             }
 412             else {
 413                 uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 414                 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
 415             }
 416                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 417                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 418                         trs_current->varset.varset = relvarset;
 419                         trs_current->varset.size = 12;
 420                         trs_current->next_rel = trs;
 421                         trs = trs_current;
 422
 423             //Agent Targbox -> Agent Targbox
 424             //(1 1 0 0 1 1 1 1 0 0 0 0)
 425             //
 426             //(1 1 0 0 0 0 1 1 0 0 1 1)
 427                         relvarset = sylvan_set_fromarray(relvars, 12);
 428             if (i*6 < deltai){
 429                 uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
 430                 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
 431             }
 432             else {
 433                 uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 434                 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
 435             }
 436                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 437                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 438                         trs_current->varset.varset = relvarset;
 439                         trs_current->varset.size = 12;
 440                         trs_current->next_rel = trs;
 441                         trs = trs_current;
 442
 443             //Targagent Box -> Targagent Box
 444             //(1 1 1 1 0 0 0 0 1 1 0 0)
 445             //or
 446             //(0 0 1 1 0 0 1 1 1 1 0 0)
 447                         relvarset = sylvan_set_fromarray(relvars, 12);
 448             if (i*6 < deltai){
 449                 uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 450                 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
 451             }
 452             else {
 453                 uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 454                 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
 455             }
 456                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 457                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 458                         trs_current->varset.varset = relvarset;
 459                         trs_current->varset.size = 12;
 460                         trs_current->next_rel = trs;
 461                         trs = trs_current;
 462
 463             //Targagent Targbox -> Targagent Targbox
 464             //(1 1 1 1 0 0 1 1 0 0 0 0)
 465             //or
 466             //(1 1 0 0 0 0 1 1 1 1 0 0)
 467                         relvarset = sylvan_set_fromarray(relvars, 12);
 468             if (i*6 < deltai){
 469                 uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 470                 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
 471             }
 472             else {
 473                 uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 474                 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
 475             }
 476                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 477                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 478                         trs_current->varset.varset = relvarset;
 479                         trs_current->varset.size = 12;
 480                         trs_current->next_rel = trs;
 481                         trs = trs_current;
 482                 } else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
 483                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 484                         unsigned int deltai = bddvar->value.var[0];
 485                         bddvar = getxy(x + xgamma, y + ygamma, bm->f);
 486                         unsigned int gammai = bddvar->value.var[0];
 487             //Agent Free -> Free Agent
 488                         //(1 0 0 0 1 1 0 1 0 0 1 1)
 489             //or
 490             //(0 1 0 0 1 1 1 0 0 0 1 1)
 491                         BDDVAR relvars[12]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5};
 492                         BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 493                         uint8_t rel_enc[12];
 494             if (i*6 < deltai){
 495                 uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
 496                 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
 497             }
 498             else {
 499                 uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 500                 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
 501             }
 502                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 503                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 504                         trs_current->varset.varset = relvarset;
 505                         trs_current->varset.size = 12;
 506                         trs_current->next_rel = trs;
 507                         trs = trs_current;
 508
 509             //Agent Target -> Free Targagent
 510             //(1 0 0 0 1 1 0 1 1 1 1 0)
 511             //or
 512             //(0 1 1 1 1 0 1 0 0 0 1 1)
 513                         relvarset = sylvan_set_fromarray(relvars, 12);
 514             if (i*6 < deltai){
 515                 uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
 516                 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
 517             }
 518             else {
 519                 uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 520                 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
 521             }
 522                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 523                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 524                         trs_current->varset.varset = relvarset;
 525                         trs_current->varset.size = 12;
 526                         trs_current->next_rel = trs;
 527                         trs = trs_current;
 528
 529             //Targagent Free -> Target Agent (LEFT || UP)
 530             //(1 0 1 1 0 1 0 1 0 0 1 1)
 531             //or
 532             //(0 1 0 0 1 1 1 0 1 1 0 1)
 533                         relvarset = sylvan_set_fromarray(relvars, 12);
 534             if (i*6 < deltai){
 535                 uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
 536                 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
 537             }
 538             else {
 539                 uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
 540                 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
 541             }
 542                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 543                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 544                         trs_current->varset.varset = relvarset;
 545                         trs_current->varset.size = 12;
 546                         trs_current->next_rel = trs;
 547                         trs = trs_current;
 548
 549             //Targagent Target -> Target Targagent (LEFT || UP)
 550             //(1 0 1 1 0 1 0 1 1 1 1 0)
 551             //or
 552             //(0 1 1 1 1 0 1 0 1 1 0 1)
 553                         relvarset = sylvan_set_fromarray(relvars, 12);
 554             if (i*6 < deltai){
 555                 uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
 556                 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
 557             }
 558             else {
 559                 uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 560                 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
 561             }
 562                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 563                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 564                         trs_current->varset.varset = relvarset;
 565                         trs_current->varset.size = 12;
 566                         trs_current->next_rel = trs;
 567                         trs = trs_current;
 568
 569             //Agent Box Box -> Agent Box Box
 570             //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
 571             //or
 572             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
 573             //or
 574             //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
 575             //or
 576             //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
 577             //or
 578             //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
 579             //or
 580             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
 581                         BDDVAR relvars1[18]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5, gammai, gammai+1, gammai+2, gammai+3, gammai+4, gammai+5};
 582                         BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
 583                         uint8_t rel_enc1[18];
 584             if (i*6 < deltai && deltai < gammai){
 585                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 586                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 587             }
 588             else if (deltai < gammai && gammai < i*6){
 589                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 590                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 591             }
 592             else if (gammai < i*6 && i*6 < deltai){
 593                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 594                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 595             }
 596             else if (i*6 < gammai && gammai < deltai){
 597                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 598                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 599             }
 600             else if (deltai < i*6 && i*6 < gammai){
 601                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 602                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 603             }
 604             else {
 605                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 606                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 607             }
 608
 609                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 610                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 611                         trs_current->varset.varset = relvarset1;
 612                         trs_current->varset.size = 18;
 613                         trs_current->next_rel = trs;
 614                         trs = trs_current;
 615
 616             //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
 617             //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
 618             //or
 619             //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
 620             //or
 621             //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
 622             //or
 623             //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
 624             //or
 625             //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
 626             //or
 627             //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
 628                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 629             if (i*6 < deltai && deltai < gammai){
 630                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 631                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 632             }
 633             else if (deltai < gammai && gammai < i*6){
 634                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 635                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 636             }
 637             else if (gammai < i*6 && i*6 < deltai){
 638                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 639                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 640             }
 641             else if (i*6 < gammai && gammai < deltai){
 642                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
 643                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 644             }
 645             else if (deltai < i*6 && i*6 < gammai){
 646                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
 647                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 648             }
 649             else {
 650                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 651                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 652             }
 653                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 654                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 655                         trs_current->varset.varset = relvarset1;
 656                         trs_current->varset.size = 18;
 657                         trs_current->next_rel = trs;
 658                         trs = trs_current;
 659
 660             //Targagent Box Box -> Targagent Box Box
 661                         //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
 662             //or
 663             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 664             //or
 665             //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 666             //or
 667             //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
 668             //or
 669             //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 670             //or
 671             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 672                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 673             if (i*6 < deltai && deltai < gammai){
 674                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 675                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 676             }
 677             else if (deltai < gammai && gammai < i*6){
 678                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 679                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 680             }
 681             else if (gammai < i*6 && i*6 < deltai){
 682                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 683                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 684             }
 685             else if (i*6 < gammai && gammai < deltai){
 686                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 687                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 688             }
 689             else if (deltai < i*6 && i*6 < gammai){
 690                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 691                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 692             }
 693             else {
 694                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 695                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 696             }
 697                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 698                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 699                         trs_current->varset.varset = relvarset1;
 700                         trs_current->varset.size = 18;
 701                         trs_current->next_rel = trs;
 702                         trs = trs_current;
 703
 704             //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
 705             //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
 706             //or
 707             //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
 708             //or
 709             //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 710             //or
 711             //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
 712             //or
 713             //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
 714             //or
 715             //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 716                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 717             if (i*6 < deltai && deltai < gammai){
 718                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 719                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 720             }
 721             else if (deltai < gammai && gammai < i*6){
 722                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 723                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 724             }
 725             else if (gammai < i*6 && i*6 < deltai){
 726                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 727                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 728             }
 729             else if (i*6 < gammai && gammai < deltai){
 730                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
 731                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 732             }
 733             else if (deltai < i*6 && i*6 < gammai){
 734                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 735                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 736             }
 737             else {
 738                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 739                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 740             }
 741                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 742                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 743                         trs_current->varset.varset = relvarset1;
 744                         trs_current->varset.size = 18;
 745                         trs_current->next_rel = trs;
 746                         trs = trs_current;
 747
 748                         //Agent Box Free -> Free Agent Box
 749             //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
 750             //or
 751             //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
 752             //or
 753             //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
 754             //or
 755             //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
 756             //or
 757             //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
 758             //or
 759             //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 760                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 761             if (i*6 < deltai && deltai < gammai){
 762                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
 763                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 764             }
 765
 766             else if (deltai < gammai && gammai < i*6){
 767                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 768                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 769             }
 770
 771             else if (gammai < i*6 && i*6 < deltai){
 772                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
 773                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 774             }
 775
 776             else if (i*6 < gammai && gammai < deltai){
 777                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
 778                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 779             }
 780             else if (deltai < i*6 && i*6 < gammai){
 781                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
 782                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 783             }
 784             else {
 785                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 786                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 787             }
 788
 789                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 790
 791                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 792                         trs_current->varset.varset = relvarset1;
 793                         trs_current->varset.size = 18;
 794                         trs_current->next_rel = trs;
 795                         trs = trs_current;
 796
 797                         //Agent Targbox Free -> Free Targagent Box
 798             //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
 799             //or
 800             //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
 801             //or
 802             //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
 803             //or
 804             //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
 805             //or
 806             //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
 807             //or
 808             //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 809                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 810             if (i*6 < deltai && deltai < gammai){
 811                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
 812                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 813             }
 814             else if (deltai < gammai && gammai < i*6){
 815                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 816                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 817             }
 818             else if (gammai < i*6 && i*6 < deltai){
 819                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
 820                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 821             }
 822             else if (i*6 < gammai && gammai < deltai){
 823                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
 824                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 825             }
 826             else if (deltai < i*6 && i*6 < gammai){
 827                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
 828                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 829             }
 830             else {
 831                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 832                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 833             }
 834                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 835                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 836                         trs_current->varset.varset = relvarset1;
 837                         trs_current->varset.size = 18;
 838                         trs_current->next_rel = trs;
 839                         trs = trs_current;
 840
 841                         //Agent Box Target -> Free Agent Targbox
 842             //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
 843             //or
 844             //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
 845             //or
 846             //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
 847             //or
 848             //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
 849             //or
 850             //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
 851             //or
 852             //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 853                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 854             if (i*6 < deltai && deltai < gammai){
 855                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
 856                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 857             }
 858             else if (deltai < gammai && gammai < i*6){
 859                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
 860                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 861             }
 862             else if (gammai < i*6 && i*6 < deltai){
 863                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
 864                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 865             }
 866             else if (i*6 < gammai && gammai < deltai){
 867                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
 868                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 869             }
 870             else if (deltai < i*6 && i*6 < gammai){
 871                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
 872                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 873             }
 874             else {
 875                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
 876                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 877             }
 878                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 879                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 880                         trs_current->varset.varset = relvarset1;
 881                         trs_current->varset.size = 18;
 882                         trs_current->next_rel = trs;
 883                         trs = trs_current;
 884
 885                         //Agent Targbox Target -> Free Targagent Targbox
 886             //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
 887             //or
 888             //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
 889             //or
 890             //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
 891             //or
 892             //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
 893             //or
 894             //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
 895             //or
 896             //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 897                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 898             if (i*6 < deltai && deltai < gammai){
 899                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
 900                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 901             }
 902             else if (deltai < gammai && gammai < i*6){
 903                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
 904                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 905             }
 906             else if (gammai < i*6 && i*6 < deltai){
 907                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
 908                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 909             }
 910             else if (i*6 < gammai && gammai < deltai){
 911                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
 912                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 913             }
 914             else if (deltai < i*6 && i*6 < gammai){
 915                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
 916                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 917             }
 918             else {
 919                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
 920                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 921             }
 922                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 923                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 924                         trs_current->varset.varset = relvarset1;
 925                         trs_current->varset.size = 18;
 926                         trs_current->next_rel = trs;
 927                         trs = trs_current;
 928
 929                         //Targagent Box Free -> Target Agent Box
 930             //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
 931             //or
 932             //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
 933             //or
 934             //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
 935             //or
 936             //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
 937             //or
 938             //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
 939             //or
 940             //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 941                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 942             if (i*6 < deltai && deltai < gammai){
 943                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
 944                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 945             }
 946             else if (deltai < gammai && gammai < i*6){
 947                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 948                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 949             }
 950             else if (gammai < i*6 && i*6 < deltai){
 951                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
 952                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 953             }
 954             else if (i*6 < gammai && gammai < deltai){
 955                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
 956                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 957             }
 958             else if (deltai < i*6 && i*6 < gammai){
 959                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
 960                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 961             }
 962             else {
 963                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
 964                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 965             }
 966                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 967                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 968                         trs_current->varset.varset = relvarset1;
 969                         trs_current->varset.size = 18;
 970                         trs_current->next_rel = trs;
 971                         trs = trs_current;
 972
 973                         //Targagent Targbox Free -> Target Targagent Box
 974             //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
 975             //or
 976             //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
 977             //or
 978             //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
 979             //or
 980             //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
 981             //or
 982             //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
 983             //or
 984             //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 985                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 986             if (i*6 < deltai && deltai < gammai){
 987                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
 988                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 989             }
 990             else if (deltai < gammai && gammai < i*6){
 991                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 992                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 993             }
 994             else if (gammai < i*6 && i*6 < deltai){
 995                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
 996                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 997             }
 998             else if (i*6 < gammai && gammai < deltai){
 999                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1000                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1001             }
1002             else if (deltai < i*6 && i*6 < gammai){
1003                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1004                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1005             }
1006             else {
1007                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1008                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1009             }
1010                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1011                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1012                         trs_current->varset.varset = relvarset1;
1013                         trs_current->varset.size = 18;
1014                         trs_current->next_rel = trs;
1015                         trs = trs_current;
1016
1017                         //Targagent Box Target -> Target Agent Targbox
1018             //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1019             //or
1020             //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1021             //or
1022             //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1023             //or
1024             //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1025             //or
1026             //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1027             //or
1028             //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1029                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1030             if (i*6 < deltai && deltai < gammai){
1031                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1032                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1033             }
1034             else if (deltai < gammai && gammai < i*6){
1035                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1036                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1037             }
1038             else if (gammai < i*6 && i*6 < deltai){
1039                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1040                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1041             }
1042             else if (i*6 < gammai && gammai < deltai){
1043                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1044                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1045             }
1046             else if (deltai < i*6 && i*6 < gammai){
1047                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1048                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1049             }
1050             else {
1051                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1052                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1053             }
1054                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1055                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1056                         trs_current->varset.varset = relvarset1;
1057                         trs_current->varset.size = 18;
1058                         trs_current->next_rel = trs;
1059                         trs = trs_current;
1060
1061                         //Targagent Targbox Target -> Target Targagent Targbox
1062             //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1063             //or
1064             //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1065             //or
1066             //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1067             //or
1068             //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1069             //or
1070             //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1071             //or
1072             //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1073                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1074             if (i*6 < deltai && deltai < gammai){
1075                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1076                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1077             }
1078             else if (deltai < gammai && gammai < i*6){
1079                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1080                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1081             }
1082             else if (gammai < i*6 && i*6 < deltai){
1083                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1084                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1085             }
1086             else if (i*6 < gammai && gammai < deltai){
1087                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1088                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1089             }
1090             else if (deltai < i*6 && i*6 < gammai){
1091                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1092                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1093             }
1094             else {
1095                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1096                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1097             }
1098                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1099                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1100                         trs_current->varset.varset = relvarset1;
1101                         trs_current->varset.size = 18;
1102                         trs_current->next_rel = trs;
1103                         trs = trs_current;
1104                 }
1105
1106         }
1107         trs_current = trs;
1108         return trs;
1109 }
1110
1111 rels *encode_rel(sokoban_screen *screen)
1112 {
1113         LACE_ME;
1114
1115         trans_t *tl = sylvan_false;
1116
1117         //left relation
1118         tl = create_single_rel(screen, LEFT);
1119         trans_t *tu = create_single_rel(screen, UP);
1120         trans_t *tr = create_single_rel(screen, RIGHT);
1121         trans_t *td = create_single_rel(screen, DOWN);
1122
1123         rels *rls = NULL;
1124         rls = (rels *)malloc(sizeof(rels));
1125         rls->rell = tl;
1126         rls->relu = tu;
1127         rls->relr = tr;
1128         rls->reld = td;
1129
1130         return rls;
1131 }