From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Thu, 21 Apr 2016 18:33:38 +0000 (+0200)
Subject: the old main is back
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=d92a18de3e99d0bb43e733cec7d3d7fad8be2c75;p=mc1516pa.git

the old main is back
---

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 232bac6..2138dfc 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -79,7 +79,7 @@ int solve(FILE *inputstream, char *lurd)
 
 	//Actually solve
 	time_start_solve = clock();
-	//BDD old = sylvan_false;
+	BDD old = sylvan_false;
 	BDD new = init->bdd;
 	//Do lurd
 	while(*lurd != '\0'){
@@ -102,10 +102,10 @@ int solve(FILE *inputstream, char *lurd)
 		}
 		lurd++;
 	}
-	//int iteration = 0;
+	int iteration = 0;
+
+	bool found = false;
 
-	//bool found = false;
-    /*
 	while(new != old){
 		DPRINT("Iteration %d\n", iteration++);
 		old = new;
@@ -120,22 +120,6 @@ 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");
-    }
-
 
 	time_end_solve = clock();
 
@@ -147,12 +131,12 @@ int solve(FILE *inputstream, char *lurd)
 	REPORT("Relation encoding: %fs\n", time_end_rel, time_start_rel);
 	REPORT("Solving encoding: %fs\n", time_end_solve, time_start_solve);
 
-    /*
+
 	if(!found){
 		printf("no solution\n");
 		return 1;
 	}
-    */
+
 	return 0;
 }