modelchecker/main.c

   1 #include <stdio.h>
   2 #include <stdbool.h>
   3 #include <ctype.h>
   4 #include <time.h>
   5 #include <unistd.h>
   6
   7 #include <sylvan.h>
   8
   9 #include "sokoban.h"
  10 #include "coord.h"
  11 #include "object.h"
  12
  13 #define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as);
  14 #define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as);
  15
  16 typedef enum {OBJECT, COORD, HYBRID} strategy;
  17
  18 //Global variables
  19 bool DEBUG = false;
  20 strategy strat = HYBRID;
  21
  22 void usage(char *prg)
  23 {
  24         ERRPRINT("Usage:\n"
  25                 "\t%s [opts] [FILE [FILE [...]]]\n"
  26                 "\n"
  27                 "Options:\n"
  28                 "\tAll strategies are mutually exclusive\n"
  29                 "\t-c       coordinate based strategy\n"
  30                 "\t-o       object based strategy\n"
  31                 "\t-y       hybrid strategy\n"
  32 //              "\t-l LURD  lURD verification strategy\n"
  33 //              "\t-r       show all positions that are a valid solution\n"
  34                 "\n"
  35                 "\t-d       enable verbose debug output\n"
  36                 "\t-h       show this help\n"
  37                 "\n"
  38                 "Positional arguments:\n"
  39                 "\tFILE     zero or more sokoban screens\n"
  40                 "\t         when no file is specified stdin will be used\n", prg);
  41 }
  42
  43 void solve(FILE *inputstream)
  44 {
  45         clock_t time_start_read, time_end_read;
  46         clock_t time_start_encode, time_end_encode;
  47
  48         time_start_read = clock();
  49         sokoban_screen *screen = parse_screen(inputstream);
  50         if (screen == NULL) printf("Something went wrong...\n");
  51         //sokoban_print(screen);
  52         time_end_read = clock();
  53
  54         time_start_encode = clock();
  55
  56         lace_init(0, 1000000);
  57         lace_startup(0, NULL, NULL);
  58         LACE_ME;
  59     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
  60     sylvan_init_bdd(6);
  61
  62         state *init = encode_screen(screen);
  63         rels *rls = encode_rel(screen);
  64
  65         BDD old = sylvan_false;
  66         BDD new = init->bdd;
  67         int iteration = 0;
  68         while(new != old){
  69                 ERRPRINT("Iteration %d\n", iteration++);
  70                 old = new;
  71         //WRONG! each trans relation (LEFT,UP,RIGHT,DOWN) contains a linked list of trans relations (not just
  72         //only one), so to compute a transition for a single direction, we need to iterate through a relevant linked list
  73         //taking disjunction of results (for a single direction there will be falses and only one screen change among the
  74         //results)
  75                 new = sylvan_or(new, sylvan_relnext(new, rls->rell->bdd, rls->rell->varset.varset));
  76                 new = sylvan_or(new, sylvan_relnext(new, rls->relu->bdd, rls->relu->varset.varset));
  77                 new = sylvan_or(new, sylvan_relnext(new, rls->relr->bdd, rls->relr->varset.varset));
  78                 new = sylvan_or(new, sylvan_relnext(new, rls->reld->bdd, rls->reld->varset.varset));
  79         }
  80                 //sylvan_printdot_nc(old);
  81         //switch(strat){
  82         //      case COORD:
  83         //              DPRINT("Encoding coordinate based\n");
  84         //              break;
  85         //      case OBJECT:
  86         //              DPRINT("Encoding object based\n");
  87         //              solve_object(screen);
  88         //              break;
  89         //      case HYBRID:
  90         //              DPRINT("Encoding hybrid based\n");
  91         //              DPRINT("Not implemented yet...\n");
  92         //              break;
  93         //      default:
  94         //              ERRPRINT("Huh?");
  95         //              exit(2);
  96         //}
  97         time_end_encode = clock();
  98
  99         //SOLVE???
 100
 101         sokoban_free(screen);
 102         ERRPRINT("Reading: %fs\n",
 103                 ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
 104         ERRPRINT("Encoding: %fs\n",
 105                 ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC);
 106 }
 107
 108 int main(int argc, char **argv)
 109 {
 110         int optchar;
 111
 112         while((optchar = getopt(argc, argv, "cdhoy")) != -1){
 113                 switch(optchar){
 114                 case 'c':
 115                         strat = COORD;
 116                         DPRINT("Strategy changed to Coordinate based\n");
 117                         break;
 118                 case 'd':
 119                         DEBUG = true;
 120                         DPRINT("Debug enabled\n");
 121                         break;
 122                 case 'h':
 123                         usage(argv[0]);
 124                         return 0;
 125                 case 'o':
 126                         strat = OBJECT;
 127                         DPRINT("Strategy changed to Object based\n");
 128                         break;
 129                 case 'y':
 130                         strat = HYBRID;
 131                         DPRINT("Strategy changed to Hybrid\n");
 132                         break;
 133                 case '?':
 134                         if(isprint(optopt)){
 135                                 ERRPRINT("Unknown option `-%c'.\n", optopt);
 136                         } else {
 137                                 ERRPRINT("Unknown option char `-\\x%x'.\n", optopt);
 138                         }
 139                         return 2;
 140                 default:
 141                         break;
 142                 }
 143         }
 144
 145         if(optind == argc){
 146                 ERRPRINT("You have not specified a file, reading from stdin\n");
 147                 solve(stdin);
 148         }
 149
 150         for(int filepathindex = optind; filepathindex < argc; filepathindex++){
 151                 char *currentfilepath = argv[filepathindex];
 152                 ERRPRINT("Processing: %s\n", currentfilepath);
 153                 FILE *currentfile = fopen(currentfilepath, "r");
 154                 DPRINT("Opening file\n");
 155                 solve(currentfile);
 156                 DPRINT("Closing file\n");
 157                 fclose(currentfile);
 158         }
 159         return 0;
 160 }