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 #include "deque.h"
  10
  11
  12 typedef struct {
  13         int x;
  14         int y;
  15 } xy;
  16
  17 typedef struct {
  18         int var[3];
  19 } bddvar;
  20
  21 typedef struct {
  22         xy key;
  23         bddvar value;
  24         UT_hash_handle hh;
  25 } xy_bddvar_map;
  26
  27 typedef struct {
  28         int key;
  29         xy value;
  30         UT_hash_handle hh;
  31 } bddvar_xy_map;
  32
  33 typedef struct {
  34         xy_bddvar_map *f;
  35         bddvar_xy_map *t;
  36 } bimap;
  37
  38 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
  39 {
  40         xy_bddvar_map k, *r = NULL;
  41         memset(&k, 0, sizeof(xy_bddvar_map));
  42         k.key.x = x;
  43         k.key.y = y;
  44         HASH_FIND(hh, map, &k.key, sizeof(xy), r);
  45         return r;
  46 }
  47
  48 bddvar_xy_map *getbdd(int key, bddvar_xy_map *map)
  49 {
  50         bddvar_xy_map k, *r = NULL;
  51         memset(&k, 0, sizeof(bddvar_xy_map));
  52         k.key = key;
  53         HASH_FIND(hh, map, &k.key, sizeof(int), r);
  54         return r;
  55 }
  56
  57
  58 bimap *create_bimap_helper(sokoban_screen *screen)
  59 {
  60         int varcount = 0;
  61         sokoban_screen *r;
  62         xy_bddvar_map *xybdd = NULL;
  63         bddvar_xy_map *bddxy = NULL;
  64         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
  65                 xy_bddvar_map *f = NULL;
  66                 f = (xy_bddvar_map *)malloc(sizeof(xy_bddvar_map));
  67                 memset(f, 0, sizeof(xy_bddvar_map));
  68                 f->key.x = r->coord.x;
  69                 f->key.y = r->coord.y;
  70                 f->value.var[0] = varcount * 2;
  71                 f->value.var[1] = (varcount + 1) * 2;
  72                 f->value.var[2] = (varcount + 2) * 2;
  73                 HASH_ADD(hh, xybdd, key, sizeof(xy), f);
  74
  75                 for (int i = 0; i <3; i++){
  76                         bddvar_xy_map *t = NULL;
  77                         t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
  78                         memset(t, 0, sizeof(bddvar_xy_map));
  79                         t->key = (varcount + i) * 2;
  80                         t->value.x = r->coord.x;
  81                         t->value.y = r->coord.y;
  82                         HASH_ADD(hh, bddxy, key, sizeof(int), t);
  83                 }
  84                 varcount = varcount + 3;
  85         }
  86         bimap *bm = NULL;
  87         bm = (bimap *)malloc(sizeof(bimap));
  88         bm->f = xybdd;
  89         bm->t = bddxy;
  90         return bm;
  91 }
  92
  93 int check_xy_exists(int x, int y, bimap *bm)
  94 {
  95         int res = 0;
  96         if (getxy(x, y, bm->f) != NULL) res = 1;
  97         return res;
  98 }
  99
 100 int check_space(int x, int y, direction d, int delta, bimap *bm)
 101 {
 102         switch(d){
 103         case LEFT: x = x - delta; break;
 104         case UP: y = y - delta; break;
 105         case RIGHT: x = x + delta; break;
 106         case DOWN: y = y + delta; break;
 107         }
 108         return check_xy_exists(x, y, bm);
 109 }
 110
 111 /*
 112  * Each coordinate has three related boolean variables. The combination of those boolean variables
 113  * defines tiles:
 114  * 000: Wall
 115  * 001: Free
 116  * 010: Box
 117  * 100: Box on target
 118  * 011: Target
 119  * 101: Agent
 120  * 110: Agent on target
 121  * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
 122  * tiles in the shrinked screen.
 123  * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
 124  * directly in transition relations.
 125  */
 126
 127 state *encode_screen(sokoban_screen *screen)
 128 {
 129         LACE_ME;
 130
 131         BDDVAR vars[HASH_COUNT(screen) * 3];
 132         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 133                 vars[i] = i * 2;
 134         }
 135
 136         uint8_t st_enc[HASH_COUNT(screen) * 3];
 137
 138         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 139         BDD s;
 140         state *fullState = NULL;
 141         fullState = (state *)malloc(sizeof(state));
 142         fullState->vars.varset = varset;
 143         fullState->vars.size = HASH_COUNT(screen) * 3;
 144         int tile_index = 0;
 145         sokoban_screen *r;
 146         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 147                 switch(r->tile){
 148                 case FREE: //001
 149                         st_enc[tile_index] = 0;
 150                         tile_index++;
 151                         st_enc[tile_index] = 0;
 152                         tile_index++;
 153                         st_enc[tile_index] = 1;
 154                         tile_index++;
 155                         break;
 156                 case WALL: //000
 157                         st_enc[tile_index] = 0;
 158                         tile_index++;
 159                         st_enc[tile_index] = 0;
 160                         tile_index++;
 161                         st_enc[tile_index] = 0;
 162                         tile_index++;
 163                         break;
 164                 case BOX: //010
 165                         st_enc[tile_index] = 0;
 166                         tile_index++;
 167                         st_enc[tile_index] = 1;
 168                         tile_index++;
 169                         st_enc[tile_index] = 0;
 170                         tile_index++;
 171                         break;
 172                 case TARGET: //011
 173                         st_enc[tile_index] = 0;
 174                         tile_index++;
 175                         st_enc[tile_index] = 1;
 176                         tile_index++;
 177                         st_enc[tile_index] = 1;
 178                         tile_index++;
 179                         break;
 180                 case AGENT: //101
 181                         st_enc[tile_index] = 1;
 182                         tile_index++;
 183                         st_enc[tile_index] = 0;
 184                         tile_index++;
 185
 186                         st_enc[tile_index] = 1;
 187                         tile_index++;
 188                         break;
 189                 case TARGAGENT: //110
 190                         st_enc[tile_index] = 1;
 191                         tile_index++;
 192                         st_enc[tile_index] = 1;
 193                         tile_index++;
 194                         st_enc[tile_index] = 0;
 195                         tile_index++;
 196                         break;
 197                 case TARGBOX: //100
 198                         st_enc[tile_index] = 1;
 199                         tile_index++;
 200                         st_enc[tile_index] = 0;
 201                         tile_index++;
 202                         st_enc[tile_index] = 0;
 203                         tile_index++;
 204                         break;
 205                 }
 206         }
 207         s = sylvan_cube(varset, st_enc);
 208         fullState->bdd = s;
 209         printf("Initial state encoded\n");
 210         return fullState;
 211 }
 212
 213 lurd_t *lappend(lurd_t *l, char c){
 214     lurd_t *temp_lrd = NULL;
 215     if (l == NULL){
 216         temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
 217         temp_lrd->c = c;
 218         temp_lrd->next = NULL;
 219         l = temp_lrd;
 220     }
 221     else {
 222         temp_lrd = l;
 223         while (temp_lrd->next != NULL){
 224             temp_lrd = temp_lrd->next;
 225         }
 226         temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
 227         temp_lrd->next->c = c;
 228         temp_lrd->next->next = NULL;
 229     }
 230     return l;
 231 }
 232
 233 int check_goal(BDD s, BDD g, BDDSET vars){
 234     LACE_ME;
 235     if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
 236     else return 0;
 237 }
 238
 239 int check_visited(BDD s, BDD v, BDDSET vars){
 240     LACE_ME;
 241     if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
 242     else return 0;
 243 }
 244
 245 state_t *explstate(state *init, rels *rls, state *g){
 246     LACE_ME;
 247     lurd_t *lrd = NULL;
 248     deque *state_queue = create();
 249     trans_t *t = NULL;
 250     state_t *tmp_state = NULL;
 251     BDD visited = init->bdd;
 252     BDD new;
 253     tmp_state->bdd = init->bdd;
 254     tmp_state->vars = init->vars;
 255     tmp_state->lrd = lrd;
 256     state_queue = enq(tmp_state, state_queue);
 257
 258     while (isEmpty(state_queue) == 1){
 259         tmp_state = get_front(state_queue);
 260         state_queue = deq(state_queue);
 261         t = rls->rell;
 262         new = sylvan_false;
 263         while (t != NULL){
 264             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 265             t = t->next_rel;
 266         }
 267         if (check_visited(new, visited, init->vars.varset) == 0){
 268             if (check_goal(new, g->bdd, init->vars.varset) == 0){
 269                 lurd_t *lrd = tmp_state->lrd;
 270                 state_t *new_state = NULL;
 271                 new_state = (state_t*)malloc(sizeof(state_t));
 272                 new_state->bdd = new;
 273                 new_state->vars = init->vars;
 274                 lrd = lappend(lrd, 'l');
 275                 new_state->lrd = lrd;
 276                 state_queue = enq(new_state, state_queue);
 277                 visited = sylvan_or(new, visited);
 278             }
 279             else {
 280                 lurd_t *lrd = tmp_state->lrd;
 281                 state_t *new_state = NULL;
 282                 new_state = (state_t*)malloc(sizeof(state_t));
 283                 new_state->bdd = new;
 284                 new_state->vars = init->vars;
 285                 lrd = lappend(lrd, 'l');
 286                 new_state->lrd = lrd;
 287                 return new_state;
 288             }
 289         }
 290
 291         t = rls->relu;
 292         new = sylvan_false;
 293         while (t != NULL){
 294             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 295             t = t->next_rel;
 296         }
 297         if (check_visited(new, visited, init->vars.varset) == 0){
 298             if (check_goal(new, g->bdd, init->vars.varset) == 0){
 299                 lurd_t *lrd = tmp_state->lrd;
 300                 state_t *new_state = NULL;
 301                 new_state = (state_t*)malloc(sizeof(state_t));
 302                 new_state->bdd = new;
 303                 new_state->vars = init->vars;
 304                 lrd = lappend(lrd, 'u');
 305                 new_state->lrd = lrd;
 306                 state_queue = enq(new_state, state_queue);
 307                 visited = sylvan_or(new, visited);
 308             }
 309             else {
 310                 lurd_t *lrd = tmp_state->lrd;
 311                 state_t *new_state = NULL;
 312                 new_state = (state_t*)malloc(sizeof(state_t));
 313                 new_state->bdd = new;
 314                 new_state->vars = init->vars;
 315                 lrd = lappend(lrd, 'u');
 316                 new_state->lrd = lrd;
 317                 return new_state;
 318             }
 319         }
 320
 321         t = rls->relr;
 322         new = sylvan_false;
 323         while (t != NULL){
 324             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 325             t = t->next_rel;
 326         }
 327         if (check_visited(new, visited, init->vars.varset) == 0){
 328             if (check_goal(new, g->bdd, init->vars.varset) == 0){
 329                 lurd_t *lrd = tmp_state->lrd;
 330                 state_t *new_state = NULL;
 331                 new_state = (state_t*)malloc(sizeof(state_t));
 332                 new_state->bdd = new;
 333                 new_state->vars = init->vars;
 334                 lrd = lappend(lrd, 'r');
 335                 new_state->lrd = lrd;
 336                 state_queue = enq(new_state, state_queue);
 337                 visited = sylvan_or(new, visited);
 338             }
 339             else {
 340                 lurd_t *lrd = tmp_state->lrd;
 341                 state_t *new_state = NULL;
 342                 new_state = (state_t*)malloc(sizeof(state_t));
 343                 new_state->bdd = new;
 344                 new_state->vars = init->vars;
 345                 lrd = lappend(lrd, 'r');
 346                 new_state->lrd = lrd;
 347                 return new_state;
 348             }
 349         }
 350
 351         t = rls->reld;
 352         new = sylvan_false;
 353         while (t != NULL){
 354             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
 355             t = t->next_rel;
 356         }
 357         if (check_visited(new, visited, init->vars.varset) == 0){
 358             if (check_goal(new, g->bdd, init->vars.varset) == 0){
 359                 lurd_t *lrd = tmp_state->lrd;
 360                 state_t *new_state = NULL;
 361                 new_state = (state_t*)malloc(sizeof(state_t));
 362                 new_state->bdd = new;
 363                 new_state->vars = init->vars;
 364                 lrd = lappend(lrd, 'd');
 365                 new_state->lrd = lrd;
 366                 state_queue = enq(new_state, state_queue);
 367                 visited = sylvan_or(new, visited);
 368             }
 369             else {
 370                 lurd_t *lrd = tmp_state->lrd;
 371                 state_t *new_state = NULL;
 372                 new_state = (state_t*)malloc(sizeof(state_t));
 373                 new_state->bdd = new;
 374                 new_state->vars = init->vars;
 375                 lrd = lappend(lrd, 'd');
 376                 new_state->lrd = lrd;
 377                 return new_state;
 378             }
 379         }
 380
 381     }
 382
 383     return NULL;
 384 }
 385
 386 state *encode_goal(sokoban_screen *screen){
 387     int boxes = 0;
 388     int targets = 0;
 389
 390     LACE_ME;
 391
 392         BDDVAR vars[HASH_COUNT(screen) * 3];
 393         for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
 394                 vars[i] = i * 2;
 395         }
 396
 397         uint8_t st_enc[HASH_COUNT(screen) * 3];
 398
 399         BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
 400         BDD s;
 401         state *fullState = NULL;
 402         fullState = (state *)malloc(sizeof(state));
 403         fullState->vars.varset = varset;
 404         fullState->vars.size = HASH_COUNT(screen) * 3;
 405         int tile_index = 0;
 406         sokoban_screen *r;
 407         for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
 408                 switch(r->tile){
 409                 case FREE: //001 -> any
 410                         st_enc[tile_index] = 2;
 411                         tile_index++;
 412                         st_enc[tile_index] = 2;
 413                         tile_index++;
 414                         st_enc[tile_index] = 2;
 415                         tile_index++;
 416                         break;
 417                 case WALL: //000 -> stays the same
 418                         st_enc[tile_index] = 0;
 419                         tile_index++;
 420                         st_enc[tile_index] = 0;
 421                         tile_index++;
 422                         st_enc[tile_index] = 0;
 423                         tile_index++;
 424                         break;
 425                 case BOX: //010 -> any
 426             boxes++;
 427                         st_enc[tile_index] = 2;
 428                         tile_index++;
 429                         st_enc[tile_index] = 2;
 430                         tile_index++;
 431                         st_enc[tile_index] = 2;
 432                         tile_index++;
 433                         break;
 434                 case TARGET: //011 -> targbox
 435             targets++;
 436                         st_enc[tile_index] = 1;
 437                         tile_index++;
 438                         st_enc[tile_index] = 0;
 439                         tile_index++;
 440                         st_enc[tile_index] = 0;
 441                         tile_index++;
 442                         break;
 443                 case AGENT: //101 -> any
 444                         st_enc[tile_index] = 2;
 445                         tile_index++;
 446                         st_enc[tile_index] = 2;
 447                         tile_index++;
 448                         st_enc[tile_index] = 2;
 449                         tile_index++;
 450                         break;
 451                 case TARGAGENT: //110 -> targbox
 452             targets++;
 453                         st_enc[tile_index] = 1;
 454                         tile_index++;
 455                         st_enc[tile_index] = 0;
 456                         tile_index++;
 457                         st_enc[tile_index] = 0;
 458                         tile_index++;
 459                         break;
 460                 case TARGBOX: //100 -> stays the same
 461             targets++;
 462             boxes++;
 463                         st_enc[tile_index] = 1;
 464                         tile_index++;
 465                         st_enc[tile_index] = 0;
 466                         tile_index++;
 467                         st_enc[tile_index] = 0;
 468                         tile_index++;
 469                         break;
 470                 }
 471         }
 472         s = sylvan_cube(varset, st_enc);
 473         fullState->bdd = s;
 474         printf("Goal state encoded\n");
 475     if (targets == 0 || (boxes != targets)) return NULL;
 476     else return fullState;
 477
 478 }
 479
 480 //test
 481 //int countTrans(trans_t *trs);
 482
 483 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 484 {
 485         LACE_ME;
 486         trans_t *trs, *trs_current;
 487         bimap *bm = create_bimap_helper(screen);
 488         int x = 0;
 489         int y = 0;
 490         bddvar_xy_map *bddxy = NULL;
 491         int xdelta = 0;
 492         int ydelta = 0;
 493         int xgamma = 0;
 494         int ygamma = 0;
 495         trs = NULL;
 496         switch(dir){
 497         case LEFT:
 498                 xdelta = -1;
 499                 ydelta = 0;
 500                 xgamma = -2;
 501                 ygamma = 0;
 502                 break;
 503         case UP:
 504                 xdelta = 0;
 505                 ydelta = -1;
 506                 xgamma = 0;
 507                 ygamma = -2;
 508                 break;
 509         case RIGHT:
 510                 xdelta = 1;
 511                 ydelta = 0;
 512                 xgamma = 2;
 513                 ygamma = 0;
 514                 break;
 515         case DOWN:
 516                 xdelta = 0;
 517                 ydelta = 1;
 518                 xgamma = 0;
 519                 ygamma = 2;
 520                 break;
 521         }
 522
 523         for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
 524                 bddxy = getbdd(i*6, bm->t);
 525                 x = bddxy->value.x;
 526                 y = bddxy->value.y;
 527                 if (check_space(x, y, dir, 1, bm) == 0){
 528             //Agent -> Agent
 529                         //1 1 0 0 1 1 (1 0 1 -> 1 0 1)
 530                         BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
 531                         BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 532                         uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
 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 = 6;
 537                         trs_current->next_rel = trs;
 538                         trs = trs_current;
 539
 540             //Targagent -> Targagent
 541                         //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
 542                         relvarset = sylvan_set_fromarray(relvars, 6);
 543             uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
 544             memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
 545
 546                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 547                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 548                         trs_current->varset.varset = relvarset;
 549                         trs_current->varset.size = 6;
 550                         trs_current->next_rel = trs;
 551                         trs = trs_current;
 552
 553                 }
 554
 555                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
 556                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 557                         unsigned int deltai = bddvar->value.var[0];
 558             //Agent Free -> Free Agent
 559             //(1 0 0 0 1 1 0 1 0 0 1 1)
 560             //or
 561             //(0 1 0 0 1 1 1 0 0 0 1 1)
 562                         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};
 563                         BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 564             uint8_t rel_enc[12];
 565             if (i*6 < deltai){
 566                 uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
 567                 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
 568             }
 569             else {
 570                 uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 571                 memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
 572             }
 573                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 574                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 575                         trs_current->varset.varset = relvarset;
 576                         trs_current->varset.size = 12;
 577                         trs_current->next_rel = trs;
 578                         trs = trs_current;
 579
 580             //Agent Target -> Free Targagent
 581             //(1 0 0 0 1 1 0 1 1 1 1 0)
 582             //or
 583             //(0 1 1 1 1 0 1 0 0 0 1 1)
 584                         relvarset = sylvan_set_fromarray(relvars, 12);
 585             if (i*6 < deltai){
 586                 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
 587                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
 588             }
 589             else {
 590                 uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 591                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
 592             }
 593                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 594                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 595                         trs_current->varset.varset = relvarset;
 596                         trs_current->varset.size = 12;
 597                         trs_current->next_rel = trs;
 598                         trs = trs_current;
 599
 600             //Targagent Free -> Target Agent
 601             //(1 0 1 1 0 1 0 1 0 0 1 1)
 602             //or
 603             //(0 1 0 0 1 1 1 0 1 1 0 1)
 604                         relvarset = sylvan_set_fromarray(relvars, 12);
 605             if (i*6 < deltai){
 606                 uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
 607                 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
 608             }
 609             else {
 610                 uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
 611                 memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
 612             }
 613                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 614                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 615                         trs_current->varset.varset = relvarset;
 616                         trs_current->varset.size = 12;
 617                         trs_current->next_rel = trs;
 618                         trs = trs_current;
 619
 620             //Targagent Target -> Target Targagent
 621             //(1 0 1 1 0 1 0 1 1 1 1 0)
 622             //or
 623             //(0 1 1 1 1 0 1 0 1 1 0 1)
 624                         relvarset = sylvan_set_fromarray(relvars, 12);
 625             if (i*6 < deltai){
 626                 uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
 627                 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
 628             }
 629             else {
 630                 uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 631                 memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
 632             }
 633                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 634                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 635                         trs_current->varset.varset = relvarset;
 636                         trs_current->varset.size = 12;
 637                         trs_current->next_rel = trs;
 638                         trs = trs_current;
 639
 640             //Agent Box -> Agent Box
 641             //(1 1 0 0 1 1 0 0 1 1 0 0)
 642             //or
 643             //(0 0 1 1 0 0 1 1 0 0 1 1)
 644                         relvarset = sylvan_set_fromarray(relvars, 12);
 645             if (i*6 < deltai){
 646                 uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 647                 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
 648             }
 649             else {
 650                 uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 651                 memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
 652             }
 653                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 654                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 655                         trs_current->varset.varset = relvarset;
 656                         trs_current->varset.size = 12;
 657                         trs_current->next_rel = trs;
 658                         trs = trs_current;
 659
 660             //Agent Targbox -> Agent Targbox
 661             //(1 1 0 0 1 1 1 1 0 0 0 0)
 662             //
 663             //(1 1 0 0 0 0 1 1 0 0 1 1)
 664                         relvarset = sylvan_set_fromarray(relvars, 12);
 665             if (i*6 < deltai){
 666                 uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
 667                 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
 668             }
 669             else {
 670                 uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 671                 memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
 672             }
 673                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 674                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 675                         trs_current->varset.varset = relvarset;
 676                         trs_current->varset.size = 12;
 677                         trs_current->next_rel = trs;
 678                         trs = trs_current;
 679
 680             //Targagent Box -> Targagent Box
 681             //(1 1 1 1 0 0 0 0 1 1 0 0)
 682             //or
 683             //(0 0 1 1 0 0 1 1 1 1 0 0)
 684                         relvarset = sylvan_set_fromarray(relvars, 12);
 685             if (i*6 < deltai){
 686                 uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 687                 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
 688             }
 689             else {
 690                 uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 691                 memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
 692             }
 693                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 694                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 695                         trs_current->varset.varset = relvarset;
 696                         trs_current->varset.size = 12;
 697                         trs_current->next_rel = trs;
 698                         trs = trs_current;
 699
 700             //Targagent Targbox -> Targagent Targbox
 701             //(1 1 1 1 0 0 1 1 0 0 0 0)
 702             //or
 703             //(1 1 0 0 0 0 1 1 1 1 0 0)
 704                         relvarset = sylvan_set_fromarray(relvars, 12);
 705             if (i*6 < deltai){
 706                 uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 707                 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
 708             }
 709             else {
 710                 uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 711                 memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
 712             }
 713                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 714                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 715                         trs_current->varset.varset = relvarset;
 716                         trs_current->varset.size = 12;
 717                         trs_current->next_rel = trs;
 718                         trs = trs_current;
 719
 720
 721                 }
 722
 723                 else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
 724                         xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
 725                         unsigned int deltai = bddvar->value.var[0];
 726                         bddvar = getxy(x + xgamma, y + ygamma, bm->f);
 727                         unsigned int gammai = bddvar->value.var[0];
 728             //Agent Free -> Free Agent
 729                         //(1 0 0 0 1 1 0 1 0 0 1 1)
 730             //or
 731             //(0 1 0 0 1 1 1 0 0 0 1 1)
 732                         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};
 733                         BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
 734                         uint8_t rel_enc[12];
 735             if (i*6 < deltai){
 736                 uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
 737                 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
 738             }
 739             else {
 740                 uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
 741                 memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
 742             }
 743                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 744                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 745                         trs_current->varset.varset = relvarset;
 746                         trs_current->varset.size = 12;
 747                         trs_current->next_rel = trs;
 748                         trs = trs_current;
 749
 750             //Agent Target -> Free Targagent
 751             //(1 0 0 0 1 1 0 1 1 1 1 0)
 752             //or
 753             //(0 1 1 1 1 0 1 0 0 0 1 1)
 754                         relvarset = sylvan_set_fromarray(relvars, 12);
 755             if (i*6 < deltai){
 756                 uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
 757                 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
 758             }
 759             else {
 760                 uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
 761                 memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
 762             }
 763                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 764                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 765                         trs_current->varset.varset = relvarset;
 766                         trs_current->varset.size = 12;
 767                         trs_current->next_rel = trs;
 768                         trs = trs_current;
 769
 770             //Targagent Free -> Target Agent (LEFT || UP)
 771             //(1 0 1 1 0 1 0 1 0 0 1 1)
 772             //or
 773             //(0 1 0 0 1 1 1 0 1 1 0 1)
 774                         relvarset = sylvan_set_fromarray(relvars, 12);
 775             if (i*6 < deltai){
 776                 uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
 777                 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
 778             }
 779             else {
 780                 uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
 781                 memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
 782             }
 783                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 784                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 785                         trs_current->varset.varset = relvarset;
 786                         trs_current->varset.size = 12;
 787                         trs_current->next_rel = trs;
 788                         trs = trs_current;
 789
 790             //Targagent Target -> Target Targagent (LEFT || UP)
 791             //(1 0 1 1 0 1 0 1 1 1 1 0)
 792             //or
 793             //(0 1 1 1 1 0 1 0 1 1 0 1)
 794                         relvarset = sylvan_set_fromarray(relvars, 12);
 795             if (i*6 < deltai){
 796                 uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
 797                 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
 798             }
 799             else {
 800                 uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 801                 memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
 802             }
 803                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 804                         trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 805                         trs_current->varset.varset = relvarset;
 806                         trs_current->varset.size = 12;
 807                         trs_current->next_rel = trs;
 808                         trs = trs_current;
 809
 810             //Agent Box Box -> Agent Box Box
 811             //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
 812             //or
 813             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
 814             //or
 815             //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
 816             //or
 817             //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
 818             //or
 819             //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
 820             //or
 821             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
 822                         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};
 823                         BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
 824                         uint8_t rel_enc1[18];
 825             if (i*6 < deltai && deltai < gammai){
 826                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 827                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 828             }
 829             else if (deltai < gammai && gammai < i*6){
 830                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 831                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 832             }
 833             else if (gammai < i*6 && i*6 < deltai){
 834                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 835                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 836             }
 837             else if (i*6 < gammai && gammai < deltai){
 838                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 839                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 840             }
 841             else if (deltai < i*6 && i*6 < gammai){
 842                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 843                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 844             }
 845             else {
 846                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 847                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 848             }
 849
 850                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 851                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 852                         trs_current->varset.varset = relvarset1;
 853                         trs_current->varset.size = 18;
 854                         trs_current->next_rel = trs;
 855                         trs = trs_current;
 856
 857             //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
 858             //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma)
 859             //or
 860             //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
 861             //or
 862             //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
 863             //or
 864             //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
 865             //or
 866             //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
 867             //or
 868             //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
 869                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 870             if (i*6 < deltai && deltai < gammai){
 871                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 872                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 873             }
 874             else if (deltai < gammai && gammai < i*6){
 875                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
 876                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 877             }
 878             else if (gammai < i*6 && i*6 < deltai){
 879                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
 880                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 881             }
 882             else if (i*6 < gammai && gammai < deltai){
 883                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
 884                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 885             }
 886             else if (deltai < i*6 && i*6 < gammai){
 887                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
 888                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 889             }
 890             else {
 891                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
 892                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 893             }
 894                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 895                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 896                         trs_current->varset.varset = relvarset1;
 897                         trs_current->varset.size = 18;
 898                         trs_current->next_rel = trs;
 899                         trs = trs_current;
 900
 901             //Targagent Box Box -> Targagent Box Box
 902                         //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
 903             //or
 904             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 905             //or
 906             //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 907             //or
 908             //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
 909             //or
 910             //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 911             //or
 912             //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 913                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 914             if (i*6 < deltai && deltai < gammai){
 915                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 916                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 917             }
 918             else if (deltai < gammai && gammai < i*6){
 919                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 920                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 921             }
 922             else if (gammai < i*6 && i*6 < deltai){
 923                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 924                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 925             }
 926             else if (i*6 < gammai && gammai < deltai){
 927                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 928                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 929             }
 930             else if (deltai < i*6 && i*6 < gammai){
 931                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 932                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 933             }
 934             else {
 935                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 936                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 937             }
 938                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 939                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 940                         trs_current->varset.varset = relvarset1;
 941                         trs_current->varset.size = 18;
 942                         trs_current->next_rel = trs;
 943                         trs = trs_current;
 944
 945             //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
 946             //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
 947             //or
 948             //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
 949             //or
 950             //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
 951             //or
 952             //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
 953             //or
 954             //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
 955             //or
 956             //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 957                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
 958             if (i*6 < deltai && deltai < gammai){
 959                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 960                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 961             }
 962             else if (deltai < gammai && gammai < i*6){
 963                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
 964                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 965             }
 966             else if (gammai < i*6 && i*6 < deltai){
 967                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
 968                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 969             }
 970             else if (i*6 < gammai && gammai < deltai){
 971                 uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
 972                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 973             }
 974             else if (deltai < i*6 && i*6 < gammai){
 975                 uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
 976                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 977             }
 978             else {
 979                 uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
 980                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
 981             }
 982                         trs_current = (trans_t *)malloc(sizeof(trans_t));
 983                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 984                         trs_current->varset.varset = relvarset1;
 985                         trs_current->varset.size = 18;
 986                         trs_current->next_rel = trs;
 987                         trs = trs_current;
 988
 989                         //Agent Box Free -> Free Agent Box
 990             //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
 991             //or
 992             //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
 993             //or
 994             //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
 995             //or
 996             //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
 997             //or
 998             //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
 999             //or
1000             //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1001                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1002             if (i*6 < deltai && deltai < gammai){
1003                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1004                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1005             }
1006
1007             else if (deltai < gammai && gammai < i*6){
1008                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1009                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1010             }
1011
1012             else if (gammai < i*6 && i*6 < deltai){
1013                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1014                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1015             }
1016
1017             else if (i*6 < gammai && gammai < deltai){
1018                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1019                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1020             }
1021             else if (deltai < i*6 && i*6 < gammai){
1022                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1023                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1024             }
1025             else {
1026                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1027                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1028             }
1029
1030                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1031
1032                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1033                         trs_current->varset.varset = relvarset1;
1034                         trs_current->varset.size = 18;
1035                         trs_current->next_rel = trs;
1036                         trs = trs_current;
1037
1038                         //Agent Targbox Free -> Free Targagent Box
1039             //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
1040             //or
1041             //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
1042             //or
1043             //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1044             //or
1045             //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
1046             //or
1047             //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
1048             //or
1049             //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1050                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1051             if (i*6 < deltai && deltai < gammai){
1052                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1053                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1054             }
1055             else if (deltai < gammai && gammai < i*6){
1056                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
1057                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1058             }
1059             else if (gammai < i*6 && i*6 < deltai){
1060                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1061                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1062             }
1063             else if (i*6 < gammai && gammai < deltai){
1064                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1065                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1066             }
1067             else if (deltai < i*6 && i*6 < gammai){
1068                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
1069                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1070             }
1071             else {
1072                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1073                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1074             }
1075                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1076                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1077                         trs_current->varset.varset = relvarset1;
1078                         trs_current->varset.size = 18;
1079                         trs_current->next_rel = trs;
1080                         trs = trs_current;
1081
1082                         //Agent Box Target -> Free Agent Targbox
1083             //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
1084             //or
1085             //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
1086             //or
1087             //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
1088             //or
1089             //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
1090             //or
1091             //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
1092             //or
1093             //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
1094                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1095             if (i*6 < deltai && deltai < gammai){
1096                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1097                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1098             }
1099             else if (deltai < gammai && gammai < i*6){
1100                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1101                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1102             }
1103             else if (gammai < i*6 && i*6 < deltai){
1104                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
1105                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1106             }
1107             else if (i*6 < gammai && gammai < deltai){
1108                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1109                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1110             }
1111             else if (deltai < i*6 && i*6 < gammai){
1112                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1113                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1114             }
1115             else {
1116                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
1117                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1118             }
1119                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1120                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1121                         trs_current->varset.varset = relvarset1;
1122                         trs_current->varset.size = 18;
1123                         trs_current->next_rel = trs;
1124                         trs = trs_current;
1125
1126                         //Agent Targbox Target -> Free Targagent Targbox
1127             //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
1128             //or
1129             //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
1130             //or
1131             //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
1132             //or
1133             //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
1134             //or
1135             //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
1136             //or
1137             //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
1138                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1139             if (i*6 < deltai && deltai < gammai){
1140                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1141                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1142             }
1143             else if (deltai < gammai && gammai < i*6){
1144                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
1145                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1146             }
1147             else if (gammai < i*6 && i*6 < deltai){
1148                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
1149                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1150             }
1151             else if (i*6 < gammai && gammai < deltai){
1152                 uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1153                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1154             }
1155             else if (deltai < i*6 && i*6 < gammai){
1156                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
1157                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1158             }
1159             else {
1160                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
1161                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1162             }
1163                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1164                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1165                         trs_current->varset.varset = relvarset1;
1166                         trs_current->varset.size = 18;
1167                         trs_current->next_rel = trs;
1168                         trs = trs_current;
1169
1170                         //Targagent Box Free -> Target Agent Box
1171             //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
1172             //or
1173             //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
1174             //or
1175             //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1176             //or
1177             //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
1178             //or
1179             //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
1180             //or
1181             //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1182                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1183             if (i*6 < deltai && deltai < gammai){
1184                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
1185                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1186             }
1187             else if (deltai < gammai && gammai < i*6){
1188                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1189                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1190             }
1191             else if (gammai < i*6 && i*6 < deltai){
1192                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1193                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1194             }
1195             else if (i*6 < gammai && gammai < deltai){
1196                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
1197                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1198             }
1199             else if (deltai < i*6 && i*6 < gammai){
1200                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
1201                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1202             }
1203             else {
1204                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1205                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1206             }
1207                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1208                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1209                         trs_current->varset.varset = relvarset1;
1210                         trs_current->varset.size = 18;
1211                         trs_current->next_rel = trs;
1212                         trs = trs_current;
1213
1214                         //Targagent Targbox Free -> Target Targagent Box
1215             //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
1216             //or
1217             //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
1218             //or
1219             //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1220             //or
1221             //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
1222             //or
1223             //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
1224             //or
1225             //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
1226                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1227             if (i*6 < deltai && deltai < gammai){
1228                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
1229                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1230             }
1231             else if (deltai < gammai && gammai < i*6){
1232                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
1233                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1234             }
1235             else if (gammai < i*6 && i*6 < deltai){
1236                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1237                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1238             }
1239             else if (i*6 < gammai && gammai < deltai){
1240                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
1241                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1242             }
1243             else if (deltai < i*6 && i*6 < gammai){
1244                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1 ,1, 0};
1245                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1246             }
1247             else {
1248                 uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1249                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1250             }
1251                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1252                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1253                         trs_current->varset.varset = relvarset1;
1254                         trs_current->varset.size = 18;
1255                         trs_current->next_rel = trs;
1256                         trs = trs_current;
1257
1258                         //Targagent Box Target -> Target Agent Targbox
1259             //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
1260             //or
1261             //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
1262             //or
1263             //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
1264             //or
1265             //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
1266             //or
1267             //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
1268             //or
1269             //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
1270                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1271             if (i*6 < deltai && deltai < gammai){
1272                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
1273                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1274             }
1275             else if (deltai < gammai && gammai < i*6){
1276                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1277                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1278             }
1279             else if (gammai < i*6 && i*6 < deltai){
1280                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
1281                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1282             }
1283             else if (i*6 < gammai && gammai < deltai){
1284                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
1285                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1286             }
1287             else if (deltai < i*6 && i*6 < gammai){
1288                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1289                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1290             }
1291             else {
1292                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
1293                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1294             }
1295                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1296                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1297                         trs_current->varset.varset = relvarset1;
1298                         trs_current->varset.size = 18;
1299                         trs_current->next_rel = trs;
1300                         trs = trs_current;
1301
1302                         //Targagent Targbox Target -> Target Targagent Targbox
1303             //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
1304             //or
1305             //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
1306             //or
1307             //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
1308             //or
1309             //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
1310             //or
1311             //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1312             //or
1313             //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
1314                         relvarset1 = sylvan_set_fromarray(relvars1, 18);
1315             if (i*6 < deltai && deltai < gammai){
1316                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
1317                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1318             }
1319             else if (deltai < gammai && gammai < i*6){
1320                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
1321                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1322             }
1323             else if (gammai < i*6 && i*6 < deltai){
1324                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
1325                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1326             }
1327             else if (i*6 < gammai && gammai < deltai){
1328                 uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
1329                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1330             }
1331             else if (deltai < i*6 && i*6 < gammai){
1332                 uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
1333                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1334             }
1335             else {
1336                 uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
1337                 memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
1338             }
1339                         trs_current = (trans_t *)malloc(sizeof(trans_t));
1340                         trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
1341                         trs_current->varset.varset = relvarset1;
1342                         trs_current->varset.size = 18;
1343                         trs_current->next_rel = trs;
1344                         trs = trs_current;
1345                 }
1346
1347         }
1348         trs_current = trs;
1349
1350     //test
1351     /*
1352     switch(dir){
1353     case LEFT:
1354         if (trs_current != NULL) printf("LEFT ok!\n");
1355         else printf ("LEFT is empty\n");
1356         printf("Num of trans relations:%d\n", countTrans(trs));
1357         break;
1358     case UP:
1359         if (trs_current != NULL) printf("UP ok!\n");
1360         else printf ("UP is empty\n");
1361         printf("Num of trans relations:%d\n", countTrans(trs));
1362         break;
1363     case RIGHT:
1364         if (trs_current != NULL) printf("RIGHT ok!\n");
1365         else printf ("RIGHT is empty\n");
1366         printf("Num of trans relations:%d\n", countTrans(trs));
1367         break;
1368     case DOWN:
1369         if (trs_current != NULL) printf("DOWN ok!\n");
1370         else printf ("DOWN is empty\n");
1371         printf("Num of trans relations:%d\n", countTrans(trs));
1372         break;
1373     }
1374     */
1375         return trs;
1376 }
1377
1378 //test
1379 /*
1380 int countTrans(trans_t *trs)
1381 {
1382     int counter = 0;
1383     while (trs != NULL){
1384         counter++;
1385         trs = trs->next_rel;
1386     }
1387     return counter;
1388 }
1389 */
1390 rels *encode_rel(sokoban_screen *screen)
1391 {
1392         LACE_ME;
1393
1394         trans_t *tl = sylvan_false;
1395
1396         //left relation
1397         tl = create_single_rel(screen, LEFT);
1398
1399         //up relation
1400         trans_t *tu = create_single_rel(screen, UP);
1401
1402         //right relation
1403         trans_t *tr = create_single_rel(screen, RIGHT);
1404
1405         //down relation
1406         trans_t *td = create_single_rel(screen, DOWN);
1407
1408         rels *rls = NULL;
1409         rls = (rels *)malloc(sizeof(rels));
1410         rls->rell = tl;
1411         rls->relu = tu;
1412         rls->relr = tr;
1413         rls->reld = td;
1414
1415         return rls;
1416 }
1417
1418 int test_trans(state *s, trans_t *t)
1419 {
1420     LACE_ME;
1421     BDD next = sylvan_false;
1422     while (t != NULL){
1423         next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
1424         if (next == s->bdd) printf("Same\n");
1425         if (next != s->bdd && next != sylvan_false) printf("Different\n");
1426         if (next == sylvan_false) printf("False\n");
1427         t = t->next_rel;
1428     }
1429     return 1;
1430 }