added verdict, also in positive case_

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 232bac6..4c03c32 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -8,7 +8,6 @@
 
 #include "sokoban.h"
 #include "coord.h"
-#include "object.h"
 
 #define DPRINT(fmt, as...) if(VERBOSE) fprintf(stderr, fmt, ## as);
 #define REPORT(s, end, start) DPRINT(s, ((double)(end-start))/CLOCKS_PER_SEC);
@@ -22,7 +21,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"
@@ -48,7 +47,7 @@ int solve(FILE *inputstream, char *lurd)
 
        //Read screen
        time_start_read = clock();
-       sokoban_screen *screen = parse_screen(inputstream, false);
+       sokoban_screen *screen = parse_screen(inputstream, true);
        if (screen == NULL) {
                printf("Something went wrong encoding the screen\n");
                return 2;
@@ -79,7 +78,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'){
@@ -102,10 +101,10 @@ int solve(FILE *inputstream, char *lurd)
                }
                lurd++;
        }
-       //int iteration = 0;
+       int iteration = 0;
+
+       bool found = false;
 
-       //bool found = false;
-    /*
        while(new != old){
                DPRINT("Iteration %d\n", iteration++);
                old = new;
@@ -120,22 +119,6 @@ int solve(FILE *inputstream, char *lurd)
                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();
 
@@ -146,13 +129,13 @@ int solve(FILE *inputstream, char *lurd)
        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);
+       DPRINT("Iterations needed: %d\n", iteration);
 
-    /*
        if(!found){
                printf("no solution\n");
                return 1;
        }
-    */
+       DPRINT("Solution found\n");
        return 0;
 }