From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Mon, 11 Apr 2016 20:16:52 +0000 (+0100)
Subject: transitions update
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=2b563274d5be82064d132314c31775119fdeeb9c;p=mc1516pa.git

transitions update
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 3c14e56..4bb4910 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -311,18 +311,17 @@ test_relprod()
 
 BDD encode_rel(sokoban_screen *screen)
 {
-	int tile_count = 0;
+	LACE_ME;
+	//	int tile_count = 0;
 	BDD t = sylvan_false;
-	BDDVAR *relvars;
-	uint8_t *rel_enc;
+	//BDDVAR relvars[];
+	//BDDSET relvarset;
+	//uint8_t rel_enc[];
 
 	bimap *bm = create_bimap_helper(screen);
 	int x = 0;
 	int y = 0;
 	bddvar_xy_map *bddxy = NULL;
-	tmp_scr *screen = NULL;
-	tmp_scr_d *screen = NULL;
-	tmp_scr_g *screen = NULL;
 
 	//left relation
 	for (unsigned int i = 0; i < HASH_COUNT(screen); i++){
@@ -331,17 +330,24 @@ BDD encode_rel(sokoban_screen *screen)
 		x = bddxy->value.x;
 		y = bddxy->value.y;
 		if (check_space(x, y, LEFT, 1, bm) == 0){
-			tmp_scr = get_coord(x, y, screen);
+			sokoban_screen *tmp_scr = get_coord(x, y, screen);
 			if (tmp_scr->tile == AGENT){
-
+				//1 1 0 0 1 1 (1 0 1 -> 1 0 1)
+				BDDVAR relvars[6]  = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
+				BDDSET relvarset = sylvan_set_fromarray(relvars, 6);
+				uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1};
+				t = sylvan_union_cube(t, relvarset, rel_enc);
 			}
 			if (tmp_scr->tile == TARGAGENT){
-
+				//1 1 1 1 0 0 (1 1 0 -> 1 1 0)
+				//relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5};
+				//rel_enc[6] = {1, 1, 1, 1, 0, 0};
+				//relvarset = sylvan_union_cube(t, relvarset, rel_enc);
 			}
 		}
 		else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){
-			tmp_scr = get_coord(x, y, screen);
-			tmp_scr_d = get_coord(x - 1, y, screen);
+			sokoban_screen *tmp_scr = get_coord(x, y, screen);
+			sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 				//can move
 			}
@@ -362,9 +368,9 @@ BDD encode_rel(sokoban_screen *screen)
 			}
 		}
 		else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){
-			tmp_scr = get_coord(x, y, screen);
-			tmp_scr_d = get_coord(x - 1, y, screen);
-			tmp_scr_g = get_coord(x - 2, y, screen);
+			sokoban_screen *tmp_scr = get_coord(x, y, screen);
+			sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
+			sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen);
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 				//can move
 			}
@@ -377,10 +383,10 @@ BDD encode_rel(sokoban_screen *screen)
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
 				//can move
 			}
-			if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g == TARGBOX)){
+			if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){
 				//can't move
 			}
-			if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g == TARGBOX)){
+			if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && (tmp_scr_g->tile == BOX || tmp_scr_g->tile == TARGBOX)){
 				//can't move
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){