goal state encoder added

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 5ca9c87..38597f6 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -61,7 +61,16 @@ void solve(FILE *inputstream)
 
        state *init = encode_screen(screen);
        rels *rls = encode_rel(screen);
-    //test_trans(init, rls->reld);
+    /*
+    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;
@@ -71,25 +80,43 @@ void solve(FILE *inputstream)
                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));
         }
+
        }
        ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
 //     sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL);