X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=06729b14764244ca06d5a5f99b955fb42a4be573;hb=c652648c47a5f1206951314a15e540f75cdbcf73;hp=16eecbedacce27f84dda041d8f4ba7b0869a8747;hpb=81eb34c9ea8b55240eb973b1e9f3911fb6da8a7d;p=mc1516pa.git diff --git a/modelchecker/main.c b/modelchecker/main.c index 16eecbe..06729b1 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -10,143 +10,154 @@ #include "coord.h" #include "object.h" -#define ERRPRINT(fmt, as...) fprintf(stderr, fmt, ## as); -#define DPRINT(fmt, as...) if(DEBUG) ERRPRINT(fmt, ## as); - -typedef enum {OBJECT, COORD, HYBRID} strategy; +#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 DEBUG = false; -strategy strat = HYBRID; +bool VERBOSE = false; void usage(char *prg) { - ERRPRINT("Usage:\n" - "\t%s [opts] [FILE [FILE [...]]]\n" + printf("Usage:\n" + "\t%s [opts] [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" + "\t-l LURD lURD verification strategy\n" + "\t-v enable verbose 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); + "\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; } -void solve(FILE *inputstream) +int solve(FILE *inputstream, char *lurd) { - clock_t time_start_read, time_end_read; - clock_t time_start_encode, time_end_encode; + 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); - if (screen == NULL) printf("Something went wrong...\n"); - //sokoban_print(screen); + sokoban_screen *screen = parse_screen(inputstream, true); + if (screen == NULL) { + printf("Something went wrong encoding the screen\n"); + return 2; + } time_end_read = clock(); - time_start_encode = 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); + 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 + for(unsigned int i = 0; irell, 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 lucd: '%c'\n", lurd[i]); + exit(2); + } + } int iteration = 0; + bool found = false; while(new != old){ - ERRPRINT("Iteration %d\n", iteration++); + DPRINT("Iteration %d\n", iteration++); old = new; - trans_t *t = rls->rell; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - t = rls->relu; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - t = rls->relr; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - t = rls->reld; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } + 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); } - //sylvan_printdot_nc(old); - //switch(strat){ - // case COORD: - // DPRINT("Encoding coordinate based\n"); - // break; - // case OBJECT: - // DPRINT("Encoding object based\n"); - // solve_object(screen); - // break; - // case HYBRID: - // DPRINT("Encoding hybrid based\n"); - // DPRINT("Not implemented yet...\n"); - // break; - // default: - // ERRPRINT("Huh?"); - // exit(2); - //} - time_end_encode = clock(); - - //SOLVE??? + time_end_solve = clock(); + //Free and print stats sokoban_free(screen); - ERRPRINT("Reading: %fs\n", - ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC); - ERRPRINT("Encoding: %fs\n", - ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC); + 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, "cdhoy")) != -1){ + while((optchar = getopt(argc, argv, "vhl:")) != -1){ switch(optchar){ - case 'c': - strat = COORD; - DPRINT("Strategy changed to Coordinate based\n"); + case 'l': + DPRINT("Lurd detected: `%s'\n", optarg); + lurd = optarg; break; - case 'd': - DEBUG = true; + case 'v': + VERBOSE = true; DPRINT("Debug enabled\n"); break; case 'h': usage(argv[0]); return 0; - case 'o': - strat = OBJECT; - DPRINT("Strategy changed to Object based\n"); - break; - case 'y': - strat = HYBRID; - DPRINT("Strategy changed to Hybrid\n"); - break; case '?': if(isprint(optopt)){ - ERRPRINT("Unknown option `-%c'.\n", optopt); + DPRINT("Skipping unknown option `-%c'.\n", optopt); } else { - ERRPRINT("Unknown option char `-\\x%x'.\n", optopt); + DPRINT("Skipping unknown option char `-\\x%x'.\n", optopt); } return 2; default: @@ -155,18 +166,18 @@ int main(int argc, char **argv) } if(optind == argc){ - ERRPRINT("You have not specified a file, reading from stdin\n"); - solve(stdin); - } - - for(int filepathindex = optind; filepathindex < argc; filepathindex++){ - char *currentfilepath = argv[filepathindex]; - ERRPRINT("Processing: %s\n", currentfilepath); - FILE *currentfile = fopen(currentfilepath, "r"); + 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"); + if(currentfile == NULL){ + printf("File could not be opened\n"); + return 2; + } DPRINT("Opening file\n"); - solve(currentfile); + return solve(currentfile, lurd); DPRINT("Closing file\n"); fclose(currentfile); } - return 0; }