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

again, transitions update
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 34bcb24..a79254b 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -379,11 +379,33 @@ BDD encode_rel(sokoban_screen *screen)
 				uint8_t rel_enc[12] = {0, 1, 1, 1, 1, 0, 1, 0, 1, 1, 0, 1};
 				t = sylvan_union_cube(t, relvarset, rel_enc);
 			}
-			if (tmp_scr->tile == AGENT && (tmp_scr_d->tile == BOX || tmp_scr_d->tile == TARGBOX)){
-				//can't move
+			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX){
+				//(0 0 1 1 0 0 1 1 0 0 1 1)
+				BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
+				BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
+				uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+				t = sylvan_union_cube(t, relvarset, rel_enc);
 			}
-			if (tmp_scr->tile == TARGAGENT && (tmp_scr_d->tile == BOX || tmp_scr_d->tile == TARGBOX)){
-				//can't move
+			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX){
+				//(1 1 0 0 0 0 1 1 0 0 1 1)
+				BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
+				BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
+				uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1};
+				t = sylvan_union_cube(t, relvarset, rel_enc);
+			}
+			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX){
+				//(0 0 1 1 0 0 1 1 1 1 0 0)
+				BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
+				BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
+				uint8_t rel_enc[12] = {0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+				t = sylvan_union_cube(t, relvarset, rel_enc);
+			}
+			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX){
+				//(1 1 0 0 0 0 1 1 1 1 0 0)
+				BDDVAR relvars[12]  = {deltai*3, deltai*3+1, deltai*3+2, deltai*3+3, deltai*3+4, deltai*3+5, i*3, i*3+1, i*3+2, i*3+3, i*3+4, i*3+5};
+				BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
+				uint8_t rel_enc[12] = {1, 1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0};
+				t = sylvan_union_cube(t, relvarset, rel_enc);
 			}
 		}
 		else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 1){