X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=85c630309be020c6d17f8e0a91b37cbec8115755;hb=956facb67e30cb9964211d00110f287f0a8d43c0;hp=409f5060053438a89512c23af53d7fc536913cb3;hpb=bfe9ddb4ffe22c1d8bdd16c39905b226cf122dd9;p=mc1516pa.git diff --git a/modelchecker/main.c b/modelchecker/main.c index 409f506..85c6303 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -2,19 +2,26 @@ #include #include #include +#include #include -#include "mc.h" #include "sokoban.h" +#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; //Global variables bool DEBUG = false; strategy strat = HYBRID; -void usage(char *prg){ - fprintf(stderr, - "Usage:\n" +void usage(char *prg) +{ + ERRPRINT("Usage:\n" "\t%s [opts] [FILE [FILE [...]]]\n" "\n" "Options:\n" @@ -33,80 +40,136 @@ void usage(char *prg){ "\t when no file is specified stdin will be used\n", prg); } -void solve(FILE *inputstream){ +void solve(FILE *inputstream) +{ clock_t time_start_read, time_end_read; clock_t time_start_encode, time_end_encode; time_start_read = clock(); - struct sokoban_screen *screen = parse_screen(inputstream); - while(screen != NULL){ - switch(screen->tile){ - case FREE: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "FREE");break; - case WALL: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "WALL");break; - case BOX: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "BOX");break; - case TARGET: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "TARGET");break; - case AGENT: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "AGENT");break; - case TARGAGENT: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "TARGAGENT");break; - case TARGBOX: printf("x = %d y = %d tile = %s\n", screen->x, screen->y, "TARGBOX");break; - } - screen = screen->next; - } - //parse_screen(inputstream); + sokoban_screen *screen = parse_screen(inputstream, false); + if (screen == NULL) printf("Something went wrong...\n"); + //sokoban_print(screen); time_end_read = clock(); time_start_encode = clock(); - switch(strat){ - case COORD: - if(DEBUG) fprintf(stderr, "Encoding coordinate based\n"); - break; - case OBJECT: - if(DEBUG) fprintf(stderr, "Encoding object based\n"); - break; - case HYBRID: - if(DEBUG) fprintf(stderr, "Encoding hybrid based\n"); - break; - default: - fprintf(stderr, "Huh?"); - exit(2); - } + + 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); + + state *init = encode_screen(screen); + state *goal = encode_goal(screen); + 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); + */ + + BDD old = sylvan_false; + BDD new = init->bdd; + 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(); - // Future: SMC - fprintf(stderr, "Reading: %fs\n", + //SOLVE??? + + sokoban_free(screen); + ERRPRINT("Reading: %fs\n", ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC); - fprintf(stderr, "Encoding: %fs\n", + ERRPRINT("Encoding: %fs\n", ((double) (time_end_encode-time_start_encode))/CLOCKS_PER_SEC); } -int main(int argc, char **argv){ +int main(int argc, char **argv) +{ int optchar; while((optchar = getopt(argc, argv, "cdhoy")) != -1){ switch(optchar){ case 'c': strat = COORD; - if(DEBUG) fprintf(stderr, "Strategy changed to Coordinate based\n"); + DPRINT("Strategy changed to Coordinate based\n"); break; case 'd': DEBUG = true; - if(DEBUG) fprintf(stderr, "Debug enabled\n"); + DPRINT("Debug enabled\n"); break; case 'h': usage(argv[0]); return 0; case 'o': strat = OBJECT; - if(DEBUG) fprintf(stderr, "Strategy changed to Object based\n"); + DPRINT("Strategy changed to Object based\n"); break; case 'y': strat = HYBRID; - if(DEBUG) fprintf(stderr, "Strategy changed to Hybrid\n"); + DPRINT("Strategy changed to Hybrid\n"); break; case '?': if(isprint(optopt)){ - fprintf(stderr, "Unknown option `-%c'.\n", optopt); + ERRPRINT("Unknown option `-%c'.\n", optopt); } else { - fprintf(stderr, "Unknown option char `-\\x%x'.\n", optopt); + ERRPRINT("Unknown option char `-\\x%x'.\n", optopt); } return 2; default: @@ -115,17 +178,17 @@ int main(int argc, char **argv){ } if(optind == argc){ - fprintf(stderr, "You have not specified a file, reading from stdin\n"); + ERRPRINT("You have not specified a file, reading from stdin\n"); solve(stdin); } for(int filepathindex = optind; filepathindex < argc; filepathindex++){ char *currentfilepath = argv[filepathindex]; - fprintf(stderr, "Processing: %s\n", currentfilepath); + ERRPRINT("Processing: %s\n", currentfilepath); FILE *currentfile = fopen(currentfilepath, "r"); - if(DEBUG) fprintf(stderr, "Opening file\n"); + DPRINT("Opening file\n"); solve(currentfile); - if(DEBUG) fprintf(stderr, "Closing file\n"); + DPRINT("Closing file\n"); fclose(currentfile); } return 0;