X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=bf165a7082133c8f362751b8a8b2398878d14faf;hb=d1d4ef8e109fe6a6e70836e7d9e59ace07e3814d;hp=68ad5a3ae0715810355e31bbf6e84f9ed2d46b8d;hpb=3461b7c4dd08242328dd59b44c6ddbcc00af6a0e;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 68ad5a3..bf165a7 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -30,14 +30,154 @@
  * 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)