Merge branch 'master' of https://github.com/dopefishh/mc1516pa
authorAlexander Fedotov <soyaxhoya@gmail.com>
Thu, 21 Apr 2016 18:35:07 +0000 (20:35 +0200)
committerAlexander Fedotov <soyaxhoya@gmail.com>
Thu, 21 Apr 2016 18:35:07 +0000 (20:35 +0200)
1  2 
modelchecker/main.c

diff --combined modelchecker/main.c
@@@ -22,7 -22,7 +22,7 @@@ void usage(char *prg
                "\t%s [opts] [FILE]\n"
                "\n"
                "Options:\n"
-               "\t-l LURD lURD verification strategy\n"
+               "\t-l LURD initial LURD\n"
                "\t-v      enable verbose output\n"
                "\t-h      show this help\n"
                "\n"
@@@ -79,7 -79,7 +79,7 @@@ int solve(FILE *inputstream, char *lurd
  
        //Actually solve
        time_start_solve = clock();
 -      //BDD old = sylvan_false;
 +      BDD old = sylvan_false;
        BDD new = init->bdd;
        //Do lurd
        while(*lurd != '\0'){
                }
                lurd++;
        }
 -      //int iteration = 0;
 +      int iteration = 0;
 +
 +      bool found = false;
  
 -      //bool found = false;
 -    /*
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
                old = new;
                new = subsolve(rls->relr, new);
                new = subsolve(rls->reld, new);
        }
 -    */
 -    state_t *res = NULL;
 -    state *cont = (state *)malloc(sizeof(cont));
 -    cont->bdd = new;
 -    cont->vars = init->vars;
 -    res = explstate(cont, rls, goal);
 -    if (res != NULL){
 -        if (res->lrd == NULL) printf("wrong\n");
 -        lurd_t *l = res->lrd;
 -        while (l != NULL){
 -            printf("%c", l->c);
 -            l = l->next;
 -        }
 -        printf("\n");
 -    }
 -
  
        time_end_solve = clock();
  
        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;
  }