X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=modelchecker%2Fmain.c;h=0b0067b80b8a07002f128925653bfb9e8fd6526d;hb=cbf15c012aa6fd764ec9ea20772b6aff6457351b;hp=b262660d4ca3418ed04144c9ffb282a8516064d7;hpb=9e1a2f4a73174e25df74833a362c583b1020fa71;p=mc1516pa.git

diff --git a/modelchecker/main.c b/modelchecker/main.c
index b262660..0b0067b 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -77,10 +77,9 @@ int solve(FILE *inputstream, char *lurd)
 	rels *rls = encode_rel(screen);
 	time_end_rel = clock();
 
-
 	//Actually solve
 	time_start_solve = clock();
-	BDD old = sylvan_false;
+	//BDD old = sylvan_false;
 	BDD new = init->bdd;
 	//Do lurd
 	while(*lurd != '\0'){
@@ -103,8 +102,10 @@ int solve(FILE *inputstream, char *lurd)
 		}
 		lurd++;
 	}
-	int iteration = 0;
+	//int iteration = 0;
+
 	bool found = false;
+    /*
 	while(new != old){
 		DPRINT("Iteration %d\n", iteration++);
 		old = new;
@@ -119,6 +120,23 @@ int solve(FILE *inputstream, char *lurd)
 		new = subsolve(rls->relr, new);
 		new = subsolve(rls->reld, new);
 	}
+    */
+    state_t *res = NULL;
+    state *cont = (state *)malloc(sizeof(cont));
+    cont->bdd = new;
+    cont->vars = init->vars;
+    res = explstate(cont, rls, goal);
+    if (res != NULL){
+        if (res->lrd == NULL) printf("wrong\n");
+        lurd_t *l = res->lrd;
+        while (l != NULL){
+            printf("%c", l->c);
+            l = l->next;
+        }
+        printf("\n");
+    } else found = 0;
+
+
 	time_end_solve = clock();
 
 	//Free and print stats