From 37c3344e7c8daf73cbcf72e7152dc2aeac6b5691 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Mon, 11 Apr 2016 23:29:07 +0100 Subject: [PATCH] left trans rel is ready --- modelchecker/coord.c | 48 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index b586629..5a6c90a 100644 --- 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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) + 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); -- 2.20.1