From: Alexander Fedotov 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));