From 81eb34c9ea8b55240eb973b1e9f3911fb6da8a7d Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Sun, 17 Apr 2016 10:19:51 +0200 Subject: [PATCH] model checker fix --- modelchecker/coord.c | 3 ++- modelchecker/main.c | 28 ++++++++++++++++++++-------- 2 files changed, 22 insertions(+), 9 deletions(-) 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){ -- 2.20.1