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