started with transitions, I think agent transitions work...

diff --git a/modelchecker/object.c b/modelchecker/object.c
index 769163f..362802d 100644 (file)
--- 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<bx; i++){
                if((x & (1<<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; i<bx; i++){
+                       state = sylvan_and(state,
+                               sylvan_xor(sylvan_ithvar(*varnum*2-1),
+                                       sylvan_xor(sylvan_ithvar(*varnum*2),
+                                               sylvan_ithvar(*varnum*2+1))));
+                       *varnum += 1;
+               }
+       } else if(dir == LEFT){
+               //TODO
+               *varnum += bx;
+       }else {
+               *varnum += bx;
+       }
+       
+       //DOWN
+       if(dir == DOWN){
+               state = sylvan_and(state,
+                       sylvan_xor(sylvan_ithvar(*varnum*2), sylvan_ithvar(*varnum*2+1)));
+               *varnum += 1;
+               for(int i = 1; i<by; i++){
+                       state = sylvan_and(state,
+                               sylvan_xor(sylvan_ithvar(*varnum*2-1),
+                                       sylvan_xor(sylvan_ithvar(*varnum*2),
+                                               sylvan_ithvar(*varnum*2+1))));
+                       *varnum += 1;
+               }
+       } else if(dir == UP){
+               //TODO
+               *varnum += by;
+       } else {
+               *varnum += by;
+       }
+
+       //Check wether it is a valid position
+       BDD legalpos = sylvan_false;
+       for(sokoban_screen *r=scr; r != NULL; r = r->hh.next){
+               int x = r->coord.x;
+               int y = r->coord.y;
+               *varnum = oldvarnum;
+
+               BDD currentx = sylvan_true;
+               for(int i = 0; i<bx; i++){
+                       if((x & (1<<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<by; i++){
+                       if((y & (1<<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<nboxes; i++){
-               state = encode_position(state, boxx[i], boxy[i], wx, wy, &varnum);
+               init = encode_position(init, boxx[i], boxy[i], wx, wy, &varnum);
        }
-       
-       return state;
+
+       varnum = 0;
+       BDD trans_r = encode_transition(scr, sylvan_true, mx, my, &varnum, RIGHT);
+       varnum = 0;
+       BDD trans_l = encode_transition(scr, sylvan_true, mx, my, &varnum, LEFT);
+       varnum = 0;
+       BDD trans_d = encode_transition(scr, sylvan_true, mx, my, &varnum, DOWN);
+       varnum = 0;
+       BDD trans_u = encode_transition(scr, sylvan_true, mx, my, &varnum, UP);
+
+       BDD old = sylvan_false;
+       BDD new = init;
+       int iteration = 0;
+       while(new != old){
+               EPRINTF("Iteration %d\n", iteration++);
+               old = new;
+               new = sylvan_or(new, sylvan_relnext(new, trans_d, false));
+               new = sylvan_or(new, sylvan_relnext(new, trans_r, false));
+               new = sylvan_or(new, sylvan_relnext(new, trans_u, false));
+               new = sylvan_or(new, sylvan_relnext(new, trans_l, false));
+               sylvan_printdot_nc(old);
+       }
+
+       return init;
 }

diff --git a/modelchecker/toy.screen b/modelchecker/toy.screen
new file mode 100644 (file)
index 0000000..8d4f16e
--- /dev/null
+++ b/modelchecker/toy.screen
@@ -0,0 +1 @@
+@$.