small update

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 38597f6..6c94363 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -60,6 +60,7 @@ void solve(FILE *inputstream)
     sylvan_init_bdd(6);
 
        state *init = encode_screen(screen);
+    state *goal = encode_goal(screen);
        rels *rls = encode_rel(screen);
     /*
     printf("Doing left\n");
@@ -75,49 +76,52 @@ void solve(FILE *inputstream)
        BDD old = sylvan_false;
        BDD new = init->bdd;
        int iteration = 0;
-       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));
-        }
+    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));
+            }
 
-        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));
-        }
-
-       }
+    }
+    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);