From: Mart Lubbers <mart@martlubbers.net>
Date: Sun, 17 Apr 2016 14:38:30 +0000 (+0200)
Subject: checked all 1 and 2 cases
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4a12ac1dc78abbc034e2e12e6571ddd474deb877;p=mc1516pa.git

checked all 1 and 2 cases
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index caa7b78..5ff92e1 100644
--- 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
--- 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
--- a/modelchecker/toy.screen
+++ b/modelchecker/toy.screen
@@ -1 +1,2 @@
-@$.
+@
+.