X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=95b8458e45e57cf7afec4d6ce0d7f3655d445f93;hb=c4d4a1d7cbe6a1c6dd2a2b3ba80b3f3029ee8186;hp=5e892113d2f8d5815b016859baac0ef67e96bb4e;hpb=7b58c6ef6de2382ed29f3e618d94b07a4b4f5791;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 5e89211..95b8458 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -1,8 +1,156 @@
 #include <stdio.h>
+#include <stdbool.h>
+#include <ctype.h>
+#include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-int main(void){
-	printf("Hello world!\n");
+#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)
+{
+	ERRPRINT("Usage:\n"
+		"\t%s [opts] [FILE [FILE [...]]]\n"
+		"\n"
+		"Options:\n"
+		"\tAll strategies are mutually exclusive\n"
+		"\t-c       coordinate based strategy\n"
+		"\t-o       object based strategy\n"
+		"\t-y       hybrid strategy\n"
+//		"\t-l LURD  lURD verification strategy\n"
+//		"\t-r       show all positions that are a valid solution\n"
+		"\n"
+		"\t-d       enable verbose debug output\n"
+		"\t-h       show this help\n"
+		"\n"
+		"Positional arguments:\n"
+		"\tFILE     zero or more sokoban screens\n"
+		"\t         when no file is specified stdin will be used\n", prg);
+}
+
+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);
+
+	state *init = encode_screen(screen);
+	rels *rls = encode_rel(screen);
+
+	BDD old = sylvan_false;
+	BDD new = init->bdd;
+	int iteration = 0;
+	while(new != old){
+		ERRPRINT("Iteration %d\n", iteration++);
+		old = new;
+		new = sylvan_or(new, sylvan_relnext(new, rls->rell->bdd, rls->rell->varset.varset));
+		new = sylvan_or(new, sylvan_relnext(new, rls->relu->bdd, rls->relu->varset.varset));
+		new = sylvan_or(new, sylvan_relnext(new, rls->relr->bdd, rls->relr->varset.varset));
+		new = sylvan_or(new, sylvan_relnext(new, rls->reld->bdd, rls->reld->varset.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);
+	//}
+	time_end_encode = clock();
+
+	//SOLVE???
+
+	sokoban_free(screen);
+	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)
+{
+	int optchar;
+
+	while((optchar = getopt(argc, argv, "cdhoy")) != -1){
+		switch(optchar){
+		case 'c':
+			strat = COORD;
+			DPRINT("Strategy changed to Coordinate based\n");
+			break;
+		case 'd':
+			DEBUG = true;
+			DPRINT("Debug enabled\n");
+			break;
+		case 'h':
+			usage(argv[0]);
+			return 0;
+		case 'o':
+			strat = OBJECT;
+			DPRINT("Strategy changed to Object based\n");
+			break;
+		case 'y':
+			strat = HYBRID;
+			DPRINT("Strategy changed to Hybrid\n");
+			break;
+		case '?':
+			if(isprint(optopt)){
+				ERRPRINT("Unknown option `-%c'.\n", optopt);
+			} else {
+				ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
+			}
+			return 2;
+		default:
+			break;
+		}
+	}
+
+	if(optind == argc){
+		ERRPRINT("You have not specified a file, reading from stdin\n");
+		solve(stdin);
+	}
+
+	for(int filepathindex = optind; filepathindex < argc; filepathindex++){
+		char *currentfilepath = argv[filepathindex];
+		ERRPRINT("Processing: %s\n", currentfilepath);
+		FILE *currentfile = fopen(currentfilepath, "r");
+		DPRINT("Opening file\n");
+		solve(currentfile);
+		DPRINT("Closing file\n");
+		fclose(currentfile);
+	}
 	return 0;
 }