sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

proper caching in all min/max/exists abstract representative functions

main
dehnert 8 years ago
parent
27ffeb3a45
commit
9a20aed7f9
5 changed files with 52 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
  2. 9
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  3. 27
      resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
  4. 34
      resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
  5. 6
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

16
resources/3rdparty/cudd-3.0.0/cudd/cuddAddAbs.c
View File

@ -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);

9
resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
View File

@ -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) {

27
resources/3rdparty/sylvan/src/sylvan_bdd_storm.c
View File

@ -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;
}

34
resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c
View File

@ -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);

6
src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
View File

@ -526,8 +526,12 @@ namespace storm {
InternalSparseQuotientExtractor<DdType, ValueType> 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<ValueType> 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<std::chrono::milliseconds>(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<std::chrono::milliseconds>(end - start).count() << "ms.");
std::shared_ptr<storm::models::sparse::Model<ValueType>> result;
if (model.getType() == storm::models::ModelType::Dtmc) {

Write Preview
Loading…
Cancel
Save