From 961d38840cf50e864cb83711bd9419033c3acd7d Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Fri, 15 Apr 2016 10:40:16 +0200 Subject: [PATCH] small update --- modelchecker/coord.c | 868 +++++++++++++------------------------------ modelchecker/coord.h | 4 +- modelchecker/main.c | 5 +- 3 files changed, 264 insertions(+), 613 deletions(-) diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 3cd3a9a..d9a924a 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -1,17 +1,7 @@ #include -#include -#include #include #include -#include -#include - -#ifdef HAVE_PROFILER -#include -#endif - #include -#include #include #include "coord.h" @@ -191,6 +181,7 @@ state *encode_screen(sokoban_screen *screen) tile_index++; st_enc[tile_index] = 0; tile_index++; + st_enc[tile_index] = 1; tile_index++; break; @@ -218,6 +209,9 @@ state *encode_screen(sokoban_screen *screen) return fullState; } +//test +int countTrans(trans_t *trs); + trans_t *create_single_rel(sokoban_screen *screen, direction dir) { LACE_ME; @@ -263,10 +257,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) x = bddxy->value.x; y = bddxy->value.y; if (check_space(x, y, dir, 1, bm) == 0){ - //Agent -> Agent //1 1 0 0 1 1 (1 0 1 -> 1 0 1) - BDDVAR relvars[6] = {i * 3, i * 3 + 1, i * 3 + 2, i * 3 + 3, i * 3 + 4, i * 3 + 5}; + BDDVAR relvars[6] = {i * 6, i * 6 + 1, i * 6 + 2, i * 6 + 3, i * 6 + 4, i * 6 + 5}; BDDSET relvarset = sylvan_set_fromarray(relvars, 6); uint8_t rel_enc[6] = {1, 1, 0, 0, 1, 1}; @@ -279,12 +272,6 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent -> Targagent //1 1 1 1 0 0 (1 1 0 -> 1 1 0) - relvars[0] = i * 3; - relvars[1] = i * 3 + 1; - relvars[2] = i * 3 + 2; - relvars[3] = i * 3 + 3; - relvars[4] = i * 3 + 4; - relvars[5] = i * 3 + 5; relvarset = sylvan_set_fromarray(relvars, 6); rel_enc[0] = 1; rel_enc[1] = 1; @@ -306,11 +293,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) xy_bddvar_map *bddvar = getxy(x + xdelta, y + ydelta, bm->f); int deltai = bddvar->value.var[0]; - //Free Agent -> Agent Free - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {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}; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5}; BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -318,33 +305,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Agent -> Targagent Free - //(0 1 1 1 1 0 1 0 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; + rel_enc[2] = 0; + rel_enc[3] = 0; rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 0; - rel_enc[9] = 0; + rel_enc[5] = 1; + rel_enc[6] = 0; + rel_enc[7] = 1; + rel_enc[8] = 1; + rel_enc[9] = 1; rel_enc[10] = 1; - rel_enc[11] = 1; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -352,32 +327,20 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Must be: Free Targagent -> Agent Target - //(0 1 0 0 1 1 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Free -> Target Agent + //(1 0 1 1 0 1 0 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 0; - rel_enc[4] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 0; rel_enc[5] = 1; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; + rel_enc[6] = 0; + rel_enc[7] = 1; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; rel_enc[11] = 1; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); @@ -386,33 +349,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Targagent -> Targagent Target - //(0 1 1 1 1 0 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Target -> Target Targagent + //(1 0 1 1 0 1 0 1 1 1 1 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; rel_enc[2] = 1; rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; + rel_enc[4] = 0; + rel_enc[5] = 1; + rel_enc[6] = 0; + rel_enc[7] = 1; rel_enc[8] = 1; rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 1; + rel_enc[10] = 1; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -420,33 +371,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Box Agent -> Box Agent - //(0 0 1 1 0 0 1 1 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Box -> Agent Box + //(1 1 0 0 1 1 0 0 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 0; - rel_enc[2] = 1; - rel_enc[3] = 1; - rel_enc[4] = 0; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; - rel_enc[8] = 0; - rel_enc[9] = 0; - rel_enc[10] = 1; - rel_enc[11] = 1; + rel_enc[0] = 1; + rel_enc[1] = 1; + rel_enc[2] = 0; + rel_enc[3] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; + rel_enc[6] = 0; + rel_enc[7] = 0; + rel_enc[8] = 1; + rel_enc[9] = 1; + rel_enc[10] = 0; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -454,33 +393,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Targbox Agent -> Targbox Agent - //(1 1 0 0 0 0 1 1 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Targbox -> Agent Targbox + //(1 1 0 0 1 1 1 1 0 0 0 0) relvarset = sylvan_set_fromarray(relvars, 12); rel_enc[0] = 1; rel_enc[1] = 1; rel_enc[2] = 0; rel_enc[3] = 0; - rel_enc[4] = 0; - rel_enc[5] = 0; + rel_enc[4] = 1; + rel_enc[5] = 1; rel_enc[6] = 1; rel_enc[7] = 1; rel_enc[8] = 0; rel_enc[9] = 0; - rel_enc[10] = 1; - rel_enc[11] = 1; + rel_enc[10] = 0; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -488,29 +415,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Box Targagent -> Box Targagent - //(0 0 1 1 0 0 1 1 1 1 0 0) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Box -> Targagent Box + //(1 1 1 1 0 0 0 0 1 1 0 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 0; + rel_enc[0] = 1; + rel_enc[1] = 1; rel_enc[2] = 1; rel_enc[3] = 1; rel_enc[4] = 0; rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 1; + rel_enc[6] = 0; + rel_enc[7] = 0; rel_enc[8] = 1; rel_enc[9] = 1; rel_enc[10] = 0; @@ -522,31 +437,19 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Targbox Targagent -> Targbox Targagent - //(1 1 0 0 0 0 1 1 1 1 0 0) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Targbox -> Targagent Targbox + //(1 1 1 1 0 0 1 1 0 0 0 0) relvarset = sylvan_set_fromarray(relvars, 12); rel_enc[0] = 1; rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 0; + rel_enc[2] = 1; + rel_enc[3] = 1; rel_enc[4] = 0; rel_enc[5] = 0; rel_enc[6] = 1; rel_enc[7] = 1; - rel_enc[8] = 1; - rel_enc[9] = 1; + rel_enc[8] = 0; + rel_enc[9] = 0; rel_enc[10] = 0; rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); @@ -564,11 +467,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) bddvar = getxy(x + xgamma, y + ygamma, bm->f); int gammai = bddvar->value.var[0]; - //Free Agent -> 1 0 1 0 0 1 Agent Free - //(0 1 0 0 1 1 1 0 0 0 1 1) - BDDVAR relvars[12] = {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}; + //Agent Free -> Free Agent + //(1 0 0 0 1 1 0 1 0 0 1 1) + BDDVAR relvars[12] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, i*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5}; BDDSET relvarset = sylvan_set_fromarray(relvars, 12); - uint8_t rel_enc[12] = {0, 1, 0, 0, 1, 1, 1, 0, 0, 0, 1, 1}; + uint8_t rel_enc[12] = {1, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 1}; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -576,33 +479,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Agent -> Targagent Free - //(0 1 1 1 1 0 1 0 0 0 1 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Agent Target -> Free Targagent + //(1 0 0 0 1 1 0 1 1 1 1 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 1; - rel_enc[3] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; + rel_enc[2] = 0; + rel_enc[3] = 0; rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 0; - rel_enc[9] = 0; + rel_enc[5] = 1; + rel_enc[6] = 0; + rel_enc[7] = 1; + rel_enc[8] = 1; + rel_enc[9] = 1; rel_enc[10] = 1; - rel_enc[11] = 1; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -610,32 +501,20 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Free Targagent -> Agent Target - //(0 1 0 0 1 1 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Free -> Target Agent + //(1 0 1 1 0 1 0 1 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; - rel_enc[2] = 0; - rel_enc[3] = 0; - rel_enc[4] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; + rel_enc[2] = 1; + rel_enc[3] = 1; + rel_enc[4] = 0; rel_enc[5] = 1; - rel_enc[6] = 1; - rel_enc[7] = 0; - rel_enc[8] = 1; - rel_enc[9] = 1; - rel_enc[10] = 0; + rel_enc[6] = 0; + rel_enc[7] = 1; + rel_enc[8] = 0; + rel_enc[9] = 0; + rel_enc[10] = 1; rel_enc[11] = 1; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); @@ -644,33 +523,21 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Targagent -> Targagent Target - //(0 1 1 1 1 0 1 0 1 1 0 1) - relvars[0] = deltai*3; - relvars[1] = deltai*3+1; - relvars[2] = deltai*3+2; - relvars[3] = deltai*3+3; - relvars[4] = deltai*3+4; - relvars[5] = deltai*3+5; - relvars[6] = i*3; - relvars[7] = i*3+1; - relvars[8] = i*3+2; - relvars[9] = i*3+3; - relvars[10] = i*3+4; - relvars[11] = i*3+5; + //Targagent Target -> Target Targagent + //(1 0 1 1 0 1 0 1 1 1 1 0) relvarset = sylvan_set_fromarray(relvars, 12); - rel_enc[0] = 0; - rel_enc[1] = 1; + rel_enc[0] = 1; + rel_enc[1] = 0; rel_enc[2] = 1; rel_enc[3] = 1; - rel_enc[4] = 1; - rel_enc[5] = 0; - rel_enc[6] = 1; - rel_enc[7] = 0; + rel_enc[4] = 0; + rel_enc[5] = 1; + rel_enc[6] = 0; + rel_enc[7] = 1; rel_enc[8] = 1; rel_enc[9] = 1; - rel_enc[10] = 0; - rel_enc[11] = 1; + rel_enc[10] = 1; + rel_enc[11] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset, rel_enc); trs_current->varset.varset = relvarset; @@ -678,48 +545,29 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Box Box Agent -> Box Box Agent - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - BDDVAR relvars1[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}; - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Box -> Agent Box Box + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) + BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, 2*deltai, 2*deltai+1, 2*deltai+2, 2*deltai+3, 2*deltai+4, 2*deltai+5, 2*gammai, 2*gammai+1, 2*gammai+2, 2*gammai+3, 2*gammai+4, 2*gammai+5}; BDD relvarset1 = sylvan_set_fromarray(relvars1, 18); uint8_t rel_enc1[18]; - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 0; - rel_enc1[2] = 1; - rel_enc1[3] = 1; - rel_enc1[4] = 0; - rel_enc1[5] = 0; + rel_enc1[0] = 1; + rel_enc1[1] = 1; + rel_enc1[2] = 0; + rel_enc1[3] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 1; rel_enc1[6] = 0; rel_enc1[7] = 0; rel_enc1[8] = 1; rel_enc1[9] = 1; rel_enc1[10] = 0; rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; - rel_enc1[14] = 0; - rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[12] = 0; + rel_enc1[13] = 0; + rel_enc1[14] = 1; + rel_enc1[15] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -727,34 +575,15 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Targbox Box Agent -> Targbox Box Agent - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Targbox -> Agent Box Targbox + //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) rel_enc1[0] = 1; rel_enc1[1] = 1; rel_enc1[2] = 0; rel_enc1[3] = 0; - rel_enc1[4] = 0; - rel_enc1[5] = 0; + rel_enc1[4] = 1; + rel_enc1[5] = 1; rel_enc1[6] = 0; rel_enc1[7] = 0; rel_enc1[8] = 1; @@ -765,8 +594,8 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) rel_enc1[13] = 1; rel_enc1[14] = 0; rel_enc1[15] = 0; - rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[16] = 0; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -774,30 +603,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Box Box Targagent -> Box Box Targagent - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Box -> Targagent Box Box + //(1 1 1 1 0 0 0 0 1 1 0 0 0 0 1 1 0 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - rel_enc1[0] = 0; - rel_enc1[1] = 0; + rel_enc1[0] = 1; + rel_enc1[1] = 1; rel_enc1[2] = 1; rel_enc1[3] = 1; rel_enc1[4] = 0; @@ -808,8 +618,8 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) rel_enc1[9] = 1; rel_enc1[10] = 0; rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 1; + rel_enc1[12] = 0; + rel_enc1[13] = 0; rel_enc1[14] = 1; rel_enc1[15] = 1; rel_enc1[16] = 0; @@ -821,32 +631,13 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Targbox Box Targagent -> Targbox Box Targagent - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Targbox -> Targagent Box Targbox + //(1 1 1 1 0 0 0 0 1 1 0 0 1 1 0 0 0 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 1 1 0 0) rel_enc1[0] = 1; rel_enc1[1] = 1; - rel_enc1[2] = 0; - rel_enc1[3] = 0; + rel_enc1[2] = 1; + rel_enc1[3] = 1; rel_enc1[4] = 0; rel_enc1[5] = 0; rel_enc1[6] = 0; @@ -857,8 +648,8 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) rel_enc1[11] = 0; rel_enc1[12] = 1; rel_enc1[13] = 1; - rel_enc1[14] = 1; - rel_enc1[15] = 1; + rel_enc1[14] = 0; + rel_enc1[15] = 0; rel_enc1[16] = 0; rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); @@ -868,46 +659,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Free Box Agent -> Box Agent Free - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Free -> Free Agent Box + //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - rel_enc1[0] = 0; + rel_enc1[0] = 1; rel_enc1[1] = 0; rel_enc1[2] = 0; - rel_enc1[3] = 1; + rel_enc1[3] = 0; rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 0; rel_enc1[7] = 1; rel_enc1[8] = 1; rel_enc1[9] = 0; rel_enc1[10] = 0; rel_enc1[11] = 1; - rel_enc1[12] = 1; + rel_enc1[12] = 0; rel_enc1[13] = 0; rel_enc1[14] = 0; - rel_enc1[15] = 0; + rel_enc1[15] = 1; rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -915,46 +687,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Free Targbox Agent -> Box Targagent Free - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Targbox Free -> Free Targagent Box + //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - rel_enc1[0] = 0; + rel_enc1[0] = 1; rel_enc1[1] = 0; rel_enc1[2] = 0; - rel_enc1[3] = 1; + rel_enc1[3] = 0; rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 1; rel_enc1[7] = 1; rel_enc1[8] = 0; rel_enc1[9] = 1; rel_enc1[10] = 0; rel_enc1[11] = 0; - rel_enc1[12] = 1; + rel_enc1[12] = 0; rel_enc1[13] = 0; rel_enc1[14] = 0; - rel_enc1[15] = 0; + rel_enc1[15] = 1; rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -962,46 +715,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Box Agent -> Targbox Agent Free - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Box Target -> Free Agent Targbox + //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; + rel_enc1[0] = 1; + rel_enc1[1] = 0; + rel_enc1[2] = 0; rel_enc1[3] = 0; rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 0; rel_enc1[7] = 1; rel_enc1[8] = 1; rel_enc1[9] = 0; rel_enc1[10] = 0; rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; + rel_enc1[12] = 0; + rel_enc1[13] = 1; + rel_enc1[14] = 1; rel_enc1[15] = 0; rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1009,46 +743,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Targbox Agent -> Targbox Targagent Free - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Agent Targbox Target -> Free Targagent Targbox + //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 0 0 1 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; - rel_enc1[2] = 1; + rel_enc1[0] = 1; + rel_enc1[1] = 0; + rel_enc1[2] = 0; rel_enc1[3] = 0; rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 1; rel_enc1[7] = 1; rel_enc1[8] = 0; rel_enc1[9] = 1; rel_enc1[10] = 0; rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; - rel_enc1[14] = 0; + rel_enc1[12] = 0; + rel_enc1[13] = 1; + rel_enc1[14] = 1; rel_enc1[15] = 0; rel_enc1[16] = 1; - rel_enc1[17] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1056,28 +771,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Free Box Targagent -> Box Agent Target - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Free -> Target Agent Box + //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) rel_enc1[0] = 0; rel_enc1[1] = 0; rel_enc1[2] = 0; @@ -1103,28 +799,9 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Free Targbox Targagent -> Box Targagent Target - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Targbox Free -> Target Targagent Box + //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) rel_enc1[0] = 0; rel_enc1[1] = 0; rel_enc1[2] = 0; @@ -1150,46 +827,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Box Targagent -> Targbox Agent Target - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Box Target -> Target Agent Targbox + //(1 0 1 1 0 1 0 1 1 0 0 1 0 1 1 0 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; + rel_enc1[0] = 1; + rel_enc1[1] = 0; rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 0; rel_enc1[7] = 1; rel_enc1[8] = 1; rel_enc1[9] = 0; rel_enc1[10] = 0; rel_enc1[11] = 1; - rel_enc1[12] = 1; - rel_enc1[13] = 0; + rel_enc1[12] = 0; + rel_enc1[13] = 1; rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1197,46 +855,27 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs_current->next_rel = trs; trs = trs_current; - //Target Targbox Targagent -> Targbox Targagent Target - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - relvars1[0] = gammai*3; - relvars1[1] = gammai*3+1; - relvars1[2] = gammai*3+2; - relvars1[3] = gammai*3+3; - relvars1[4] = gammai*3+4; - relvars1[5] = gammai*3+5; - relvars1[6] = deltai*3; - relvars1[7] = deltai*3+1; - relvars1[8] = deltai*3+2; - relvars1[9] = deltai*3+3; - relvars1[10] = deltai*3+4; - relvars1[11] = deltai*3+5; - relvars1[12] = i*3; - relvars1[13] = i*3+1; - relvars1[14] = i*3+2; - relvars1[15] = i*3+3; - relvars1[16] = i*3+4; - relvars1[17] = i*3+5; + //Targagent Targbox Target -> Target Targagent Targbox + //(1 0 1 1 0 1 1 1 0 1 0 0 0 1 1 0 1 0) relvarset1 = sylvan_set_fromarray(relvars1, 18); - //(0 1 1 0 1 0 1 1 0 1 0 0 1 0 1 1 0 1) - rel_enc1[0] = 0; - rel_enc1[1] = 1; + rel_enc1[0] = 1; + rel_enc1[1] = 0; rel_enc1[2] = 1; - rel_enc1[3] = 0; - rel_enc1[4] = 1; - rel_enc1[5] = 0; + rel_enc1[3] = 1; + rel_enc1[4] = 0; + rel_enc1[5] = 1; rel_enc1[6] = 1; rel_enc1[7] = 1; rel_enc1[8] = 0; rel_enc1[9] = 1; rel_enc1[10] = 0; rel_enc1[11] = 0; - rel_enc1[12] = 1; - rel_enc1[13] = 0; + rel_enc1[12] = 0; + rel_enc1[13] = 1; rel_enc1[14] = 1; - rel_enc1[15] = 1; - rel_enc1[16] = 0; - rel_enc1[17] = 1; + rel_enc1[15] = 0; + rel_enc1[16] = 1; + rel_enc1[17] = 0; trs_current = (trans_t *)malloc(sizeof(trans_t)); trs_current->bdd = sylvan_cube(relvarset1, rel_enc1); trs_current->varset.varset = relvarset1; @@ -1246,9 +885,45 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) } } trs_current = trs; + + //test + switch(dir){ + case LEFT: + if (trs_current != NULL) printf("LEFT ok!\n"); + else printf ("LEFT is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case UP: + if (trs_current != NULL) printf("UP ok!\n"); + else printf ("UP is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case RIGHT: + if (trs_current != NULL) printf("RIGHT ok!\n"); + else printf ("RIGHT is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + case DOWN: + if (trs_current != NULL) printf("DOWN ok!\n"); + else printf ("DOWN is empty\n"); + printf("Num of trans relations:%d\n", countTrans(trs)); + break; + } + return trs; } +//test +int countTrans(trans_t *trs) +{ + int counter = 0; + while (trs != NULL){ + counter++; + trs = trs->next_rel; + } + return counter; +} + rels *encode_rel(sokoban_screen *screen) { LACE_ME; @@ -1277,45 +952,18 @@ rels *encode_rel(sokoban_screen *screen) return rls; } -int -test_relprod() +int test_trans(state *s, trans_t *t) { LACE_ME; - - BDDVAR vars[] = {0,2,4}; - BDDVAR all_vars[] = {0,1,2,3,4,5}; - BDDVAR all_vars2[] = {0,1}; - //BDDVAR short_vars[] = {0,1}; - /*BDDVAR short_vars2[] = {2,3}; - BDDVAR short_vars3[] = {0,1,2,3};*/ - - BDDSET vars_set = sylvan_set_fromarray(vars, 3); - BDDSET all_vars_set = sylvan_set_fromarray(all_vars, 6); - BDDSET all_vars_set2 = sylvan_set_fromarray(all_vars2, 2); - //BDDSET short_vars_set = sylvan_set_fromarray(short_vars, 2); - /*BDDSET short_vars_set2 = sylvan_set_fromarray(short_vars2, 2); - BDDSET short_vars_set3 = sylvan_set_fromarray(short_vars3, 4);*/ - - BDD s, t, next, prev; - BDD zeroes, ones; - - // transition relation: 000 --> 111 and !000 --> 000 - t = sylvan_false; - t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){0,1})); - //t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){1,0,2,0,2,0})); - t = sylvan_union_cube(t, all_vars_set2, ((uint8_t[]){1,0})); - // t = sylvan_union_cube(t, all_vars_set, ((uint8_t[]){0,1})); - - s = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - zeroes = sylvan_cube(vars_set, (uint8_t[]){1,0,0}); - ones = sylvan_cube(vars_set, (uint8_t[]){0,0,0}); - - next = sylvan_relnext(s, t, all_vars_set); - prev = sylvan_relprev(t, next, all_vars_set); - if (next == zeroes) printf("Pass 1\n"); - if (prev == ones) printf("Pass 2\n"); - //trans *ts; - //ts = NULL; - - return 0; + int counter = 0; + BDD next = sylvan_false; + while (t != NULL){ + next = sylvan_relnext(s->bdd, t->bdd, t->varset.varset); + if (next == s->bdd) printf("Same\n"); + if (next != s->bdd && next != sylvan_false) printf("Different\n"); + if (next == sylvan_false) printf("False\n"); + t = t->next_rel; + } + printf("Trans:%d\n", counter); + return 1; } diff --git a/modelchecker/coord.h b/modelchecker/coord.h index 33f7e91..56f770f 100644 --- a/modelchecker/coord.h +++ b/modelchecker/coord.h @@ -32,6 +32,8 @@ state *encode_screen(sokoban_screen *screen); rels *encode_rel(sokoban_screen *screen); -//int test_relprod(); +int test_trans(state *s, trans_t *t); + +int test_relprod(); #endif diff --git a/modelchecker/main.c b/modelchecker/main.c index 6b1c0d4..8ee1bd3 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -61,9 +61,10 @@ void solve(FILE *inputstream) switch(strat){ case COORD: DPRINT("Encoding coordinate based\n"); - //encode_screen(screen); + state *s = encode_screen(screen); //test_relprod(); - encode_rel(screen); + rels *rls = encode_rel(screen); + test_trans(s, rls->relr); break; case OBJECT: DPRINT("Encoding object based\n"); -- 2.20.1