X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fcoord.c;h=f9dd7e5c7abe754af61a6b1dc2795bdb86c2b767;hb=8054a7885e6e03b2998bf5bfd3b415816cd61cf9;hp=200db36abd4b2d57a35604809303c56b86646843;hpb=20e06a2f606199140022d17e16f0f58d807f1b0f;p=mc1516pa.git diff --git a/modelchecker/coord.c b/modelchecker/coord.c index 200db36..f9dd7e5 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -312,14 +312,14 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Target -> Free Targagent //(1 0 0 0 1 1 0 1 1 1 1 0) //or - //(0 1 1 1 1 0 0 1 1 1 1 0) + //(0 1 1 1 1 0 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); if (i < deltai){ uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); } else { - uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0}; + uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); } trs_current = (trans_t *)malloc(sizeof(trans_t)); @@ -539,16 +539,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Box -> Agent Box Box //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 (i delta gamma) //or - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (delta gamma i) //or - //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) //or - //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) + //(1 1 0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0) (i gamma delta) //or - //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) + //(0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (delta i gamma) //or - //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + //(0 0 1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) BDDVAR relvars1[18] = {i*6, i*6+1, i*6+2, i*6+3, i*6+4, i*6+5, deltai, deltai+1, deltai+2, deltai+3, deltai+4, deltai+5, gammai, gammai+1, gammai+2, gammai+3, gammai+4, gammai+5}; BDD relvarset1 = sylvan_set_fromarray(relvars1, 18); uint8_t rel_enc1[18]; @@ -569,11 +570,11 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else if ((deltai < i) < gammai){ - uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1}; + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { - uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0}; + uint8_t rel_enc__[18] = {0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } @@ -585,17 +586,17 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs = trs_current; //Agent Box Targbox -> Agent Box Targbox (LEFT || UP) - //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) + //(1 1 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 0) (i delta gamma) //or - //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) + //(0 0 1 1 0 0 1 1 0 0 0 0 1 1 0 0 1 1) (delta gamma i) //or - //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) + //(1 1 0 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0) (gamma i delta) //or - //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) + //(1 1 0 0 1 1 1 1 0 0 0 0 0 0 1 1 0 0) (i gamma delta) //or - //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) + //(0 0 1 1 0 0 1 1 0 0 1 1 1 1 0 0 0 0) (delta i gamma) //or - //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) + //(1 1 0 0 0 0 0 0 1 1 0 0 1 1 0 0 1 1) (gamma delta i) relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 1, 1, 0, 0, 0, 0}; @@ -718,16 +719,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Free -> Free Agent Box //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) + //(1 0 0 0 1 1 0 1 1 0 0 1 0 0 0 1 1 0) //or //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1) + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 0 0 1 1 //or //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //(0 0 0 1 1 0 1 0 0 0 1 1 0 1 1 0 0 1 //or //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1) + //(1 0 0 0 1 1 0 0 0 1 1 0 0 1 1 0 0 1 //or //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0) + //(0 1 1 0 0 1 1 0 0 0 1 1 0 0 0 1 1 0 //or //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 0 1 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; @@ -762,16 +769,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Targbox Free -> Free Targagent Box //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0) + //(1 0 0 0 1 1 1 1 0 1 0 0 0 0 0 1 1 0 //or //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1) + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 0 0 1 1 //or //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0) + //(0 0 0 1 1 0 1 0 0 0 1 1 1 1 0 1 0 0 //or //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0) + //(1 0 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 0 //or //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0) + //(1 1 0 1 0 0 1 0 0 0 1 1 0 0 0 1 1 0 //or //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1) + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 0 0 1 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; @@ -806,16 +819,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Box Target -> Free Agent Targbox //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0) + //(1 0 0 0 1 1 0 1 1 0 0 1 0 1 1 0 1 0 //or //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1) + //(0 1 1 0 0 1 0 1 1 0 1 0 1 0 0 0 1 1 //or //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1) + //(0 1 1 0 1 0 1 0 0 0 1 1 0 1 1 0 0 1 //or //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1) + //(1 0 0 0 1 1 0 1 1 0 1 0 0 1 1 0 0 1 //or //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0) + //(0 1 1 0 0 1 1 0 0 0 1 1 0 1 1 0 1 0 //or //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1) + //(0 1 1 0 1 0 0 1 1 0 0 1 1 0 0 0 1 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0}; @@ -850,6 +869,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Agent Targbox Target -> Free Targagent Targbox //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0) + //(1 0 0 0 1 1 1 1 0 1 0 0 0 1 1 0 1 0 //or //(1 1 0 1 0 0 0 1 1 0 1 0 1 0 0 0 1 1) //or @@ -894,16 +914,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent Box Free -> Target Agent Box //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0) + //(1 0 1 1 0 1 0 1 1 0 0 1 0 0 0 1 1 0 //or //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1) + //(0 1 1 0 0 1 0 0 0 1 1 0 1 0 1 1 0 1 //or //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1) + //(0 0 0 1 1 0 1 0 1 1 0 1 0 1 1 0 0 1 //or //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1) + //(1 0 1 1 0 1 0 0 0 1 1 0 0 1 1 0 0 1 //or //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0) + //(0 1 1 0 0 1 1 0 1 1 0 1 0 0 0 1 1 0 //or //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1) + //(0 0 0 1 1 0 0 1 1 0 0 1 1 0 1 1 0 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0, 1, 1, 0}; @@ -938,16 +964,22 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) //Targagent Targbox Free -> Target Targagent Box //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0) + //(1 0 1 1 0 1 1 1 0 1 0 0 0 0 0 1 1 0 //or //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1) + //(1 1 0 1 0 0 0 0 0 1 1 0 1 0 1 1 0 1 //or //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0) + //(0 0 0 1 1 0 1 0 1 1 0 1 1 1 0 1 0 0 //or //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0) + //(1 0 1 1 0 1 0 0 0 1 1 0 1 1 0 1 0 0 //or //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0) + //(1 1 0 1 0 0 1 0 1 1 0 1 0 0 0 1 1 0 //or //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1) + //(0 0 0 1 1 0 1 1 0 1 0 0 1 0 1 1 0 1 relvarset1 = sylvan_set_fromarray(relvars1, 18); if ((i < deltai) < gammai){ uint8_t rel_enc__[18] = {1, 0, 1, 1, 0, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0, 1, 1, 0}; @@ -966,7 +998,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else if ((deltai < i) < gammai){ - uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, 1, 1, 0}; + uint8_t rel_enc__[18] = {1, 1, 0, 1, 0, 0, 1, 0, 1, 1, 0, 1, 0, 0, 0, ,1 ,1, 0}; memcpy(rel_enc1, rel_enc__, 18*sizeof(uint8_t)); } else { @@ -1072,6 +1104,7 @@ 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"); @@ -1094,7 +1127,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) printf("Num of trans relations:%d\n", countTrans(trs)); break; } - + */ return trs; }