goal state encoder added

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 0f5a507..fa815f0 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -209,8 +209,102 @@ state *encode_screen(sokoban_screen *screen)
        return fullState;
 }
 
+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)
 {
@@ -283,6 +377,7 @@ 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){
                        xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f);
                        unsigned int deltai = bddvar->value.var[0];
@@ -293,7 +388,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        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];
-            if (i < deltai){
+            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));
             }
@@ -313,7 +408,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 1 1 1 0 1 0 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -333,7 +428,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 0 0 1 1 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -353,7 +448,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 1 1 1 0 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -373,7 +468,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 0 1 1 0 0 1 1 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -393,7 +488,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //
             //(1 1 0 0 0 0 1 1 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -413,7 +508,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 0 1 1 0 0 1 1 1 1 0 0)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -433,7 +528,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(1 1 0 0 0 0 1 1 1 1 0 0)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -450,6 +545,7 @@ 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);
                        unsigned int deltai = bddvar->value.var[0];
@@ -462,7 +558,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        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];
-            if (i < deltai){
+            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));
             }
@@ -482,7 +578,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 1 1 1 0 1 0 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -502,7 +598,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 0 0 1 1 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -522,7 +618,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //or
             //(0 1 1 1 1 0 1 0 1 1 0 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
-            if (i < deltai){
+            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));
             }
@@ -552,23 +648,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -597,23 +693,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -641,23 +737,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -685,23 +781,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -729,23 +825,26 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if (i < deltai && deltai < gammai){
+            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){
+
+            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 && i < deltai){
+
+            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 < gammai && gammai < deltai){
+
+            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 && i < gammai){
+            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));
             }
@@ -753,7 +852,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                 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;
@@ -773,23 +874,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if (i < deltai && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -817,23 +918,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 0 0 1 1)
                        relvarset1 = sylvan_set_fromarray(relvars1, 18);
-            if (i < deltai && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -861,23 +962,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -905,23 +1006,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if (i < deltai && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -949,23 +1050,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if (i < deltai && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -993,23 +1094,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 && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -1037,23 +1138,23 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
             //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);
-            if (i < deltai && deltai < gammai){
+            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){
+            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 && i < deltai){
+            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 < gammai && gammai < deltai){
+            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 && i < gammai){
+            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));
             }
@@ -1068,6 +1169,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs_current->next_rel = trs;
                        trs = trs_current;
                }
+
        }
        trs_current = trs;
 
@@ -1100,6 +1202,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 }
 
 //test
+/*
 int countTrans(trans_t *trs)
 {
     int counter = 0;
@@ -1109,7 +1212,7 @@ int countTrans(trans_t *trs)
     }
     return counter;
 }
-
+*/
 rels *encode_rel(sokoban_screen *screen)
 {
        LACE_ME;
@@ -1141,7 +1244,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);
@@ -1150,6 +1252,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;
 }

diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index 56f770f..e289045 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -34,6 +34,8 @@ rels *encode_rel(sokoban_screen *screen);
 
 int test_trans(state *s, trans_t *t);
 
+state *encode_goal(sokoban_screen *screen);
+
 int test_relprod();
 
 #endif

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 5ca9c87..38597f6 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -61,7 +61,16 @@ void solve(FILE *inputstream)
 
        state *init = encode_screen(screen);
        rels *rls = encode_rel(screen);
-    //test_trans(init, rls->reld);
+    /*
+    printf("Doing left\n");
+    test_trans(init, rls->rell);
+    printf("Doing up\n");
+    test_trans(init, rls->relu);
+    printf("Doing right\n");
+    test_trans(init, rls->relr);
+    printf("Doing down\n");
+    test_trans(init, rls->reld);
+    */
 
        BDD old = sylvan_false;
        BDD new = init->bdd;
@@ -71,25 +80,43 @@ void solve(FILE *inputstream)
                ERRPRINT("Iteration %d\n", iteration++);
         trans_t *t = rls->rell;
 
+        //for testing
+        /*
+        BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
+        BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
+        BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
+        BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
+        if (new == teststate2) printf("Wrong!\n");
+        */
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;
+            //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
         }
+
         t = rls->relu;
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;
+            //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
         }
+
+
         t = rls->relr;
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;
+            //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
         }
+
+
         t = rls->reld;
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;
+            //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
         }
+
        }
        ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
 //     sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);