From: Mart Lubbers Date: Wed, 20 Apr 2016 18:20:56 +0000 (+0200) Subject: Merge remote-tracking branch 'origin/lurd' X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=6d27f2cbfee60299b29e28167962574d09851d34;p=mc1516pa.git Merge remote-tracking branch 'origin/lurd' Conflicts: modelchecker/main.c --- 6d27f2cbfee60299b29e28167962574d09851d34 diff --cc modelchecker/benchmark.sh index 0000000,0000000..05808dd new file mode 100644 --- /dev/null +++ b/modelchecker/benchmark.sh @@@ -1,0 -1,0 +1,6 @@@ ++#!/bin/bash ++make ++for i in 2000 107 1001 387 372 792 747 38 754 2; do ++ echo "Problem: $i" ++ time ./main -v ../sokobanzip/screens/screen.$i ++done diff --cc modelchecker/main.c index bdf8a12,b50a1a4..1f518eb --- a/modelchecker/main.c +++ b/modelchecker/main.c @@@ -18,112 -21,204 +18,137 @@@ 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" -// "\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); } -int lurd_solve(FILE *inputstream, char *lurd){ - - sokoban_screen *screen = parse_screen(inputstream, false); - if (screen == NULL) printf("Something went wrong...\n"); - - lace_init(0, 1000000); - lace_startup(0, NULL, NULL); +BDD subsolve(trans_t *t, BDD new){ LACE_ME; - sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26); - sylvan_init_bdd(6); - - state *init = encode_screen(screen); - state *goal = encode_goal(screen); - if (goal == NULL) printf("WRONG\n"); - rels *rls = encode_rel(screen); - BDD new = init->bdd; - trans_t *t = NULL; - - while (*lurd != '\n'){ - printf("We're here1\n"); - switch(*lurd){ - case 'l': - printf("We're here2\n"); - t = rls->rell; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - lurd++; - break; - case 'u': - t = rls->relu; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - lurd++; - break; - case 'r': - t = rls->relr; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - lurd++; - break; - case 'd': - t = rls->reld; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - } - lurd++; - break; - default: lurd++; - } - - } - - double check = 0; - if (goal != NULL) { - check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset); - } - if (check > 0) return 1; - else return 0; + while (t != NULL){ + new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); + t = t->next_rel; + } + return new; } - int solve(FILE *inputstream) -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, false); - if (screen == NULL) printf("Something went wrong...\n"); - //sokoban_print(screen); + 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); - state *goal = encode_goal(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); - /* - printf("Doing left\n"); - test_trans(init, rls->rell); - printf("Doing up\n"); - test_trans(init, rls->relu); - printf("Doing right\n"); - test_trans(init, rls->relr); - printf("Doing down\n"); - test_trans(init, rls->reld); - */ + time_end_rel = clock(); + + + //Actually solve + time_start_solve = clock(); BDD old = sylvan_false; BDD new = init->bdd; ++ //Do lurd ++ while(*lurd != '\0'){ ++ switch(*lurd){ ++ case 'l': ++ new = subsolve(rls->rell, 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); ++ exit(2); ++ } ++ lurd++; ++ } int iteration = 0; - if (goal != NULL){ - while(new != old){ - old = new; - ERRPRINT("Iteration %d\n", iteration++); - trans_t *t = rls->rell; - - //for testing - /* - BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9); - BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0}); - BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0})); - BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1})); - if (new == teststate2) printf("Wrong!\n"); - */ - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - - t = rls->relu; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - - - t = rls->relr; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - - - t = rls->reld; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - double check = sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset); - if (check > 0){ - printf("Solution is found after %d iteration(s)!\n", iteration); - break; - } - } - } - else printf("No solution found!\n"); - //ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset)); -// sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL); -// sylvan_printdot_nc(old); - time_end_encode = clock(); + bool found = false; + while(new != old){ + DPRINT("Iteration %d\n", iteration++); + old = new; + if(sylvan_satcount(sylvan_and(goal->bdd, new), init->vars.varset) > 0){ + found = true; + break; + } - //SOLVE??? + //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); + } + 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, "vh")) != -1){ - 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': @@@ -142,14 -245,19 +167,13 @@@ } if(optind == argc){ - ERRPRINT("You have not specified a file, reading from stdin\n"); - //solve(stdin); - char lrd[] = "ll\n"; - if (lurd_solve(stdin, lrd) == 1) printf ("The given lurd solves the given screen\n"); - else printf ("The given lurd can not solve the given screen\n"); - } - - 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); ++ return solve(stdin, lurd); + } else { + DPRINT("Processing: %s\n", argv[optind]); - DPRINT("Thus skipping the other %d files\n", argc-optind); + FILE *currentfile = fopen(argv[optind], "r"); DPRINT("Opening file\n"); - return solve(currentfile); - solve(currentfile); ++ return solve(currentfile, lurd); DPRINT("Closing file\n"); fclose(currentfile); }