From d1d4ef8e109fe6a6e70836e7d9e59ace07e3814d Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Thu, 7 Apr 2016 12:10:33 +0100 Subject: [PATCH] state encoding done (needs checking) --- modelchecker/coord.c | 101 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 86 insertions(+), 15 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index dec0a28..bf165a7 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -37,70 +37,141 @@ BDD encode_screen(sokoban_screen *screen) { BDD state = sylvan_false; - //int tile_index = 0; + int tile_index = 0; 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){ - + 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 { - + 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){ - + 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 { - + 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){ - + 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 { - + 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){ - + 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 { - + 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){ - + 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 { - + 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){ - + 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 { - + 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){ - + 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 { - + 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; -- 2.20.1