From: Alexander Fedotov <soyaxhoya@gmail.com>
Date: Sun, 17 Apr 2016 07:48:05 +0000 (+0200)
Subject: small update
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4885d6dc58a7cf7df3073b3f08fc3a83e525d68f;p=mc1516pa.git

small update
---

diff --git a/modelchecker/main.c b/modelchecker/main.c
index 95b8458..61edfca 100644
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -68,6 +68,10 @@ 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));