repositories
/
mc1516pa.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
2b56327
)
transitions update
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 21:19:29 +0000
(22:19 +0100)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 21:19:29 +0000
(22:19 +0100)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
4bb4910
..
34bcb24
100644
(file)
--- a/
modelchecker/coord.c
+++ b/
modelchecker/coord.c
@@
-340,25
+340,44
@@
BDD encode_rel(sokoban_screen *screen)
}
if (tmp_scr->tile == TARGAGENT){
//1 1 1 1 0 0 (1 1 0 -> 1 1 0)
}
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);
+ 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, 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) == 0){
sokoban_screen *tmp_scr = get_coord(x, y, screen);
sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
}
}
else if (check_space(x, y, LEFT, 1, bm) == 1 && check_space(x, y, LEFT, 2, bm) == 0){
sokoban_screen *tmp_scr = get_coord(x, y, screen);
sokoban_screen *tmp_scr_d = get_coord(x - 1, y, screen);
+ xy_bddvar_map *bddvar = getxy(x - 1, y, bm->f);
+ int deltai = bddvar->value.var[0];
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == FREE){
- //can move
+ //(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};
+ BDDSET relvarset = sylvan_set_fromarray(relvars, 12);
+ uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGET){
- //can move
+ //(0 1 1 0 1 1 1 0 0 1 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, 1, 1, 0, 1, 1, 1, 0, 0, 1, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == FREE){
- //can move
+ //(0 1 0 1 1 0 1 0 1 0 0 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, 1, 0, 1, 1, 0, 1, 0, 1, 0, 0, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGET){
- //can move
+ //(0 1 1 1 1 0 1 0 1 1 0 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, 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 || tmp_scr_d->tile == TARGBOX)){
//can't move