left trans rel is ready

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)
+                               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);