From: Mart Lubbers Date: Tue, 12 Apr 2016 18:33:05 +0000 (+0200) Subject: started with transitions, I think agent transitions work... X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=b9448d600bb0f3249ae08db3a9ecd5f1f7794fda;p=mc1516pa.git started with transitions, I think agent transitions work... --- diff --git a/modelchecker/object.c b/modelchecker/object.c index 769163f..362802d 100644 --- a/modelchecker/object.c +++ b/modelchecker/object.c @@ -7,6 +7,8 @@ #define MAX_BOX 50 #define EPRINTF(fmt, as...) fprintf(stderr, fmt, ##as) +typedef enum {UP, DOWN, LEFT, RIGHT} direction; + int ilog2(int x) { int l = 1; @@ -27,9 +29,9 @@ void get_screen_metrics(sokoban_screen *screen, *agentx = 0; *agenty = 0; sokoban_screen *r; - for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){ + for(r=screen; r != NULL; r = r->hh.next){ *mx = r->coord.x > *mx ? r->coord.x : *mx; - *my = r->coord.x > *mx ? r->coord.x : *mx; + *my = r->coord.y > *my ? r->coord.x : *my; switch(r->tile){ case TARGAGENT: case AGENT: @@ -47,15 +49,16 @@ void get_screen_metrics(sokoban_screen *screen, } } +//LSB first BDD encode_int(BDD state, int x, int bx, int *variablenum) { LACE_ME; char *encoding = malloc(bx); for(int i = 0; i 0){ - state = sylvan_and(state, sylvan_ithvar(*variablenum)); + state = sylvan_and(state, sylvan_ithvar(*variablenum*2)); } else { - state = sylvan_and(state, sylvan_nithvar(*variablenum)); + state = sylvan_and(state, sylvan_nithvar(*variablenum*2)); } *variablenum += 1; } @@ -69,6 +72,83 @@ BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum) return encode_int(state, y, by, variablenum); } +BDD encode_transition(sokoban_screen *scr, BDD state, int bx, int by, int *varnum, direction dir) +{ + LACE_ME; + //Increase the position + int oldvarnum = *varnum; + + //RIGHT + if(dir == RIGHT){ + state = sylvan_and(state, + sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1))); + *varnum += 1; + for(int i = 1; ihh.next){ + int x = r->coord.x; + int y = r->coord.y; + *varnum = oldvarnum; + + BDD currentx = sylvan_true; + for(int i = 0; i 0){ + currentx = sylvan_and(currentx, sylvan_ithvar(*varnum*2+1)); + } else { + currentx = sylvan_and(currentx, sylvan_nithvar(*varnum*2+1)); + } + *varnum += 1; + } + + BDD currenty = sylvan_true; + for(int i = 0; i 0){ + currenty = sylvan_and(currenty, sylvan_ithvar(*varnum*2+1)); + } else { + currenty = sylvan_and(currenty, sylvan_nithvar(*varnum*2+1)); + } + *varnum += 1; + } + legalpos = sylvan_or(legalpos, + sylvan_and(currentx, currenty)); + } + + return sylvan_and(state, legalpos); +} + /* * We have variables numbered 1... * Per coordinate we need k=bitsx+bitsy variables @@ -79,21 +159,44 @@ BDD encode_position(BDD state, int x, int y, int bx, int by, int *variablenum) */ BDD solve_object(sokoban_screen *scr) { + LACE_ME; int nboxes, mx, my, wx, wy, agentx, agenty; int varnum = 0; int boxx[MAX_BOX]; int boxy[MAX_BOX]; + get_screen_metrics(scr, &nboxes, &mx, &my, &agentx, &agenty, boxx, boxy); EPRINTF("Max x: %d, thus %d bits\n", mx, (wx = ilog2(mx))); EPRINTF("Max y: %d, thus %d bits\n", my, (wy = ilog2(my))); EPRINTF("%d boxes\n", nboxes); - BDD state = sylvan_true; - state = encode_position(state, agentx, agenty, wx, wy, &varnum); + BDD init = encode_position(sylvan_true, agentx, agenty, wx, wy, &varnum); for(int i = 0; i