From c4d4a1d7cbe6a1c6dd2a2b3ba80b3f3029ee8186 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Fri, 15 Apr 2016 17:22:05 +0200 Subject: [PATCH] small update modelchecken --- modelchecker/main.c | 52 ++++++++++++++++++++++++++++----------------- 1 file changed, 32 insertions(+), 20 deletions(-) diff --git a/modelchecker/main.c b/modelchecker/main.c index 8ee1bd3..95b8458 100644 --- a/modelchecker/main.c +++ b/modelchecker/main.c @@ -58,31 +58,43 @@ void solve(FILE *inputstream) LACE_ME; sylvan_init_package(1LL<<21, 1LL<<27, 1LL<<20, 1LL<<26); sylvan_init_bdd(6); - switch(strat){ - case COORD: - DPRINT("Encoding coordinate based\n"); - state *s = encode_screen(screen); - //test_relprod(); - rels *rls = encode_rel(screen); - test_trans(s, rls->relr); - break; - case OBJECT: - DPRINT("Encoding object based\n"); - solve_object(screen); - break; - case HYBRID: - DPRINT("Encoding hybrid based\n"); - DPRINT("Not implemented yet...\n"); - break; - default: - ERRPRINT("Huh?"); - exit(2); + + state *init = encode_screen(screen); + rels *rls = encode_rel(screen); + + BDD old = sylvan_false; + BDD new = init->bdd; + int iteration = 0; + while(new != old){ + ERRPRINT("Iteration %d\n", iteration++); + old = new; + 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)); } - sokoban_free(screen); + //sylvan_printdot_nc(old); + //switch(strat){ + // case COORD: + // DPRINT("Encoding coordinate based\n"); + // break; + // case OBJECT: + // DPRINT("Encoding object based\n"); + // solve_object(screen); + // break; + // case HYBRID: + // DPRINT("Encoding hybrid based\n"); + // DPRINT("Not implemented yet...\n"); + // break; + // default: + // ERRPRINT("Huh?"); + // exit(2); + //} time_end_encode = clock(); //SOLVE??? + sokoban_free(screen); ERRPRINT("Reading: %fs\n", ((double) (time_end_read-time_start_read))/CLOCKS_PER_SEC); ERRPRINT("Encoding: %fs\n", -- 2.20.1