state encoding done (needs checking)

[mc1516pa.git] / modelchecker / coord.c

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 4c19a60..bf165a7 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -18,12 +18,166 @@
 #include "sokoban.h"
 
 
+/*
+ * Each coordinate has three related boolean variables. The combination of those boolean variables
+ * defines tiles:
+ * 000: Wall
+ * 001: Free
+ * 010: Box
+ * 100: Box on target
+ * 011: Target
+ * 101: Agent
+ * 110: Agent on target
+ * In the BDD representation, the state is represented by n * 3 variables, where n is the number of
+ * tiles in the shrinked screen.
+ * It seems that the move variable is not necessary since non-deterministic moves can be emvedded
+ * directly in transition relations.
+ */
+
 BDD encode_screen(sokoban_screen *screen)
 {
-       int num_tiles;
-       num_tiles = HASH_COUNT(screen);
-       printf("Number of tiles: %d\n", num_tiles);
-       return sylvan_true;
+       BDD state = sylvan_false;
+       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;
+               }
+       }
+       return state;
 }
 
 BDD encode_rel(sokoban_screen *screen)