From 50c4622421e7d21749bc546d35e40b47cd40b353 Mon Sep 17 00:00:00 2001 From: Alexander Fedotov Date: Wed, 20 Apr 2016 15:21:25 +0200 Subject: [PATCH] small update --- modelchecker/main.c | 86 ++++++++++++++++++++++++--------------------- 1 file changed, 45 insertions(+), 41 deletions(-) diff --git a/modelchecker/main.c b/modelchecker/main.c index 38597f6..6c94363 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -60,6 +60,7 @@ void solve(FILE *inputstream) sylvan_init_bdd(6); state *init = encode_screen(screen); + state *goal = encode_goal(screen); rels *rls = encode_rel(screen); /* printf("Doing left\n"); @@ -75,49 +76,52 @@ void solve(FILE *inputstream) BDD old = sylvan_false; BDD new = init->bdd; int iteration = 0; - while(new != old){ - old = new; - ERRPRINT("Iteration %d\n", iteration++); - trans_t *t = rls->rell; - - //for testing - /* - BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9); - BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0}); - BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0})); - BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1})); - if (new == teststate2) printf("Wrong!\n"); - */ - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } + if (goal != NULL){ + while(new != old){ + old = new; + ERRPRINT("Iteration %d\n", iteration++); + trans_t *t = rls->rell; + + //for testing + /* + BDDSET testvars = sylvan_set_fromarray(((BDDVAR[]){0,2,4,6,8,10,12,14,16}), 9); + BDD teststate = sylvan_cube(testvars, (uint8_t[]){1,0,1,0,0,1,0,1,0}); + BDD teststate1 = sylvan_or(teststate, sylvan_cube(testvars, (uint8_t[]){0,0,1,1,0,1,0,1,0})); + BDD teststate2 = sylvan_or(teststate1, sylvan_cube(testvars, (uint8_t[]){0,1,0,0,0,1,1,0,1})); + if (new == teststate2) printf("Wrong!\n"); + */ + while (t != NULL){ + new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); + t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); + } + + t = rls->relu; + while (t != NULL){ + new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); + t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); + } + + + t = rls->relr; + while (t != NULL){ + new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); + t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); + } + + + t = rls->reld; + while (t != NULL){ + new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); + t = t->next_rel; + //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); + } - t = rls->relu; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); } - - - t = rls->relr; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - - - t = rls->reld; - while (t != NULL){ - new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset)); - t = t->next_rel; - //ERRPRINT("Satcount: %f\n", sylvan_satcount(new, init->vars.varset)); - } - - } + } + else printf("No solution found!\n"); ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset)); // sylvan_enum(old, init->vars.varset, (enum_cb)callback, NULL); // sylvan_printdot_nc(old); -- 2.20.1