From 0a8ebd63de0624a2fc002a78e092694893016d41 Mon Sep 17 00:00:00 2001
From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Mon, 11 Apr 2016 11:23:05 +0100
Subject: [PATCH] state encoding as it has to be

---
 modelchecker/coord.c | 228 +++++++++++++++++--------------------------
 modelchecker/coord.h |   2 +
 modelchecker/main.c  |   1 +
 3 files changed, 92 insertions(+), 139 deletions(-)

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 8905a17..8641bad 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -57,6 +57,23 @@ typedef struct {
 	BDD *reld;
 } rels;
 
+typedef struct {
+	int *vars;
+	int size;
+} variables;
+
+typedef struct
+{
+    BDD bdd;
+    BDD variables;
+} *state;
+
+typedef struct
+{
+    BDD bdd;
+    BDD variables;
+} *trans;
+
 xy_bddvar_map *getxy(int x, int y, xy_bddvar_map *map)
 {
 	xy_bddvar_map k, *r = NULL;
@@ -175,141 +192,80 @@ bimap *create_bimap_helper(sokoban_screen *screen)
 
 BDD encode_screen(sokoban_screen *screen)
 {
-	BDD state = sylvan_false;
+	LACE_ME;
+
+	BDDVAR vars[HASH_COUNT(screen) * 3];
+	for (uint8_t i = 0; i < HASH_COUNT(screen) * 3; i++){
+		vars[i] = i;
+	}
+
+	uint8_t st_enc[HASH_COUNT(screen) * 3];
+
+	BDDSET varset = sylvan_set_fromarray(vars, HASH_COUNT(screen) * 3);
+	BDD state;
 	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++;
-			}
+		case FREE: //001
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
 			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++;
-			}
+		case WALL: //000
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
 			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++;
-			}
+		case BOX: //010
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
 			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++;
-			}
+		case TARGET: //011
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
 			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++;
-			}
+		case AGENT: //101
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
 			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++;
-			}
+		case TARGAGENT: //110
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
 			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++;
-			}
+		case TARGBOX: //100
+			st_enc[tile_index] = 1;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
+			st_enc[tile_index] = 0;
+			tile_index++;
 			break;
 		}
 	}
-	/*
+	/* some testing...
 	xy_bddvar_map *map = NULL;
 	map = create_xy_bddvar_map(screen);
 	xy_bddvar_map *m = getxy(1, 1, map);
@@ -319,7 +275,7 @@ BDD encode_screen(sokoban_screen *screen)
 	printf("Test1: %d %d\n", m->value.var[0], m->value.var[1]);
 	printf("Test2: %d %d\n", m2->value.x, m2->value.y);
 	*/
-	/*
+	/* some more testing...
 	bimap *bm = NULL;
 	bm = create_bimap_helper(screen);
 	xy_bddvar_map *m = getxy(1, 1, bm->f);
@@ -329,6 +285,8 @@ BDD encode_screen(sokoban_screen *screen)
 	printf("%d tiles were encoded\n", tile_index);
 	if (bm != NULL) printf ("WORKS!\n");
 	*/
+	state = sylvan_cube(varset, st_enc);
+	printf("Initial state encoded\n");
 	return state;
 }
 
@@ -337,22 +295,14 @@ BDD encode_rel(sokoban_screen *screen)
 	int num_tiles;
 	num_tiles = HASH_COUNT(screen);
 	printf("Number of tiles: %d\n", num_tiles);
-	return sylvan_true;
-}
 
-void test()
-{
+	//left relation
 
-	printf("Test!\n");
-	BDD a = sylvan_true;
-	BDD b = sylvan_not(a);
-	if (b == sylvan_false){
-		printf("BDD works!\n");
-	} else {
-		printf("BDD does not work!\n");
-	}
-	LACE_ME;
-	BDD c = sylvan_ithvar(1);
-	if (sylvan_high(c) == sylvan_true && sylvan_low(c) == sylvan_false) printf("VAR works 1\n");
-	if (sylvan_var(c) == 1) printf("Var works 2\n");
+	//up relation
+
+	//right relation
+
+	//down relation
+
+	return sylvan_true;
 }
diff --git a/modelchecker/coord.h b/modelchecker/coord.h
index 2580d60..2ec2918 100644
--- a/modelchecker/coord.h
+++ b/modelchecker/coord.h
@@ -7,4 +7,6 @@ BDD encode_screen(sokoban_screen *screen);
 
 BDD encode_rel(sokoban_screen *screen);
 
+//int test_relprod();
+
 #endif
diff --git a/modelchecker/main.c b/modelchecker/main.c
index e954c07..7940dc9 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -62,6 +62,7 @@ void solve(FILE *inputstream)
 		case COORD:
 			DPRINT("Encoding coordinate based\n");
 			encode_screen(screen);
+			//test_relprod();
 			break;
 		case OBJECT:
 			DPRINT("Encoding object based\n");
-- 
2.20.1