Merge branch 'master' of https://github.com/dopefishh/mc1516pa

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index b262660..79bb46d 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -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"
@@ -77,7 +77,6 @@ int solve(FILE *inputstream, char *lurd)
        rels *rls = encode_rel(screen);
        time_end_rel = clock();
 
-
        //Actually solve
        time_start_solve = clock();
        BDD old = sylvan_false;
@@ -104,7 +103,9 @@ int solve(FILE *inputstream, char *lurd)
                lurd++;
        }
        int iteration = 0;
+
        bool found = false;
+
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
                old = new;
@@ -119,6 +120,7 @@ int solve(FILE *inputstream, char *lurd)
                new = subsolve(rls->relr, new);
                new = subsolve(rls->reld, new);
        }
+
        time_end_solve = clock();
 
        //Free and print stats
@@ -129,10 +131,12 @@ int solve(FILE *inputstream, char *lurd)
        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;
 }