repositories
/
mc1516pa.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a598272
)
left trans rel is ready
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 22:29:07 +0000
(23:29 +0100)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Mon, 11 Apr 2016 22:29:07 +0000
(23:29 +0100)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
b586629
..
5a6c90a
100644
(file)
--- a/
modelchecker/coord.c
+++ b/
modelchecker/coord.c
@@
-446,47
+446,95
@@
BDD encode_rel(sokoban_screen *screen)
}
if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == BOX){
//(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 == BOX){
//(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d-> tile == BOX && tmp_scr_g->tile == TARGBOX){
//(1 1 0 0 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){
//(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 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_g->tile == BOX){
//(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 == BOX){
//(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 1, 1, 0, 0, 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 == BOX && tmp_scr_g->tile == TARGBOX){
//(1 1 0 0 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){
//(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {1, 1, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 1, 1, 0, 0};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
//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 == BOX && tmp_scr_g->tile == FREE){
//free box agent -> box agent free
//(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
//(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 == TARGBOX && tmp_scr_g->tile == FREE){
//(free targbox agent -> box targagent free)
//(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
//(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 == BOX && tmp_scr_g->tile == TARGET){
//(target box agent -> targbox agent free)
//(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
//(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 == AGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
//(target targbox agent -> targbox targagent free)
//(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0, 1, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == FREE){
//(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 == BOX && tmp_scr_g->tile == FREE){
//(free box targagent -> box agent target)
//(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == FREE){
//(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 == TARGBOX && tmp_scr_g->tile == FREE){
//(free targbox targagent -> box targagent target)
//(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 0, 0, 1, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == BOX && tmp_scr_g->tile == TARGET){
//(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 == BOX && tmp_scr_g->tile == TARGET){
//(target box targagent -> targbox agent target)
//(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
//(target targbox targagent -> targbox targagent target)
//(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
}
if (tmp_scr->tile == TARGAGENT && tmp_scr_d->tile == TARGBOX && tmp_scr_g->tile == TARGET){
//(target targbox targagent -> targbox targagent target)
//(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1)
+ BDDVAR relvars[18] = {gammai*3, gammai*3+1, gammai*3+2, gammai*3+3, gammai*3+4, gammai*3+5, 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, 18);
+ uint8_t rel_enc[18] = {0, 1, 1, 0, 1, 0, 1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1};
+ t = sylvan_union_cube(t, relvarset, rel_enc);
}
}
printf("x:%d y:%d\n", x, y);
}
}
printf("x:%d y:%d\n", x, y);