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