transition fix

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 48f3b07..0f5a507 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -262,7 +262,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;
@@ -449,6 +448,7 @@ 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){
                        xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
@@ -538,7 +538,6 @@ 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)
             //(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)
@@ -553,23 +552,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        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];
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && i < 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));
             }
@@ -598,23 +597,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -642,23 +641,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -686,23 +685,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -719,40 +718,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -769,40 +762,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -819,40 +806,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -869,7 +850,6 @@ 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)
-            //(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
@@ -881,23 +861,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -914,40 +894,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -964,40 +938,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -1025,23 +993,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }
@@ -1058,41 +1026,34 @@ 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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(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)
-            //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1
-            //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if ((i < deltai) < gammai){
+            if (i < 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) < i){
+            else if (deltai < gammai && 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){
+            else if (gammai < i && 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){
+            else if (i < 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) < gammai){
+            else if (deltai < i && 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));
             }

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 20ad57b..5ca9c87 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -61,6 +61,7 @@ void solve(FILE *inputstream)
 
        state *init = encode_screen(screen);
        rels *rls = encode_rel(screen);
+    //test_trans(init, rls->reld);
 
        BDD old = sylvan_false;
        BDD new = init->bdd;