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