add safety switch for parsing, fixed agent error

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 7cc1070..20ad57b 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -46,7 +46,7 @@ void solve(FILE *inputstream)
        clock_t time_start_encode, time_end_encode;
 
        time_start_read = clock();
-       sokoban_screen *screen = parse_screen(inputstream);
+       sokoban_screen *screen = parse_screen(inputstream, false);
        if (screen == NULL) printf("Something went wrong...\n");
        //sokoban_print(screen);
        time_end_read = clock();
@@ -91,23 +91,8 @@ void solve(FILE *inputstream)
         }
        }
        ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
-               //sylvan_printdot_nc(old);
-       //switch(strat){
-       //      case COORD:
-       //              DPRINT("Encoding coordinate based\n");
-       //              break;
-       //      case OBJECT:
-       //              DPRINT("Encoding object based\n");
-       //              solve_object(screen);
-       //              break;
-       //      case HYBRID:
-       //              DPRINT("Encoding hybrid based\n");
-       //              DPRINT("Not implemented yet...\n");
-       //              break;
-       //      default:
-       //              ERRPRINT("Huh?");
-       //              exit(2);
-       //}
+//     sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
+//     sylvan_printdot_nc(old);
        time_end_encode = clock();
 
        //SOLVE???

diff --git a/modelchecker/sokoban.c b/modelchecker/sokoban.c
index 4f3c8a1..fd268c0 100644 (file)
--- a/modelchecker/sokoban.c
+++ b/modelchecker/sokoban.c
@@ -75,13 +75,16 @@ void sokoban_free(sokoban_screen *screen)
        }
 }
 
-sokoban_screen *parse_screen(FILE *stream)
+sokoban_screen *parse_screen(FILE *stream, bool safe)
 {
-       int buffer, x, y, agent_x, agent_y;
+       int buffer, x, y, agent_x, agent_y, boxes, targets, agents;
        x = 0;
        y = 0;
        agent_x = 0;
        agent_y = 0;
+       boxes = 0;
+       targets = 0;
+       agents = 0;
        sokoban_screen *screen = NULL;
        while((buffer = fgetc(stream)) != EOF){
                if (buffer == '\n'){
@@ -95,20 +98,48 @@ sokoban_screen *parse_screen(FILE *stream)
                                screen = add_coord(x, y, AGENT, screen);
                                agent_x = x;
                                agent_y = y;
+                               agents++;
+                               break;
+                       case '.':
+                               screen = add_coord(x, y, TARGET, screen);
+                               targets++;
                                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;
+                       case '$':
+                               screen = add_coord(x, y, BOX, screen);
+                               boxes++;
+                               break;
+                       case '*': 
+                               screen = add_coord(x, y, TARGBOX, screen);
+                               boxes++;
+                               targets++;
+                               break;
+                       case '+': 
+                               screen = add_coord(x, y, TARGAGENT, screen);
+                               agent_x = x;
+                               agent_y = y;
+                               agents++;
+                               targets++;
+                               break;
                        default: return NULL;
                        }
                        x++;
                }
        }
+       if(safe == true && boxes != targets){
+               fprintf(stderr, 
+                       "Invalid screen. Boxes: %d, Targets: %d\n", boxes, targets);
+               exit(1);
+       }
+       if(safe == true && agents != 1){
+               fprintf(stderr, 
+                       "Invalid screen. There has to be exactly one agent. Found: %d\n", 
+                       agents);
+               exit(1);
+       }
+
        sokoban_screen *newscreen = NULL;
        newscreen = sokoban_shrink(agent_x, agent_y, screen, newscreen);
-       //sokoban_print(screen); //unshrinked screen
        sokoban_free(screen);
        return newscreen;
 }

diff --git a/modelchecker/sokoban.h b/modelchecker/sokoban.h
index 6b8823d..7043a74 100644 (file)
--- a/modelchecker/sokoban.h
+++ b/modelchecker/sokoban.h
@@ -1,6 +1,7 @@
 #ifndef SOKOBAN_H
 #define SOKOBAN_H
 #include <stdio.h>
+#include <stdbool.h>
 
 #include "uthash.h"
 
@@ -17,7 +18,7 @@ typedef struct {
        UT_hash_handle hh;
 } sokoban_screen;
 
-sokoban_screen *parse_screen(FILE *stream);
+sokoban_screen *parse_screen(FILE *stream, bool safe);
 
 sokoban_screen *get_coord(int x, int y, sokoban_screen *screen);