X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=66323454384e1ab905439a24af68ea95a323ce1e;hb=66136542e2b9208dd3a7b7e2f9bd0ea3f6418a6b;hp=dec0a284c7ecc095c512c0d097cff9e00ba941ad;hpb=398bd3da91c0916cd22ecab17da1b24eb549a9a0;p=mc1516pa.git

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index dec0a28..6632345 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -37,72 +37,136 @@
 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;
 		}
 	}