diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c index 1f8414017..a1d7e6105 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c @@ -1024,6 +1024,10 @@ cuddAddMinAbstractRepresentativeRecur( return(res1); } + if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { + return(res); + } + /* Abstract a variable that does not appear in f. */ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { res = cuddAddMinAbstractRepresentativeRecur(manager, f, cuddT(cube)); @@ -1044,10 +1048,6 @@ cuddAddMinAbstractRepresentativeRecur( return(res1); } - if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstractRepresentative, f, cube)) != NULL) { - return(res); - } - E = cuddE(f); T = cuddT(f); @@ -1211,6 +1211,10 @@ cuddAddMaxAbstractRepresentativeRecur( } + if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstractRepresentative, f, cube)) != NULL) { + return(res); + } + /* Abstract a variable that does not appear in f. */ if (cuddI(manager,f->index) > cuddI(manager,cube->index)) { res = cuddAddMaxAbstractRepresentativeRecur(manager, f, cuddT(cube)); @@ -1231,10 +1235,6 @@ cuddAddMaxAbstractRepresentativeRecur( return(res1); } - if ((res = cuddCacheLookup2(manager, Cudd_addMaxAbstractRepresentative, f, cube)) != NULL) { - return(res); - } - E = cuddE(f); T = cuddT(f); diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index 8c3026b9d..d640d2147 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -563,6 +563,10 @@ cuddBddExistAbstractRepresentativeRecur( } /* From now on, cube and f are non-constant. */ + /* Check the cache. */ + if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) { + return(res); + } /* Abstract a variable that does not appear in f. */ if (manager->perm[F->index] > manager->perm[cube->index]) { @@ -586,11 +590,6 @@ cuddBddExistAbstractRepresentativeRecur( return(res1); } - /* Check the cache. */ - if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) { - return(res); - } - /* Compute the cofactors of f. */ T = cuddT(F); E = cuddE(F); if (f != F) { diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c index 89f2c31a2..7e982cc1c 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_bdd_storm.c @@ -12,7 +12,6 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr if (aRegular == sylvan_false) { if (aIsNegated) { if (sylvan_set_isempty(variables)) { - //printf("return in preprocessing...2\n"); return sylvan_true; } else { //printf("return in preprocessing...3\n"); @@ -35,18 +34,22 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return a; } } else if (sylvan_set_isempty(variables)) { - //printf("return in preprocessing...4\n"); return a; } + + BDD result; + if (cache_get3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, variables, (size_t)2, &result)) { + sylvan_stats_count(MTBDD_ABSTRACT_CACHED); + return result; + } + /* From now on, f and cube are non-constant. */ bddnode_t na = MTBDD_GETNODE(a); BDDVAR level = bddnode_getvariable(na); bddnode_t nv = MTBDD_GETNODE(variables); BDDVAR vv = bddnode_getvariable(nv); - - //printf("a level %i and cube level %i\n", level, vv); - + /* Abstract a variable that does not appear in f. */ if (level > vv) { BDD _v = sylvan_set_next(variables); @@ -64,7 +67,6 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr } sylvan_deref(res); - //printf("return after abstr. var that does not appear in f...\n"); return res1; } @@ -128,13 +130,14 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr return sylvan_invalid; } - // cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res); - // TODO: CACHING HERE + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, variables, (size_t)2, res)) { + sylvan_stats_count(MTBDD_ABSTRACT_CACHEDPUT); + } sylvan_deref(res1Inf); sylvan_deref(res2Inf); - //printf("return properly computed result...\n"); return res; } else { /* if (level == vv) */ BDD res1 = CALL(sylvan_existsRepresentative, aLow, variables, level); @@ -162,7 +165,11 @@ TASK_IMPL_3(BDD, sylvan_existsRepresentative, BDD, a, BDD, variables, BDDVAR, pr sylvan_deref(res1); sylvan_deref(res2); - //printf("return of last case...\n"); + /* Store in cache */ + if (cache_put3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, variables, (size_t)2, res)) { + sylvan_stats_count(MTBDD_ABSTRACT_CACHEDPUT); + } + return res; } diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 873c116f4..39de0400b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -616,11 +616,18 @@ TASK_IMPL_3(BDD, mtbdd_min_abstract_representative, MTBDD, a, BDD, v, BDDVAR, pr return res1; } + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, v, (size_t)1, &result)) { + sylvan_stats_count(MTBDD_ABSTRACT_CACHED); + return result; + } + mtbddnode_t na = MTBDD_GETNODE(a); uint32_t va = mtbddnode_getvariable(na); bddnode_t nv = MTBDD_GETNODE(v); BDDVAR vv = bddnode_getvariable(nv); - + /* Abstract a variable that does not appear in a. */ if (va > vv) { BDD _v = sylvan_set_next(v); @@ -640,13 +647,6 @@ TASK_IMPL_3(BDD, mtbdd_min_abstract_representative, MTBDD, a, BDD, v, BDDVAR, pr return res1; } - /* Check cache */ - MTBDD result; - if (cache_get3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, v, (size_t)1, &result)) { - sylvan_stats_count(MTBDD_ABSTRACT_CACHED); - return result; - } - MTBDD E = mtbdd_getlow(a); MTBDD T = mtbdd_gethigh(a); @@ -796,12 +796,19 @@ TASK_IMPL_3(BDD, mtbdd_max_abstract_representative, MTBDD, a, MTBDD, v, uint32_t return res1; } - + + /* Check cache */ + MTBDD result; + if (cache_get3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, v, (size_t)0, &result)) { + sylvan_stats_count(MTBDD_ABSTRACT_CACHED); + return result; + } + mtbddnode_t na = MTBDD_GETNODE(a); uint32_t va = mtbddnode_getvariable(na); bddnode_t nv = MTBDD_GETNODE(v); BDDVAR vv = bddnode_getvariable(nv); - + /* Abstract a variable that does not appear in a. */ if (vv < va) { BDD _v = sylvan_set_next(v); @@ -821,13 +828,6 @@ TASK_IMPL_3(BDD, mtbdd_max_abstract_representative, MTBDD, a, MTBDD, v, uint32_t return res1; } - /* Check cache */ - MTBDD result; - if (cache_get3(CACHE_MTBDD_ABSTRACT_REPRESENTATIVE, a, v, (size_t)0, &result)) { - sylvan_stats_count(MTBDD_ABSTRACT_CACHED); - return result; - } - MTBDD E = mtbdd_getlow(a); MTBDD T = mtbdd_gethigh(a); diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 5767cb448..502885d7d 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -526,8 +526,12 @@ namespace storm { InternalSparseQuotientExtractor sparseExtractor(model.getManager(), model.getRowVariables(), model.getNondeterminismVariables()); auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs()); + auto start = std::chrono::high_resolution_clock::now(); storm::storage::SparseMatrix quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix(), partition); + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + start = std::chrono::high_resolution_clock::now(); storm::models::sparse::StateLabeling quotientStateLabeling(partition.getNumberOfBlocks()); quotientStateLabeling.addLabel("init", sparseExtractor.extractStates(model.getInitialStates(), partition)); quotientStateLabeling.addLabel("deadlock", sparseExtractor.extractStates(model.getDeadlockStates(), partition)); @@ -546,6 +550,8 @@ namespace storm { quotientStateLabeling.addLabel(stream.str(), sparseExtractor.extractStates(model.getStates(expression), partition)); } } + end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); std::shared_ptr> result; if (model.getType() == storm::models::ModelType::Dtmc) {