model checker fix

[mc1516pa.git] / modelchecker / main.c

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 95b8458..16eecbe 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -68,10 +68,26 @@ void solve(FILE *inputstream)
        while(new != old){
                ERRPRINT("Iteration %d\n", iteration++);
                old = new;
-               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){