encoding update (unfinished)

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 68ad5a3..dec0a28 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -30,14 +30,83 @@
  * 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;
+       for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+               switch(r->tile){
+               case FREE:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
+                       break;
+               case WALL:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
+                       break;
+               case BOX:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
+                       break;
+               case TARGET:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
+                       break;
+               case AGENT:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
+                       break;
+               case TARGAGENT:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
+                       break;
+               case TARGBOX:
+                       if (state == sylvan_false){
+
+                       }
+                       else {
+
+                       }
+                       printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
+                       break;
+               }
+       }
+       return state;
 }
 
 BDD encode_rel(sokoban_screen *screen)