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

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 00f8b32..79bb46d 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -1,36 +1,184 @@
 #include <stdio.h>
+#include <stdbool.h>
+#include <ctype.h>
+#include <time.h>
+#include <unistd.h>
 
 #include <sylvan.h>
 
-//#include <sokoban.h>
-//#include <object.h>
-//#include <coord.h>
-//#include <mc.h>
-
-int main(void){
-	// Mart:
-	// Argument parsing
-	// ./main [opts] [FILEPATH [FILEPATH ...]]
-	// -o         Objectbased
-	// -c         Coordinatebased
-	// -y         hYbrid
-	// -h         Help
-	//
-	// FUTURE:
-	// -r         Also compute the set of all reachable solution states
-	// -l LURD    Check if LURD is a valid path
-	//
-	// FILEPATH   Optional input file(s)
-	
-	// Alex:
-	// Screen reading
-	// - Removing outside walls
-	// - Bucket fill
-	// - [tile]
-	// - tile = structure {int, int, enumtile}
-	
-	// Both: Encoding in both schemes
-	
-	// Future: SMC
+#include "sokoban.h"
+#include "coord.h"
+#include "object.h"
+
+#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 VERBOSE = false;
+
+void usage(char *prg)
+{
+	printf("Usage:\n"
+		"\t%s [opts] [FILE]\n"
+		"\n"
+		"Options:\n"
+		"\t-l LURD initial LURD\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);
+}
+
+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;
+}
+
+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,
+		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 encoding the screen\n");
+		return 2;
+	}
+	time_end_read = 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);
+
+	//Encode screen
+	time_start_scr = clock();
+	state *init = encode_screen(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);
+	time_end_rel = clock();
+
+	//Actually solve
+	time_start_solve = clock();
+	BDD old = sylvan_false;
+	BDD new = init->bdd;
+	//Do lurd
+	while(*lurd != '\0'){
+		switch(*lurd){
+		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 lurd: '%c'\n", *lurd);
+			exit(2);
+		}
+		lurd++;
+	}
+	int iteration = 0;
+
+	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);
+	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;
+	char *lurd = "";
+
+	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");
+			break;
+		case 'h':
+			usage(argv[0]);
+			return 0;
+		case '?':
+			if(isprint(optopt)){
+				DPRINT("Skipping unknown option `-%c'.\n", optopt);
+			} else {
+				DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt);
+			}
+			return 2;
+		default:
+			break;
+		}
+	}
+
+	if(optind == argc){
+		DPRINT("You have not specified a file, reading from stdin\n");
+		return solve(stdin, lurd);
+	} else {
+		DPRINT("Processing: %s\n", argv[optind]);
+		FILE *currentfile = fopen(argv[optind], "r");
+		DPRINT("Opening file\n");
+		return solve(currentfile, lurd);
+		DPRINT("Closing file\n");
+		fclose(currentfile);
+	}
+}