X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=79bb46d5b561fd952ecb1e58783a9a657611e534;hb=6b4ffb3fcb69b5380bc75440a4bc73b5dc963921;hp=1f518eba9cdbb6c1958a09aa4d43e4079687103a;hpb=6d27f2cbfee60299b29e28167962574d09851d34;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 1f518eb..79bb46d 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -22,7 +22,7 @@ void usage(char *prg)
 		"\t%s [opts] [FILE]\n"
 		"\n"
 		"Options:\n"
-		"\t-l LURD lURD verification strategy\n"
+		"\t-l LURD initial LURD\n"
 		"\t-v	   enable verbose output\n"
 		"\t-h	   show this help\n"
 		"\n"
@@ -77,7 +77,6 @@ int solve(FILE *inputstream, char *lurd)
 	rels *rls = encode_rel(screen);
 	time_end_rel = clock();
 
-
 	//Actually solve
 	time_start_solve = clock();
 	BDD old = sylvan_false;
@@ -98,13 +97,15 @@ int solve(FILE *inputstream, char *lurd)
 			new = subsolve(rls->reld, new);
 			break;
 		default:
-			printf("Unknown character in lucd: '%c'\n", *lurd);
+			printf("Unknown character in lurd: '%c'\n", *lurd);
 			exit(2);
 		}
 		lurd++;
 	}
 	int iteration = 0;
+
 	bool found = false;
+
 	while(new != old){
 		DPRINT("Iteration %d\n", iteration++);
 		old = new;
@@ -119,6 +120,7 @@ int solve(FILE *inputstream, char *lurd)
 		new = subsolve(rls->relr, new);
 		new = subsolve(rls->reld, new);
 	}
+
 	time_end_solve = clock();
 
 	//Free and print stats
@@ -129,10 +131,12 @@ int solve(FILE *inputstream, char *lurd)
 	REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
 	REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
 
+
 	if(!found){
 		printf("no solution\n");
 		return 1;
 	}
+
 	return 0;
 }