that was tough...
authorAlexander Fedotov <soyaxhoya@gmail.com>
Sat, 16 Apr 2016 22:54:40 +0000 (00:54 +0200)
committerAlexander Fedotov <soyaxhoya@gmail.com>
Sat, 16 Apr 2016 22:54:40 +0000 (00:54 +0200)
modelchecker/coord.c

index d9a924a..200db36 100644 (file)
@@ -66,16 +66,16 @@ bimap *create_bimap_helper(sokoban_screen *screen)
                memset(f, 0, sizeof(xy_bddvar_map));
                f->key.x = r->coord.x;
                f->key.y = r->coord.y;
-               f->value.var[0] = varcount;
-               f->value.var[1] = varcount + 1;
-               f->value.var[2] = varcount + 2;
+               f->value.var[0] = varcount * 2;
+               f->value.var[1] = (varcount + 1) * 2;
+               f->value.var[2] = (varcount + 2) * 2;
                HASH_ADD(hh, xybdd, key, sizeof(xy), f);
 
                for (int i = 0; i <3; i++){
                        bddvar_xy_map *t = NULL;
                        t = (bddvar_xy_map *)malloc(sizeof(bddvar_xy_map));
                        memset(t, 0, sizeof(bddvar_xy_map));
-                       t->key = varcount + i;
+                       t->key = (varcount + i) * 2;
                        t->value.x = r->coord.x;
                        t->value.y = r->coord.y;
                        HASH_ADD(hh, bddxy, key, sizeof(int), t);
@@ -253,7 +253,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
        }
 
        for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
-               bddxy = getbdd(i*3, bm->t);
+               bddxy = getbdd(i*6, bm->t);
                x = bddxy->value.x;
                y = bddxy->value.y;
                if (check_space(x, y, dir, 1, bm) == 0){
@@ -273,12 +273,8 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //Targagent -> Targagent
                        //1 1 1 1 0 0 (1 1 0 -> 1 1 0)
                        relvarset = sylvan_set_fromarray(relvars, 6);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 1;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 0;
+            uint8_t rel_enc1[6] = {1, 1, 1, 1, 0, 0};
+            memcpy(rel_enc, rel_enc1, 6*sizeof(uint8_t));
 
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
@@ -289,15 +285,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                }
                else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
-
                        xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
-                       int deltai = bddvar->value.var[0];
-
+                       unsigned int deltai = bddvar->value.var[0];
             //Agent Free -> Free Agent
             //(1 0 0 0 1 1 0 1 0 0 1 1)
-                       BDDVAR relvars[12]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5};
+            //or
+            //(0 1 0 0 1 1 1 0 0 0 1 1)
+                       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};
                        BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
-                       uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+            uint8_t rel_enc[12];
+            if (i < deltai){
+                uint8_t rel_enc0[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc0[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc0, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -307,19 +311,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Target -> Free Targagent
             //(1 0 0 0 1 1 0 1 1 1 1 0)
+            //or
+            //(0 1 1 1 1 0 0 1 1 1 1 0)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 0;
-                       rel_enc[3] = 0;
-                       rel_enc[4] = 1;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
+                memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0};
+                memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -329,19 +331,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Targagent Free -> Target Agent
             //(1 0 1 1 0 1 0 1 0 0 1 1)
+            //or
+            //(0 1 0 0 1 1 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 0;
-                       rel_enc[9] = 0;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 1;
+            if (i < deltai){
+                uint8_t rel_enc3[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc3[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc, rel_enc3, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -351,19 +351,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Targagent Target -> Target Targagent
             //(1 0 1 1 0 1 0 1 1 1 1 0)
+            //or
+            //(0 1 1 1 1 0 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc4[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
+                memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc4[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc, rel_enc4, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -373,19 +371,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Box -> Agent Box
             //(1 1 0 0 1 1 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 1;
-                       rel_enc[2] = 0;
-                       rel_enc[3] = 0;
-                       rel_enc[4] = 1;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 0;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 0;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc5[12] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc5[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc5, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -395,19 +391,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Targbox -> Agent Targbox
             //(1 1 0 0 1 1 1 1 0 0 0 0)
+            //
+            //(1 1 0 0 0 0 1 1 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 1;
-                       rel_enc[2] = 0;
-                       rel_enc[3] = 0;
-                       rel_enc[4] = 1;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 1;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 0;
-                       rel_enc[9] = 0;
-                       rel_enc[10] = 0;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc6[12] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc6[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc6, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -417,19 +411,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Targagent Box -> Targagent Box
             //(1 1 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 1;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 0;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 0;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 0;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc7[12] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc7[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc, rel_enc7, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -439,19 +431,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Targagent Targbox -> Targagent Targbox
             //(1 1 1 1 0 0 1 1 0 0 0 0)
+            //or
+            //(1 1 0 0 0 0 1 1 1 1 0 0)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 1;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 0;
-                       rel_enc[6] = 1;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 0;
-                       rel_enc[9] = 0;
-                       rel_enc[10] = 0;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc8[12] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc8[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc, rel_enc8, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -461,17 +451,25 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                }
                else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
-
                        xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
-                       int deltai = bddvar->value.var[0];
+                       unsigned int deltai = bddvar->value.var[0];
                        bddvar = getxy(x + xgamma, y + ygamma, bm->f);
-                       int gammai = bddvar->value.var[0];
-
+                       unsigned int gammai = bddvar->value.var[0];
             //Agent Free -> Free Agent
                        //(1 0 0 0 1 1 0 1 0 0 1 1)
-                       BDDVAR relvars[12]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, i*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5};
+            //or
+            //(0 1 0 0 1 1 1 0 0 0 1 1)
+                       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};
                        BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
-                       uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+                       uint8_t rel_enc[12];
+            if (i < deltai){
+                uint8_t rel_enc_[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc_[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc_, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -481,19 +479,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Target -> Free Targagent
             //(1 0 0 0 1 1 0 1 1 1 1 0)
+            //or
+            //(0 1 1 1 1 0 1 0 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 0;
-                       rel_enc[3] = 0;
-                       rel_enc[4] = 1;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc9[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
+                memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc9[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc9, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -501,21 +497,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs_current->next_rel = trs;
                        trs = trs_current;
 
-            //Targagent Free -> Target Agent
+            //Targagent Free -> Target Agent (LEFT || UP)
             //(1 0 1 1 0 1 0 1 0 0 1 1)
+            //or
+            //(0 1 0 0 1 1 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 0;
-                       rel_enc[9] = 0;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 1;
+            if (i < deltai){
+                uint8_t rel_enc10[12] = {1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1, 1};
+                memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc10[12] = {0, 1, 0, 0, 1, 1, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc, rel_enc10, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -523,21 +517,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs_current->next_rel = trs;
                        trs = trs_current;
 
-            //Targagent Target -> Target Targagent
+            //Targagent Target -> Target Targagent (LEFT || UP)
             //(1 0 1 1 0 1 0 1 1 1 1 0)
+            //or
+            //(0 1 1 1 1 0 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-                       rel_enc[0] = 1;
-                       rel_enc[1] = 0;
-                       rel_enc[2] = 1;
-                       rel_enc[3] = 1;
-                       rel_enc[4] = 0;
-                       rel_enc[5] = 1;
-                       rel_enc[6] = 0;
-                       rel_enc[7] = 1;
-                       rel_enc[8] = 1;
-                       rel_enc[9] = 1;
-                       rel_enc[10] = 1;
-                       rel_enc[11] = 0;
+            if (i < deltai){
+                uint8_t rel_enc11[12] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 1, 1, 0};
+                memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc11[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc, rel_enc11, 12*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset, rel_enc);
                        trs_current->varset.varset = relvarset;
@@ -547,27 +539,44 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Agent Box Box -> Agent Box Box
                        //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
-                       BDDVAR relvars1[18]  = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5, 2*gammai, 2*gammai+1, 2*gammai+2, 2*gammai+3, 2*gammai+4, 2*gammai+5};
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //or
+            //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+                       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};
                        BDD relvarset1 = sylvan_set_fromarray(relvars1, 18);
                        uint8_t rel_enc1[18];
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 1;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 0;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -575,27 +584,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs_current->next_rel = trs;
                        trs = trs_current;
 
-            //Agent Box Targbox -> Agent Box Targbox
+            //Agent Box Targbox -> Agent Box Targbox (LEFT || UP)
             //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1)
+            //or
+            //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0)
+            //or
+            //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0)
+            //or
+            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 1;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 0;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 1;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 0;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -605,25 +630,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
             //Targagent Box Box -> Targagent Box Box
                        //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 1;
-                       rel_enc1[2] = 1;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 0;
-                       rel_enc1[5] = 0;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 0;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -631,27 +672,43 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs_current->next_rel = trs;
                        trs = trs_current;
 
-            //Targagent Box Targbox -> Targagent Box Targbox
+            //Targagent Box Targbox -> Targagent Box Targbox (LEFT || UP)
             //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 1 1 0 0)
+            //or
+            //(1 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 0 0)
+            //or
+            //(1 1 1 1 0 0 1 1 0 0 0 0 0 0 1 1 0 0)
+            //or
+            //(0 0 1 1 0 0 1 1 1 1 0 0 1 1 0 0 0 0)
+            //or
+            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 1;
-                       rel_enc1[2] = 1;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 0;
-                       rel_enc1[5] = 0;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 0;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 1;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 0;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -661,25 +718,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Box Free -> Free Agent Box
             //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0)
+            //or
+            //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1)
+            //or
+            //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
+            //or
+            //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1)
+            //or
+            //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0)
+            //or
+            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 0;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 1;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 0;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -689,25 +762,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Targbox Free -> Free Targagent Box
             //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0)
+            //or
+            //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1)
+            //or
+            //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
+            //or
+            //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0)
+            //or
+            //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0)
+            //or
+            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 1;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 0;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 0;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -717,25 +806,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Box Target -> Free Agent Targbox
             //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0)
+            //or
+            //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1)
+            //or
+            //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1)
+            //or
+            //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1)
+            //or
+            //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0)
+            //or
+            //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 0;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 1;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -745,25 +850,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Agent Targbox Target -> Free Targagent Targbox
             //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0)
+            //or
+            //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1)
+            //or
+            //(0 1 1 0 1 0 1 0 0 0 1 1 1 1 0 1 0 0)
+            //or
+            //(1 0 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0 0)
+            //or
+            //(1 1 0 1 0 0 1 0 0 0 1 1 0 1 1 0 1 0)
+            //or
+            //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 0;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 1;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 0;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -773,25 +894,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Box Free -> Target Agent Box
             //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0)
+            //or
+            //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1)
+            //or
+            //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
+            //or
+            //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1)
+            //or
+            //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0)
+            //or
+            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 0;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 0;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 0;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 1;
-                       rel_enc1[12] = 1;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 1;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -801,25 +938,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Targbox Free -> Target Targagent Box
             //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0)
+            //or
+            //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1)
+            //or
+            //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
+            //or
+            //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0)
+            //or
+            //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0)
+            //or
+            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 0;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 0;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 1;
-                       rel_enc1[5] = 0;
-                       rel_enc1[6] = 1;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 0;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 1;
-                       rel_enc1[13] = 0;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 1;
-                       rel_enc1[16] = 0;
-                       rel_enc1[17] = 1;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -829,25 +982,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Box Target -> Target Agent Targbox
             //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0)
+            //or
+            //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 1 1 0 1)
+            //or
+            //(0 1 1 0 1 0 1 0 1 1 0 1 0 1 1 0 0 1)
+            //or
+            //(1 0 1 1 0 1 0 1 1 0 1 0 0 1 1 0 0 1)
+            //or
+            //(0 1 1 0 0 1 1 0 1 1 0 1 0 1 1 0 1 0)
+            //or
+            //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 1;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 0;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 0;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 1;
-                       rel_enc1[9] = 0;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 1;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;
@@ -857,25 +1026,41 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 
                        //Targagent Targbox Target -> Target Targagent Targbox
             //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0)
+            //or
+            //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 1 1 0 1)
+            //or
+            //(0 1 1 0 1 0 1 0 1 1 0 1 1 1 0 1 0 0)
+            //or
+            //(1 0 1 1 0 1 0 1 1 0 1 0 1 1 0 1 0 0)
+            //or
+            //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
+            //or
+            //(1 1 0 1 0 0 1 0 1 1 0 1 0 1 1 0 1 0)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-                       rel_enc1[0] = 1;
-                       rel_enc1[1] = 0;
-                       rel_enc1[2] = 1;
-                       rel_enc1[3] = 1;
-                       rel_enc1[4] = 0;
-                       rel_enc1[5] = 1;
-                       rel_enc1[6] = 1;
-                       rel_enc1[7] = 1;
-                       rel_enc1[8] = 0;
-                       rel_enc1[9] = 1;
-                       rel_enc1[10] = 0;
-                       rel_enc1[11] = 0;
-                       rel_enc1[12] = 0;
-                       rel_enc1[13] = 1;
-                       rel_enc1[14] = 1;
-                       rel_enc1[15] = 0;
-                       rel_enc1[16] = 1;
-                       rel_enc1[17] = 0;
+            if ((i < deltai) < gammai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < gammai) < i){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((gammai < i) < deltai){
+                uint8_t rel_enc__[18] = {0, 1, 1, 0, 1, 0, 1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((i < gammai) < deltai){
+                uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else if ((deltai < i) < gammai){
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
+            else {
+                uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0};
+                memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t));
+            }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));
                        trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
                        trs_current->varset.varset = relvarset1;