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