repositories
/
mc1516pa.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
398bd3d
)
state encoding done (needs checking)
author
Alexander Fedotov
<soyaxhoya@gmail.com>
Thu, 7 Apr 2016 11:10:33 +0000
(12:10 +0100)
committer
Alexander Fedotov
<soyaxhoya@gmail.com>
Thu, 7 Apr 2016 11:10:33 +0000
(12:10 +0100)
modelchecker/coord.c
patch
|
blob
|
history
diff --git
a/modelchecker/coord.c
b/modelchecker/coord.c
index
dec0a28
..
bf165a7
100644
(file)
--- a/
modelchecker/coord.c
+++ b/
modelchecker/coord.c
@@
-37,70
+37,141
@@
BDD encode_screen(sokoban_screen *screen)
{
BDD state = sylvan_false;
BDD encode_screen(sokoban_screen *screen)
{
BDD state = sylvan_false;
-
//
int tile_index = 0;
+ int tile_index = 0;
sokoban_screen *r;
sokoban_screen *r;
+ LACE_ME;
for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
switch(r->tile){
case FREE:
if (state == sylvan_false){
for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
switch(r->tile){
case FREE:
if (state == sylvan_false){
-
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
break;
case WALL:
if (state == sylvan_false){
}
printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y);
break;
case WALL:
if (state == sylvan_false){
-
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
break;
case BOX:
if (state == sylvan_false){
}
printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y);
break;
case BOX:
if (state == sylvan_false){
-
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
break;
case TARGET:
if (state == sylvan_false){
}
printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y);
break;
case TARGET:
if (state == sylvan_false){
-
+ state = sylvan_not(sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
break;
case AGENT:
if (state == sylvan_false){
}
printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y);
break;
case AGENT:
if (state == sylvan_false){
-
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
}
printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
break;
case TARGAGENT:
if (state == sylvan_false){
}
printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y);
break;
case TARGAGENT:
if (state == sylvan_false){
-
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
break;
case TARGBOX:
if (state == sylvan_false){
}
printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y);
break;
case TARGBOX:
if (state == sylvan_false){
-
+ state = sylvan_ithvar(tile_index);
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
else {
}
else {
-
+ state = sylvan_and(state, sylvan_ithvar(tile_index));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
+ state = sylvan_and(state, sylvan_not(sylvan_ithvar(tile_index)));
+ tile_index++;
}
printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
break;
}
printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y);
break;