From 4885d6dc58a7cf7df3073b3f08fc3a83e525d68f Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Sun, 17 Apr 2016 09:48:05 +0200 Subject: [PATCH] small update --- modelchecker/main.c | 4 ++++ 1 file changed, 4 insertions(+) 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)); -- 2.20.1