From: Mart Lubbers <mart@martlubbers.net>
Date: Tue, 19 Apr 2016 18:57:38 +0000 (+0200)
Subject: add safety switch for parsing, fixed agent error
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=eb450f1c327ba2556ffd0f70be0278090c767a57;p=mc1516pa.git

add safety switch for parsing, fixed agent error
---

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 7cc1070..20ad57b 100644
--- 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
--- 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
--- 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);