checked all 1 and 2 cases

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index caa7b78..5ff92e1 100644 (file)
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -310,16 +310,16 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
                        trs = trs_current;
 
             //Agent Target -> Free Targagent
-            //(1 0 0 0 1 1 0 1 1 1 1 0)
+            //(1 0 0 0 1 1 - 0 1 1 1 1 0)
             //or
-            //(0 1 1 1 1 0 0 1 1 1 1 0)
+            //(0 1 1 1 1 0 - 1 0 0 0 1 1)
                        relvarset = sylvan_set_fromarray(relvars, 12);
             if (i < deltai){
                 uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0};
                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
             }
             else {
-                uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0};
+                uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1};
                 memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t));
             }
                        trs_current = (trans_t *)malloc(sizeof(trans_t));

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 16eecbe..fd37c23 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -66,9 +66,11 @@ void solve(FILE *inputstream)
        BDD new = init->bdd;
        int iteration = 0;
        while(new != old){
-               ERRPRINT("Iteration %d\n", iteration++);
                old = new;
+               ERRPRINT("Iteration %d\n", iteration++);
+               ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
         trans_t *t = rls->rell;
+
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;

diff --git a/modelchecker/toy.screen b/modelchecker/toy.screen
index 8d4f16e..a381e1a 100644 (file)
--- a/modelchecker/toy.screen
+++ b/modelchecker/toy.screen
@@ -1 +1,2 @@
-@$.
+@
+.