repositories
/
mc1516pa.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
2a66deb
)
transitions update
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 20:16:52 +0000
(21:16 +0100)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 20:16:52 +0000
(21:16 +0100)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
3c14e56
..
4bb4910
100644
(file)
--- a/
modelchecker/coord.c
+++ b/
modelchecker/coord.c
@@
-311,18
+311,17
@@
test_relprod()
BDD encode_rel(sokoban_screen *screen)
{
BDD encode_rel(sokoban_screen *screen)
{
- int tile_count = 0;
+ LACE_ME;
+ // int tile_count = 0;
BDD t = sylvan_false;
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;
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++){
//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){
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){
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){
}
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){
}
}
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
}
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){
}
}
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
}
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 == 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
}
//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){
//can't move
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){