X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=63250915d82f2f3f651f497666b84bae949be66f;hb=6dc70f7da8631fd09dea07b36d582c3812beca86;hp=d9a924a5bffe263c9feae12ced853e09df901401;hpb=961d38840cf50e864cb83711bd9419033c3acd7d;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index d9a924a..6325091 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -6,6 +6,7 @@
 
 #include "coord.h"
 #include "sokoban.h"
+#include "deque.h"
 
 
 typedef struct {
@@ -66,16 +67,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);
@@ -209,8 +210,296 @@ state *encode_screen(sokoban_screen *screen)
 	return fullState;
 }
 
+lurd_t *lappend(lurd_t *l, char c){
+    lurd_t *temp_lrd = NULL;
+    if (l == NULL){
+        temp_lrd = (lurd_t *)malloc(sizeof(lurd_t));
+        temp_lrd->c = c;
+        temp_lrd->next = NULL;
+        l = temp_lrd;
+    }
+    else {
+        temp_lrd = l;
+        while (temp_lrd->next != NULL){
+            temp_lrd = temp_lrd->next;
+        }
+        temp_lrd->next = (lurd_t *)malloc(sizeof(lurd_t));
+        temp_lrd->next->c = c;
+        temp_lrd->next->next = NULL;
+    }
+    return l;
+}
+
+int check_goal(BDD s, BDD g, BDDSET vars){
+    LACE_ME;
+    if(sylvan_satcount(sylvan_and(s, g), vars) > 0) return 1;
+    else return 0;
+}
+
+int check_visited(BDD s, BDD v, BDDSET vars){
+    LACE_ME;
+    if(sylvan_satcount(sylvan_and(s, v), vars) > 0) return 1;
+    else return 0;
+}
+
+state_t *explstate(state *init, rels *rls, state *g){
+    LACE_ME;
+    deque *state_queue = create();
+    trans_t *t = NULL;
+    state_t *tmp_state = (state_t *)malloc(sizeof(state_t));
+    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+    //state_t *new_state = (state_t *)malloc(sizeof(state_t));
+    BDD visited = init->bdd;
+    BDD new;
+    tmp_state->bdd = init->bdd;
+    tmp_state->vars = init->vars;
+    tmp_state->lrd = lrd;
+    state_queue = enq(tmp_state, state_queue);
+
+    while (isEmpty(state_queue) == 0){
+        tmp_state = get_front(state_queue);
+        state_queue = deq(state_queue);
+        new = tmp_state->bdd;
+        t = rls->rell;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'l');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'l');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+        t = rls->relu;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'u');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'u');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+        t = rls->relr;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'r');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'r');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+
+        t = rls->reld;
+        while (t != NULL){
+            new = sylvan_relnext(tmp_state->bdd, t->bdd, t->varset.varset);
+            if (new != sylvan_false && new != tmp_state->bdd) break;
+            t = t->next_rel;
+        }
+        if (new != sylvan_false && new != tmp_state->bdd){
+            if (check_visited(new, visited, init->vars.varset) == 0){
+                if (check_goal(new, g->bdd, init->vars.varset) == 0){
+
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'd');
+                    new_state->lrd = lrd;
+                    state_queue = enq(new_state, state_queue);
+                    visited = sylvan_or(new, visited);
+                }
+                else {
+                    printf("GOAL\n");
+                    lurd_t *lrd = (lurd_t *)malloc(sizeof(lurd_t));
+                    state_t *new_state = (state_t *)malloc(sizeof(state_t));
+                    memcpy(lrd, tmp_state->lrd, sizeof(lurd_t));
+
+                    new_state->bdd = new;
+                    new_state->vars = init->vars;
+                    lrd = lappend(lrd, 'd');
+                    new_state->lrd = lrd;
+                    return new_state;
+                }
+            }
+        }
+
+
+    }
+
+    return NULL;
+}
+
+state *encode_goal(sokoban_screen *screen){
+    int boxes = 0;
+    int targets = 0;
+
+    LACE_ME;
+
+	BDDVAR vars[HASH_COUNT(screen) * 3];
+	for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
+		vars[i] = i * 2;
+	}
+
+	uint8_t st_enc[HASH_COUNT(screen) * 3];
+
+	BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
+	BDD s;
+	state *fullState = NULL;
+	fullState = (state *)malloc(sizeof(state));
+	fullState->vars.varset = varset;
+	fullState->vars.size = HASH_COUNT(screen) * 3;
+	int tile_index = 0;
+	sokoban_screen *r;
+	for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+		switch(r->tile){
+		case FREE: //001 -> any
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			break;
+		case WALL: //000 -> stays the same
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			break;
+		case BOX: //010 -> any
+            boxes++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			break;
+		case TARGET: //011 -> targbox
+            targets++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			break;
+		case AGENT: //101 -> any
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			st_enc[tile_index] = 2;
+			tile_index++;
+			break;
+		case TARGAGENT: //110 -> targbox
+            targets++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			break;
+		case TARGBOX: //100 -> stays the same
+            targets++;
+            boxes++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			break;
+		}
+	}
+	s = sylvan_cube(varset, st_enc);
+	fullState->bdd = s;
+	printf("Goal state encoded\n");
+    if (targets == 0 || (boxes != targets)) return NULL;
+    else return fullState;
+
+}
+
 //test
-int countTrans(trans_t *trs);
+//int countTrans(trans_t *trs);
 
 trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 {
@@ -253,7 +542,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){
@@ -262,7 +551,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5};
 			BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
 			uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
-
 			trs_current = (trans_t *)malloc(sizeof(trans_t));
 			trs_current->bdd = sylvan_cube(relvarset, rel_enc);
 			trs_current->varset.varset = relvarset;
@@ -273,12 +561,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);
@@ -288,16 +572,25 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			trs = trs_current;
 
 		}
-		else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 0){
 
+		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*6 < 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 +600,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*6 < 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, 1, 0, 0, 0, 1, 1};
+                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 +620,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*6 < 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 +640,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*6 < 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 +660,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*6 < 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 +680,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*6 < 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 +700,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*6 < 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 +720,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*6 < 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;
@@ -459,19 +738,29 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			trs_current->next_rel = trs;
 			trs = trs_current;
 
+
 		}
-		else if (check_space(x, y, dir, 1, bm) == 1 && check_space(x, y, dir, 2, bm) == 1){
 
+		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*6 < 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 +770,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*6 < 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 +788,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*6 < 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 +808,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*6 < 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;
@@ -546,28 +829,45 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			trs = trs_current;
 
             //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};
+            //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma)
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
+            //or
+            //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma)
+            //or
+            //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
+			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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < gammai){
+                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 {
+                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));
+            }
+
 			trs_current = (trans_t *)malloc(sizeof(trans_t));
 			trs_current->bdd = sylvan_cube(relvarset1, rel_enc1);
 			trs_current->varset.varset = relvarset1;
@@ -575,27 +875,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
-            //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0)
+            //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) (i delta gamma)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i)
+            //or
+            //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta)
+            //or
+            //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta)
+            //or
+            //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma)
+            //or
+            //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i)
 			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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +921,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +963,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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,26 +1009,47 @@ 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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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;
 			trs_current->varset.size = 18;
@@ -689,25 +1058,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1102,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1146,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1190,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1234,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1278,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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 +1322,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*6 < deltai && 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 && gammai < i*6){
+                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*6 && i*6 < 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*6 < gammai && 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*6 && i*6 < 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] = {0, 1, 1, 0, 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;
@@ -883,10 +1364,12 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 			trs_current->next_rel = trs;
 			trs = trs_current;
 		}
+
 	}
 	trs_current = trs;
 
     //test
+    /*
     switch(dir){
     case LEFT:
         if (trs_current != NULL) printf("LEFT ok!\n");
@@ -909,11 +1392,12 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
         printf("Num of trans relations:%d\n", countTrans(trs));
         break;
     }
-
+    */
 	return trs;
 }
 
 //test
+/*
 int countTrans(trans_t *trs)
 {
     int counter = 0;
@@ -923,7 +1407,7 @@ int countTrans(trans_t *trs)
     }
     return counter;
 }
-
+*/
 rels *encode_rel(sokoban_screen *screen)
 {
 	LACE_ME;
@@ -955,7 +1439,6 @@ rels *encode_rel(sokoban_screen *screen)
 int test_trans(state *s, trans_t *t)
 {
     LACE_ME;
-    int counter = 0;
     BDD next = sylvan_false;
     while (t != NULL){
         next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset);
@@ -964,6 +1447,5 @@ int test_trans(state *s, trans_t *t)
         if (next == sylvan_false) printf("False\n");
         t = t->next_rel;
     }
-    printf("Trans:%d\n", counter);
     return 1;
 }