modelchecker/coord.c

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