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

trans upd
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index ca75a14..b586629 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -414,8 +414,8 @@ BDD encode_rel(sokoban_screen *screen)
 			sokoban_screen *tmp_scr_g = get_coord(x - 2, y, screen);
 			xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
 			int deltai = bddvar->value.var[0];
-			//			bddvar = getxy(x - 2, y, bm->f);
-			//			int gammai = bddvar->value.var[0];
+			bddvar = getxy(x - 2, y, bm->f);
+			int gammai = bddvar->value.var[0];
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
 				//(0 1 0 0 1 1 1 0 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};
@@ -445,40 +445,48 @@ BDD encode_rel(sokoban_screen *screen)
 				t = sylvan_union_cube(t, relvarset, rel_enc);
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
-				//can't move
+				//(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
-				//can't move
+				//(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
-				//can't move
+				//(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
-				//can't move
+				//(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
-				//can move
+				//free box agent -> box agent free
+				//(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
-				//can move
+				//(free targbox agent -> box targagent free)
+				//(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
-				//can move
+				//(target box agent -> targbox agent free)
+				//(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
 			}
 			if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
-				//can move
+				//(target targbox agent -> targbox targagent free)
+				//(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
-				//can move
+				//(free box targagent -> box agent target)
+				//(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
-				//can move
+				//(free targbox targagent -> box targagent target)
+				//(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
-				//can move
+				//(target box targagent -> targbox agent target)
+				//(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
 			}
 			if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
-				//can move
+				//(target targbox targagent -> targbox targagent target)
+				//(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
 			}
 		}
 		printf("x:%d y:%d\n", x, y);