From: Mart Lubbers <mart@martlubbers.net>
Date: Wed, 20 Apr 2016 17:08:51 +0000 (+0200)
Subject: Cleaned up main, removed some options
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=ac8d9afc8de1218083638d0871e98ff15daa9aab;p=mc1516pa.git

Cleaned up main, removed some options
---

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 85c6303..bdf8a12 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -10,166 +10,130 @@
 #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;
+#define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
+#define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
 
 //Global variables
-bool DEBUG = false;
-strategy strat = HYBRID;
+bool VERBOSE = false;
 
 void usage(char *prg)
 {
-	ERRPRINT("Usage:\n"
-		"\t%s [opts] [FILE [FILE [...]]]\n"
+	printf("Usage:\n"
+		"\t%s [opts] [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"
+//		"\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"
+		"\t-v	   enable verbose 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);
+		"\tFILE	 zero or one sokoban screens\n"
+		"\t		 when no file is specified stdin will be used\n", prg);
+}
+
+BDD subsolve(trans_t *t, BDD new){
+	LACE_ME;
+	while (t != NULL){
+		new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+		t = t->next_rel;
+	}
+	return new;
 }
 
-void solve(FILE *inputstream)
+int solve(FILE *inputstream)
 {
-	clock_t time_start_read, time_end_read;
-	clock_t time_start_encode, time_end_encode;
+	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,
+		time_start_solve, time_end_solve;
 
+	//Read screen
 	time_start_read = clock();
 	sokoban_screen *screen = parse_screen(inputstream, false);
-	if (screen == NULL) printf("Something went wrong...\n");
-	//sokoban_print(screen);
+	if (screen == NULL) {
+		printf("Something went wrong encoding the screen\n");
+		return 2;
+	}
 	time_end_read = clock();
 
-	time_start_encode = clock();
-
+	//Lace and sylvan blork
 	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);
+	sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
+	sylvan_init_bdd(6);
 
+	//Encode screen
+	time_start_scr = clock();
 	state *init = encode_screen(screen);
-    state *goal = encode_goal(screen);
+	time_end_scr = clock();
+
+	//Encode goal
+	time_start_goal = clock();
+	state *goal = encode_goal(screen);
+	time_end_goal = clock();
+
+	//Encode transitions
+	time_start_rel = clock();
 	rels *rls = encode_rel(screen);
-    /*
-    printf("Doing left\n");
-    test_trans(init, rls->rell);
-    printf("Doing up\n");
-    test_trans(init, rls->relu);
-    printf("Doing right\n");
-    test_trans(init, rls->relr);
-    printf("Doing down\n");
-    test_trans(init, rls->reld);
-    */
+	time_end_rel = clock();
 
+	//Actually solve
+	time_start_solve = clock();
 	BDD old = sylvan_false;
 	BDD new = init->bdd;
 	int iteration = 0;
-    if (goal != NULL){
-        while(new != old){
-            old = new;
-            ERRPRINT("Iteration %d\n", iteration++);
-            trans_t *t = rls->rell;
-
-            //for testing
-            /*
-              BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9);
-              BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0});
-              BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0}));
-              BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1}));
-              if (new == teststate2) printf("Wrong!\n");
-            */
-            while (t != NULL){
-                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
-                t = t->next_rel;
-                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
-            }
-
-            t = rls->relu;
-            while (t != NULL){
-                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
-                t = t->next_rel;
-                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
-            }
-
-
-            t = rls->relr;
-            while (t != NULL){
-                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
-                t = t->next_rel;
-                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
-            }
-
-
-            t = rls->reld;
-            while (t != NULL){
-                new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
-                t = t->next_rel;
-                //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset));
-            }
-            double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset);
-            if (check > 0){
-                printf("Solution is found after %d iteration(s)!\n", iteration);
-                break;
-            }
-        }
-    }
-    else printf("No solution found!\n");
-	//ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
-//	sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);
-//	sylvan_printdot_nc(old);
-	time_end_encode = clock();
-
-	//SOLVE???
+	bool found = false;
+	while(new != old){
+		DPRINT("Iteration %d\n", iteration++);
+		old = new;
+		if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){
+			found = true;
+			break;
+		}
 
+		//Left, Up, Right, Down moves
+		new = subsolve(rls->rell, new);
+		new = subsolve(rls->relu, new);
+		new = subsolve(rls->relr, new);
+		new = subsolve(rls->reld, new);
+	}
+	time_end_solve = clock();
+
+	//Free and print stats
 	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);
+	REPORT("Reading: %fs\n", time_end_read, time_start_read);
+	REPORT("Screen encoding: %fs\n", time_end_scr, time_start_scr);
+	REPORT("Goal encoding: %fs\n", time_end_goal, time_start_goal);
+	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;
 }
 
 int main(int argc, char **argv)
 {
 	int optchar;
 
-	while((optchar = getopt(argc, argv, "cdhoy")) != -1){
+	while((optchar = getopt(argc, argv, "vh")) != -1){
 		switch(optchar){
-		case 'c':
-			strat = COORD;
-			DPRINT("Strategy changed to Coordinate based\n");
-			break;
-		case 'd':
-			DEBUG = true;
+		case 'v':
+			VERBOSE = 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);
+				DPRINT("Skipping unknown option `-%c'.\n", optopt);
 			} else {
-				ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
+				DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
 			}
 			return 2;
 		default:
@@ -178,18 +142,15 @@ int main(int argc, char **argv)
 	}
 
 	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("You have not specified a file, reading from stdin\n");
+		return solve(stdin);
+	} else {
+		DPRINT("Processing: %s\n", argv[optind]);
+		DPRINT("Thus skipping the other %d files\n", argc-optind);
+		FILE *currentfile = fopen(argv[optind], "r");
 		DPRINT("Opening file\n");
-		solve(currentfile);
+		return solve(currentfile);
 		DPRINT("Closing file\n");
 		fclose(currentfile);
 	}
-	return 0;
 }
diff --git a/modelchecker/test.sh b/modelchecker/test.sh
index 2aa9aea..84d30e7 100755
--- a/modelchecker/test.sh
+++ b/modelchecker/test.sh
@@ -10,6 +10,7 @@ PASSED=0
 for testscreen in tests/[^g]*; do
 	NUM="$(basename "$(echo $testscreen | cut -d'.' -f1)")"
 	OUT="$(./main "$testscreen" 2>&1| grep -Po "(?<=Satcount: )\d+(?=\.)")"
+	./main "$testscreen" 2>&1
 	if [ "$NUM" -ne "$OUT" ]; then
 		echo "$testscreen failed, expected: $NUM, got: $OUT."
 		echo "'$(cat "$testscreen")'"