From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Sun, 17 Apr 2016 08:19:51 +0000 (+0200)
Subject: model checker fix
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=81eb34c9ea8b55240eb973b1e9f3911fb6da8a7d;p=mc1516pa.git

model checker fix
---

diff --git a/modelchecker/coord.c b/modelchecker/coord.c
index 200db36..caa7b78 100644
--- a/modelchecker/coord.c
+++ b/modelchecker/coord.c
@@ -1072,6 +1072,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
 	trs_current = trs;
 
     //test
+    /*
     switch(dir){
     case LEFT:
         if (trs_current != NULL) printf("LEFT ok!\n");
@@ -1094,7 +1095,7 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir)
         printf("Num of trans relations:%d\n", countTrans(trs));
         break;
     }
-
+    */
 	return trs;
 }
 
diff --git a/modelchecker/main.c b/modelchecker/main.c
index 61edfca..16eecbe 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -68,14 +68,26 @@ void solve(FILE *inputstream)
 	while(new != old){
 		ERRPRINT("Iteration %d\n", iteration++);
 		old = new;
-        //WRONG! each trans relation (LEFT,UP,RIGHT,DOWN) contains a linked list of trans relations (not just
-        //only one), so to compute a transition for a single direction, we need to iterate through a relevant linked list
-        //taking disjunction of results (for a single direction there will be falses and only one screen change among the
-        //results)
-		new = sylvan_or(new, sylvan_relnext(new, rls->rell->bdd, rls->rell->varset.varset));
-		new = sylvan_or(new, sylvan_relnext(new, rls->relu->bdd, rls->relu->varset.varset));
-		new = sylvan_or(new, sylvan_relnext(new, rls->relr->bdd, rls->relr->varset.varset));
-		new = sylvan_or(new, sylvan_relnext(new, rls->reld->bdd, rls->reld->varset.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;
+        }
+        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;
+        }
 	}
 		//sylvan_printdot_nc(old);
 	//switch(strat){