From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 7 Apr 2016 10:49:25 +0000 (+0100)
Subject: encoding update (unfinished)
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;ds=sidebyside;h=398bd3da91c0916cd22ecab17da1b24eb549a9a0;hp=3461b7c4dd08242328dd59b44c6ddbcc00af6a0e;p=mc1516pa.git

encoding update (unfinished)
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 68ad5a3..dec0a28 100644
--- 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)