modelchecker/main.c

   1 #include <stdio.h>
   2 #include <stdbool.h>
   3 #include <ctype.h>
   4 #include <time.h>
   5
   6 #include <sylvan.h>
   7
   8 #include "mc.h"
   9 #include "sokoban.h"
  10 #include "uthash.h"
  11
  12 //Global variables
  13 bool DEBUG = false;
  14 strategy strat = HYBRID;
  15
  16 void usage(char *prg)
  17 {
  18         fprintf(stderr,
  19                 "Usage:\n"
  20                 "\t%s [opts] [FILE [FILE [...]]]\n"
  21                 "\n"
  22                 "Options:\n"
  23                 "\tAll strategies are mutually exclusive\n"
  24                 "\t-c       coordinate based strategy\n"
  25                 "\t-o       object based strategy\n"
  26                 "\t-y       hybrid strategy\n"
  27 //              "\t-l LURD  lURD verification strategy\n"
  28 //              "\t-r       show all positions that are a valid solution\n"
  29                 "\n"
  30                 "\t-d       enable verbose debug output\n"
  31                 "\t-h       show this help\n"
  32                 "\n"
  33                 "Positional arguments:\n"
  34                 "\tFILE     zero or more sokoban screens\n"
  35                 "\t         when no file is specified stdin will be used\n", prg);
  36 }
  37
  38 void solve(FILE *inputstream)
  39 {
  40         clock_t time_start_read, time_end_read;
  41         clock_t time_start_encode, time_end_encode;
  42
  43         time_start_read = clock();
  44         sokoban_screen *screen = parse_screen(inputstream);
  45         if (screen == NULL) printf("Something went wrong...\n");
  46         sokoban_print(screen);
  47         //parse_screen(inputstream);
  48         time_end_read = clock();
  49
  50         time_start_encode = clock();
  51         switch(strat){
  52         case COORD:
  53                 if(DEBUG) fprintf(stderr, "Encoding coordinate based\n");
  54                 break;
  55         case OBJECT:
  56                 if(DEBUG) fprintf(stderr, "Encoding object based\n");
  57                 break;
  58         case HYBRID:
  59                 if(DEBUG) fprintf(stderr, "Encoding hybrid based\n");
  60                 break;
  61         default:
  62                 fprintf(stderr, "Huh?");
  63                 exit(2);
  64         }
  65         time_end_encode = clock();
  66
  67         // Future: SMC
  68         fprintf(stderr, "Reading: %fs\n",
  69                 ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
  70         fprintf(stderr, "Encoding: %fs\n",
  71                 ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
  72 }
  73
  74 int main(int argc, char **argv)
  75 {
  76         int optchar;
  77
  78         while((optchar = getopt(argc, argv, "cdhoy")) != -1){
  79                 switch(optchar){
  80                 case 'c':
  81                         strat = COORD;
  82                         if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n");
  83                         break;
  84                 case 'd':
  85                         DEBUG = true;
  86                         if(DEBUG) fprintf(stderr, "Debug enabled\n");
  87                         break;
  88                 case 'h':
  89                         usage(argv[0]);
  90                         return 0;
  91                 case 'o':
  92                         strat = OBJECT;
  93                         if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n");
  94                         break;
  95                 case 'y':
  96                         strat = HYBRID;
  97                         if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n");
  98                         break;
  99                 case '?':
 100                         if(isprint(optopt)){
 101                                 fprintf(stderr, "Unknown option `-%c'.\n", optopt);
 102                         } else {
 103                                 fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt);
 104                         }
 105                         return 2;
 106                 default:
 107                         break;
 108                 }
 109         }
 110
 111         if(optind == argc){
 112                 fprintf(stderr, "You have not specified a file, reading from stdin\n");
 113                 solve(stdin);
 114         }
 115
 116         for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 117                 char *currentfilepath = argv[filepathindex];
 118                 fprintf(stderr, "Processing: %s\n", currentfilepath);
 119                 FILE *currentfile = fopen(currentfilepath, "r");
 120                 if(DEBUG) fprintf(stderr, "Opening file\n");
 121                 solve(currentfile);
 122                 if(DEBUG) fprintf(stderr, "Closing file\n");
 123                 fclose(currentfile);
 124         }
 125         return 0;
 126 }