state encoding done (needs checking)

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index dec0a28..bf165a7 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -37,70 +37,141 @@
 BDD encode_screen(sokoban_screen *screen)
 {
        BDD state = sylvan_false;
-       //int tile_index = 0;
+       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++;
                        }
                        printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
                        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++;
                        }
                        printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
                        break;