X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=7940dc94d65aceab344e5f156e1e11a0e0e8e208;hb=03c6e2f515f6516448ec39aa40a439b9fc20c4c8;hp=76f5e95430bd9e185aa7cdb9b2adc351524b823c;hpb=1f2f3bf57f4c245c9c0a065bff85427e9afcca8b;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 76f5e95..7940dc9 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -1,19 +1,27 @@
 #include <stdio.h>
 #include <stdbool.h>
 #include <ctype.h>
+#include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
-#include "mc.h"
 
-//#include <sokoban.h>
-//#include <object.h>
-//#include <coord.h>
+#include "sokoban.h"
+#include "coord.h"
+#include "object.h"
 
+#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
+#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
+
+typedef enum {OBJECT, COORD, HYBRID} strategy;
+
+//Global variables
 bool DEBUG = false;
+strategy strat = HYBRID;
 
-void usage(char *prg){
-	fprintf(stderr, 
-		"Usage:\n"
+void usage(char *prg)
+{
+	ERRPRINT("Usage:\n"
 		"\t%s [opts] [FILE [FILE [...]]]\n"
 		"\n"
 		"Options:\n"
@@ -32,53 +40,83 @@ void usage(char *prg){
 		"\t         when no file is specified stdin will be used\n", prg);
 }
 
-void solve(FILE *inputstream){
-	int buffer;
-	while((buffer = fgetc(inputstream)) != EOF){
-		printf("%c", buffer);
+void solve(FILE *inputstream)
+{
+	clock_t time_start_read, time_end_read;
+	clock_t time_start_encode, time_end_encode;
+
+	time_start_read = clock();
+	sokoban_screen *screen = parse_screen(inputstream);
+	if (screen == NULL) printf("Something went wrong...\n");
+	//sokoban_print(screen);
+	time_end_read = clock();
+
+	time_start_encode = clock();
+
+	lace_init(0, 1000000);
+	lace_startup(0, NULL, NULL);
+	LACE_ME;
+    sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
+    sylvan_init_bdd(6);
+	switch(strat){
+		case COORD:
+			DPRINT("Encoding coordinate based\n");
+			encode_screen(screen);
+			//test_relprod();
+			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);
 	}
-	// Alex:
-	// Screen reading
-	// - Removing outside walls
-	// - Bucket fill
-	// - [tile]
-	// - tile = structure {int, int, enumtile}
-
-	// Both: Encoding in both schemes
-	
-	// Future: SMC
+	sokoban_free(screen);
+	time_end_encode = clock();
+
+	//SOLVE???
+
+	ERRPRINT("Reading: %fs\n",
+		((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
+	ERRPRINT("Encoding: %fs\n",
+		((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 }
 
-int main(int argc, char **argv){
-	strategy strat = HYBRID;
+int main(int argc, char **argv)
+{
 	int optchar;
 
 	while((optchar = getopt(argc, argv, "cdhoy")) != -1){
 		switch(optchar){
 		case 'c':
 			strat = COORD;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+			DPRINT("Strategy changed to Coordinate based\n");
 			break;
 		case 'd':
 			DEBUG = true;
-			if(DEBUG) fprintf(stderr, "Debug enabled\n");
+			DPRINT("Debug enabled\n");
 			break;
 		case 'h':
 			usage(argv[0]);
 			return 0;
 		case 'o':
 			strat = OBJECT;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
+			DPRINT("Strategy changed to Object based\n");
 			break;
 		case 'y':
 			strat = HYBRID;
-			if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
+			DPRINT("Strategy changed to Hybrid\n");
 			break;
 		case '?':
 			if(isprint(optopt)){
-				fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+				ERRPRINT("Unknown option `-%c'.\n", optopt);
 			} else {
-				fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+				ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 			}
 			return 2;
 		default:
@@ -87,18 +125,17 @@ int main(int argc, char **argv){
 	}
 
 	if(optind == argc){
-		fprintf(stderr, "You have not specified a file, reading from stdin\n");
+		ERRPRINT("You have not specified a file, reading from stdin\n");
 		solve(stdin);
 	}
 
 	for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 		char *currentfilepath = argv[filepathindex];
-		fprintf(stderr, "Processing: %s\n", currentfilepath);
-		if(DEBUG) fprintf(stderr, "Strategy: %d\n", strat);
+		ERRPRINT("Processing: %s\n", currentfilepath);
 		FILE *currentfile = fopen(currentfilepath, "r");
-		if(DEBUG) fprintf(stderr, "Opening file\n");
+		DPRINT("Opening file\n");
 		solve(currentfile);
-		if(DEBUG) fprintf(stderr, "Closing file\n");
+		DPRINT("Closing file\n");
 		fclose(currentfile);
 	}
 	return 0;