some
[mc1516pa.git] / modelchecker / main.c
index 5e89211..c439d30 100644 (file)
@@ -1,8 +1,112 @@
 #include <stdio.h>
+#include <stdbool.h>
+#include <ctype.h>
+#include <time.h>
 
 #include <sylvan.h>
+#include "mc.h"
 
-int main(void){
-       printf("Hello world!\n");
+//#include <sokoban.h>
+//#include <object.h>
+//#include <coord.h>
+
+bool DEBUG = false;
+
+void usage(char *prg){
+       fprintf(stderr, 
+               "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, time_file_read;
+       int buffer;
+
+       time_start = clock();
+       while((buffer = fgetc(inputstream)) != EOF){
+               printf("%c", buffer);
+               // Alex:
+               // Screen reading
+               // - Removing outside walls
+               // - Bucket fill
+               // - [tile]
+               // - tile = structure {int, int, enumtile}
+       }
+       time_file_read = clock();
+
+       // Both: Encoding in both schemes
+       
+       // Future: SMC
+       fprintf(stderr, "CPU time taken: %fs\n",
+               ((double) (time_file_read-time_start))/CLOCKS_PER_SEC);
+}
+
+int main(int argc, char **argv){
+       strategy strat = HYBRID;
+       int optchar;
+
+       while((optchar = getopt(argc, argv, "cdhoy")) != -1){
+               switch(optchar){
+               case 'c':
+                       strat = COORD;
+                       if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
+                       break;
+               case 'd':
+                       DEBUG = true;
+                       if(DEBUG) fprintf(stderr, "Debug enabled\n");
+                       break;
+               case 'h':
+                       usage(argv[0]);
+                       return 0;
+               case 'o':
+                       strat = OBJECT;
+                       if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
+                       break;
+               case 'y':
+                       strat = HYBRID;
+                       if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
+                       break;
+               case '?':
+                       if(isprint(optopt)){
+                               fprintf(stderr, "Unknown option `-%c'.\n", optopt);
+                       } else {
+                               fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
+                       }
+                       return 2;
+               default:
+                       break;
+               }
+       }
+
+       if(optind == argc){
+               fprintf(stderr, "You have not specified a file, reading from stdin\n");
+               solve(stdin);
+       }
+
+       for(int filepathindex = optind; filepathindex < argc; filepathindex++){
+               char *currentfilepath = argv[filepathindex];
+               fprintf(stderr, "Processing: %s\n", currentfilepath);
+               if(DEBUG) fprintf(stderr, "Strategy: %d\n", strat);
+               FILE *currentfile = fopen(currentfilepath, "r");
+               if(DEBUG) fprintf(stderr, "Opening file\n");
+               solve(currentfile);
+               if(DEBUG) fprintf(stderr, "Closing file\n");
+               fclose(currentfile);
+       }
        return 0;
 }