X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=7cc10704231e88d942f2b92ed37d0d0a32697993;hb=82a071f2894cfcc59511458c69e8e59581055880;hp=8ee1bd3395e73123f7c175eaedca9fdb04198c28;hpb=961d38840cf50e864cb83711bd9419033c3acd7d;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 8ee1bd3..7cc1070 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -58,31 +58,61 @@ void solve(FILE *inputstream)
 	LACE_ME;
     sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26);
     sylvan_init_bdd(6);
-	switch(strat){
-		case COORD:
-			DPRINT("Encoding coordinate based\n");
-			state *s = encode_screen(screen);
-			//test_relprod();
-			rels *rls = encode_rel(screen);
-            test_trans(s, rls->relr);
-			break;
-		case OBJECT:
-			DPRINT("Encoding object based\n");
-			solve_object(screen);
-			break;
-		case HYBRID:
-			DPRINT("Encoding hybrid based\n");
-			DPRINT("Not implemented yet...\n");
-			break;
-		default:
-			ERRPRINT("Huh?");
-			exit(2);
+
+	state *init = encode_screen(screen);
+	rels *rls = encode_rel(screen);
+
+	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;
+
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        t = rls->relu;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        t = rls->relr;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
+        t = rls->reld;
+        while (t != NULL){
+            new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
+            t = t->next_rel;
+        }
 	}
-	sokoban_free(screen);
+	ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
+		//sylvan_printdot_nc(old);
+	//switch(strat){
+	//	case COORD:
+	//		DPRINT("Encoding coordinate based\n");
+	//		break;
+	//	case OBJECT:
+	//		DPRINT("Encoding object based\n");
+	//		solve_object(screen);
+	//		break;
+	//	case HYBRID:
+	//		DPRINT("Encoding hybrid based\n");
+	//		DPRINT("Not implemented yet...\n");
+	//		break;
+	//	default:
+	//		ERRPRINT("Huh?");
+	//		exit(2);
+	//}
 	time_end_encode = clock();
 
 	//SOLVE???
 
+	sokoban_free(screen);
 	ERRPRINT("Reading: %fs\n",
 		((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC);
 	ERRPRINT("Encoding: %fs\n",