From: Mart Lubbers Date: Sun, 17 Apr 2016 14:38:30 +0000 (+0200) Subject: checked all 1 and 2 cases X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=4a12ac1dc78abbc034e2e12e6571ddd474deb877;p=mc1516pa.git checked all 1 and 2 cases --- diff --git a/modelchecker/coord.c b/modelchecker/coord.c index caa7b78..5ff92e1 100644 --- a/modelchecker/coord.c +++ b/modelchecker/coord.c @@ -310,16 +310,16 @@ trans_t *create_single_rel(sokoban_screen *screen, direction dir) trs = trs_current; //Agent Target -> Free Targagent - //(1 0 0 0 1 1 0 1 1 1 1 0) + //(1 0 0 0 1 1 - 0 1 1 1 1 0) //or - //(0 1 1 1 1 0 0 1 1 1 1 0) + //(0 1 1 1 1 0 - 1 0 0 0 1 1) relvarset = sylvan_set_fromarray(relvars, 12); if (i < deltai){ uint8_t rel_enc2[12] = {1, 0, 0, 0, 1, 1, 0, 1, 1, 1, 1, 0}; memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); } else { - uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 0, 1, 1, 1, 1, 0}; + uint8_t rel_enc2[12] = {0, 1, 1, 1, 1, 0, 1, 0, 0, 0, 1, 1}; memcpy(rel_enc, rel_enc2, 12*sizeof(uint8_t)); } trs_current = (trans_t *)malloc(sizeof(trans_t)); diff --git a/modelchecker/main.c b/modelchecker/main.c index 16eecbe..fd37c23 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -66,9 +66,11 @@ void solve(FILE *inputstream) BDD new = init->bdd; int iteration = 0; while(new != old){ - ERRPRINT("Iteration %d\n", iteration++); old = new; + ERRPRINT("Iteration %d\n", iteration++); + ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.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; diff --git a/modelchecker/toy.screen b/modelchecker/toy.screen index 8d4f16e..a381e1a 100644 --- a/modelchecker/toy.screen +++ b/modelchecker/toy.screen @@ -1 +1,2 @@ -@$. +@ +.