X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=06729b14764244ca06d5a5f99b955fb42a4be573;hb=c652648c47a5f1206951314a15e540f75cdbcf73;hp=bdf8a1279a233e248563418f291790971a1bc5f9;hpb=ac8d9afc8de1218083638d0871e98ff15daa9aab;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index bdf8a12..06729b1 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -22,15 +22,13 @@ void usage(char *prg)
 		"\t%s [opts] [FILE]\n"
 		"\n"
 		"Options:\n"
-//		"\t-l LURD  lURD verification strategy\n"
-//		"\t-r	   show all positions that are a valid solution\n"
-		"\n"
+		"\t-l LURD lURD verification strategy\n"
 		"\t-v	   enable verbose output\n"
 		"\t-h	   show this help\n"
 		"\n"
 		"Positional arguments:\n"
 		"\tFILE	 zero or one sokoban screens\n"
-		"\t		 when no file is specified stdin will be used\n", prg);
+		"\t      when no file is specified stdin will be used\n", prg);
 }
 
 BDD subsolve(trans_t *t, BDD new){
@@ -42,7 +40,7 @@ BDD subsolve(trans_t *t, BDD new){
 	return new;
 }
 
-int solve(FILE *inputstream)
+int solve(FILE *inputstream, char *lurd)
 {
 	clock_t time_start_read, time_end_read, time_start_scr, time_end_scr,
 		time_start_goal, time_end_goal, time_start_rel, time_end_rel,
@@ -50,7 +48,7 @@ int solve(FILE *inputstream)
 
 	//Read screen
 	time_start_read = clock();
-	sokoban_screen *screen = parse_screen(inputstream, false);
+	sokoban_screen *screen = parse_screen(inputstream, true);
 	if (screen == NULL) {
 		printf("Something went wrong encoding the screen\n");
 		return 2;
@@ -79,10 +77,31 @@ int solve(FILE *inputstream)
 	rels *rls = encode_rel(screen);
 	time_end_rel = clock();
 
+
 	//Actually solve
 	time_start_solve = clock();
 	BDD old = sylvan_false;
 	BDD new = init->bdd;
+	//Do lurd
+	for(unsigned int i = 0; i<strlen(lurd); i++){
+		switch(lurd[i]){
+		case 'l':
+			new = subsolve(rls->rell, new);
+			break;
+        case 'u':
+			new = subsolve(rls->relu, new);
+			break;
+		case 'r':
+			new = subsolve(rls->relr, new);
+			break;
+		case 'd':
+			new = subsolve(rls->reld, new);
+			break;
+		default:
+			printf("Unknown character in lucd: '%c'\n", lurd[i]);
+			exit(2);
+		}
+	}
 	int iteration = 0;
 	bool found = false;
 	while(new != old){
@@ -119,9 +138,14 @@ int solve(FILE *inputstream)
 int main(int argc, char **argv)
 {
 	int optchar;
+	char *lurd = "";
 
-	while((optchar = getopt(argc, argv, "vh")) != -1){
+	while((optchar = getopt(argc, argv, "vhl:")) != -1){
 		switch(optchar){
+		case 'l':
+			DPRINT("Lurd detected: `%s'\n", optarg);
+			lurd = optarg;
+			break;
 		case 'v':
 			VERBOSE = true;
 			DPRINT("Debug enabled\n");
@@ -143,13 +167,16 @@ int main(int argc, char **argv)
 
 	if(optind == argc){
 		DPRINT("You have not specified a file, reading from stdin\n");
-		return solve(stdin);
+		return solve(stdin, lurd);
 	} else {
 		DPRINT("Processing: %s\n", argv[optind]);
-		DPRINT("Thus skipping the other %d files\n", argc-optind);
 		FILE *currentfile = fopen(argv[optind], "r");
+		if(currentfile == NULL){
+			printf("File could not be opened\n");
+			return 2;
+		}
 		DPRINT("Opening file\n");
-		return solve(currentfile);
+		return solve(currentfile, lurd);
 		DPRINT("Closing file\n");
 		fclose(currentfile);
 	}