state encoding as it has to be

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 8905a17..8641bad 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -57,6 +57,23 @@ typedef struct {
        BDD *reld;
 } rels;
 
+typedef struct {
+       int *vars;
+       int size;
+} variables;
+
+typedef struct
+{
+    BDD bdd;
+    BDD variables;
+} *state;
+
+typedef struct
+{
+    BDD bdd;
+    BDD variables;
+} *trans;
+
 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
 {
        xy_bddvar_map k, *r = NULL;
@@ -175,141 +192,80 @@ bimap *create_bimap_helper(sokoban_screen *screen)
 
 BDD encode_screen(sokoban_screen *screen)
 {
-       BDD state = sylvan_false;
+       LACE_ME;
+
+       BDDVAR vars[HASH_COUNT(screen) * 3];
+       for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
+               vars[i] = i;
+       }
+
+       uint8_t st_enc[HASH_COUNT(screen) * 3];
+
+       BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
+       BDD state;
        int tile_index = 0;
        sokoban_screen *r;
-       LACE_ME;
        for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
                switch(r->tile){
-               case FREE:
-                       if (state == sylvan_false){
-                               state = sylvan_not(sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
+               case FREE: //001
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
                        break;
-               case WALL:
-                       if (state == sylvan_false){
-                               state = sylvan_not(sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
+               case WALL: //000
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
                        break;
-               case BOX:
-                       if (state == sylvan_false){
-                               state = sylvan_not(sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
+               case BOX: //010
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
                        break;
-               case TARGET:
-                       if (state == sylvan_false){
-                               state = sylvan_not(sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
+               case TARGET: //011
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
                        break;
-               case AGENT:
-                       if (state == sylvan_false){
-                               state = sylvan_ithvar(tile_index);
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                       }
+               case AGENT: //101
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
                        break;
-               case TARGAGENT:
-                       if (state == sylvan_false){
-                               state = sylvan_ithvar(tile_index);
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
+               case TARGAGENT: //110
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
                        break;
-               case TARGBOX:
-                       if (state == sylvan_false){
-                               state = sylvan_ithvar(tile_index);
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
-                       else {
-                               state = sylvan_and(state, sylvan_ithvar(tile_index));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                               state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
-                               tile_index++;
-                       }
+               case TARGBOX: //100
+                       st_enc[tile_index] = 1;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
+                       st_enc[tile_index] = 0;
+                       tile_index++;
                        break;
                }
        }
-       /*
+       /* some testing...
        xy_bddvar_map *map = NULL;
        map = create_xy_bddvar_map(screen);
        xy_bddvar_map *m = getxy(1, 1, map);
@@ -319,7 +275,7 @@ BDD encode_screen(sokoban_screen *screen)
        printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
        printf("Test2: %d %d\n", m2->value.x, m2->value.y);
        */
-       /*
+       /* some more testing...
        bimap *bm = NULL;
        bm = create_bimap_helper(screen);
        xy_bddvar_map *m = getxy(1, 1, bm->f);
@@ -329,6 +285,8 @@ BDD encode_screen(sokoban_screen *screen)
        printf("%d tiles were encoded\n", tile_index);
        if (bm != NULL) printf ("WORKS!\n");
        */
+       state = sylvan_cube(varset, st_enc);
+       printf("Initial state encoded\n");
        return state;
 }
 
@@ -337,22 +295,14 @@ BDD encode_rel(sokoban_screen *screen)
        int num_tiles;
        num_tiles = HASH_COUNT(screen);
        printf("Number of tiles: %d\n", num_tiles);
-       return sylvan_true;
-}
 
-void test()
-{
+       //left relation
 
-       printf("Test!\n");
-       BDD a = sylvan_true;
-       BDD b = sylvan_not(a);
-       if (b == sylvan_false){
-               printf("BDD works!\n");
-       } else {
-               printf("BDD does not work!\n");
-       }
-       LACE_ME;
-       BDD c = sylvan_ithvar(1);
-       if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
-       if (sylvan_var(c) == 1) printf("Var works 2\n");
+       //up relation
+
+       //right relation
+
+       //down relation
+
+       return sylvan_true;
 }

diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index 2580d60..2ec2918 100644 (file)
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -7,4 +7,6 @@ BDD encode_screen(sokoban_screen *screen);
 
 BDD encode_rel(sokoban_screen *screen);
 
+//int test_relprod();
+
 #endif

diff --git a/modelchecker/main.c b/modelchecker/main.c
index e954c07..7940dc9 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -62,6 +62,7 @@ void solve(FILE *inputstream)
                case COORD:
                        DPRINT("Encoding coordinate based\n");
                        encode_screen(screen);
+                       //test_relprod();
                        break;
                case OBJECT:
                        DPRINT("Encoding object based\n");