tiny update

[mc1516pa.git] / modelchecker / sokoban.c

diff --git a/modelchecker/sokoban.c b/modelchecker/sokoban.c
index 9d42daf..4f3c8a1 100644 (file)
--- a/modelchecker/sokoban.c
+++ b/modelchecker/sokoban.c
@@ -1,38 +1,114 @@
 #include <stdio.h>
 #include <stdlib.h>
-
 #include "sokoban.h"
 
-//Still need to remove outside walls and unreachable places.
-struct sokoban_screen *parse_screen(FILE *stream){
-       int buffer, x, y;
+sokoban_screen *add_coord(int x, int y, sokoban_tile tile, sokoban_screen *screen)
+{
+       sokoban_screen *r = NULL;
+
+       r = (sokoban_screen *)malloc(sizeof(sokoban_screen));
+       memset(r, 0, sizeof(sokoban_screen));
+       r->coord.x = x;
+       r->coord.y = y;
+       r->tile = tile;
+       HASH_ADD(hh, screen, coord, sizeof(record_key), r);
+       return screen;
+}
+
+sokoban_screen *get_coord(int x, int y, sokoban_screen *screen)
+{
+       sokoban_screen k, *r = NULL;
+       memset(&k, 0, sizeof(sokoban_screen));
+       k.coord.x = x;
+       k.coord.y = y;
+       HASH_FIND(hh, screen, &k.coord, sizeof(record_key), r);
+       return r;
+}
+
+sokoban_screen *delete_coord(int x, int y, sokoban_screen *screen)
+{
+       sokoban_screen *r = NULL;
+       r = get_coord(x, y, screen);
+       if (r) HASH_DEL(screen, r);
+       return screen;
+}
+
+void sokoban_print(sokoban_screen *screen)
+{
+       sokoban_screen *r;
+       for(r=screen; r != NULL; r = (sokoban_screen *)(r->hh.next)){
+               switch(r->tile){
+               case FREE: printf("x = %d y = %d FREE\n", r->coord.x, r->coord.y); break;
+               case WALL: printf("x = %d y = %d WALL\n", r->coord.x, r->coord.y); break;
+               case BOX: printf("x = %d y = %d BOX\n", r->coord.x, r->coord.y); break;
+               case TARGET: printf("x = %d y = %d TARGET\n", r->coord.x, r->coord.y); break;
+               case AGENT: printf("x = %d y = %d AGENT\n", r->coord.x, r->coord.y); break;
+               case TARGAGENT: printf("x = %d y = %d TARGAGENT\n", r->coord.x, r->coord.y); break;
+               case TARGBOX: printf("x = %d y = %d TARGBOX\n", r->coord.x, r->coord.y); break;
+               }
+       }
+}
+
+sokoban_screen *sokoban_shrink(int x, int y, sokoban_screen *screen, sokoban_screen *newscreen)
+{
+       sokoban_screen *c, *nc = NULL;
+       c = get_coord(x, y, screen);
+       if (c) {
+               nc = get_coord(c->coord.x, c->coord.y, newscreen);
+               if (c->tile != WALL && nc == NULL) {
+                       newscreen = add_coord(x, y, c->tile, newscreen);
+                       newscreen = sokoban_shrink(x-1, y, screen, newscreen);
+                       newscreen = sokoban_shrink(x+1, y, screen, newscreen);
+                       newscreen = sokoban_shrink(x, y-1, screen, newscreen);
+                       newscreen = sokoban_shrink(x, y+1, screen, newscreen);
+               }
+       }
+       return newscreen;
+}
+
+void sokoban_free(sokoban_screen *screen)
+{
+       sokoban_screen *r, *tmp = NULL;
+       HASH_ITER(hh, screen, r, tmp) {
+               HASH_DEL(screen, r);
+               free(r);
+       }
+}
+
+sokoban_screen *parse_screen(FILE *stream)
+{
+       int buffer, x, y, agent_x, agent_y;
        x = 0;
        y = 0;
-       struct sokoban_screen *head, *current;
-       head = NULL;
+       agent_x = 0;
+       agent_y = 0;
+       sokoban_screen *screen = NULL;
        while((buffer = fgetc(stream)) != EOF){
                if (buffer == '\n'){
                        x = 0;
                        y++;
                }
                else {
-                       current = (struct sokoban_screen *)malloc(sizeof(struct sokoban_screen));
-                       current->next = head;
                        switch(buffer) {
-                               case ' ' : current->tile = FREE; break;
-                               case '@' : current->tile = AGENT; break;
-                               case '.' : current->tile = TARGET; break;
-                               case '#' : current->tile = WALL; break;
-                               case '$' : current->tile = BOX; break;
-                               case '*' : current->tile = TARGBOX; break;
-                               case '+' : current->tile = TARGAGENT; break;
-                               default: return NULL;
+                       case ' ': screen = add_coord(x, y, FREE, screen); break;
+                       case '@':
+                               screen = add_coord(x, y, AGENT, screen);
+                               agent_x = x;
+                               agent_y = y;
+                               break;
+                       case '.': screen = add_coord(x, y, TARGET, screen); break;
+                       case '#': screen = add_coord(x, y, WALL, screen); break;
+                       case '$': screen = add_coord(x, y, BOX, screen); break;
+                       case '*': screen = add_coord(x, y, TARGBOX, screen); break;
+                       case '+': screen = add_coord(x, y, TARGAGENT, screen); break;
+                       default: return NULL;
                        }
-                       current->x = x;
-                       current->y = y;
                        x++;
-                       head = current;
                }
        }
-       return head;
+       sokoban_screen *newscreen = NULL;
+       newscreen = sokoban_shrink(agent_x, agent_y, screen, newscreen);
+       //sokoban_print(screen); //unshrinked screen
+       sokoban_free(screen);
+       return newscreen;
 }