From 86c233f3dff00aa65b0a6d1e7488acc922dc14b1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 May 2016 18:18:58 +0200 Subject: [PATCH] fixed bug in sylvan Former-commit-id: 3f3a3df83d557759d3acdb69a8e35ac928f1e62a --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 10 ++--- .../3rdparty/sylvan/src/sylvan_mtbdd_storm.c | 37 +++++++++++++++++++ .../3rdparty/sylvan/src/sylvan_mtbdd_storm.h | 2 + .../sylvan/src/sylvan_obj_mtbdd_storm.hpp | 2 +- .../3rdparty/sylvan/src/sylvan_obj_storm.cpp | 8 ++++ .../SymbolicMinMaxLinearEquationSolver.cpp | 2 +- 6 files changed, 54 insertions(+), 7 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index f553f9e7e..87db4c84b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -1434,8 +1434,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, sho if (result != SYNC(mtbdd_equal_norm_d2)) result = mtbdd_false; if (result == mtbdd_false) *shortcircuit = 1; - /* Store in cache */ - cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result); + /* Store in cache (only if we are not short circuiting) */ + if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM, a, b, svalue, result); return result; } @@ -1470,7 +1470,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, // assume Double MTBDD double va = mtbdd_getdouble(a); double vb = mtbdd_getdouble(b); - if (va == 0) return mtbdd_false; + if (va == 0.0 || va == -0.0) return mtbdd_false; va = (va - vb) / va; if (va < 0) va = -va; return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false; @@ -1501,8 +1501,8 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*, if (result != SYNC(mtbdd_equal_norm_rel_d2)) result = mtbdd_false; if (result == mtbdd_false) *shortcircuit = 1; - /* Store in cache */ - cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result); + /* Store in cache (only if we are not short circuiting) */ + if (!*shortcircuit) cache_put3(CACHE_MTBDD_EQUAL_NORM_REL, a, b, svalue, result); return result; } diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c index 37fd53cf5..dab4860c0 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c @@ -1,3 +1,40 @@ +/** + * Generate SHA2 structural hashes. + * Hashes are independent of location. + * Mainly useful for debugging purposes. + */ +static void +mtbdd_sha2_rec(MTBDD mtbdd, SHA256_CTX *ctx) +{ + if (mtbdd == sylvan_true || mtbdd == sylvan_false) { + SHA256_Update(ctx, (void*)&mtbdd, sizeof(MTBDD)); + return; + } + + mtbddnode_t node = GETNODE(mtbdd); + if (mtbddnode_isleaf(node)) { + uint64_t val = mtbddnode_getvalue(node); + SHA256_Update(ctx, (void*)&val, sizeof(uint64_t)); + } else if (mtbddnode_getmark(node) == 0) { + mtbddnode_setmark(node, 1); + uint32_t level = mtbddnode_getvariable(node); + if (MTBDD_STRIPMARK(mtbddnode_gethigh(node))) level |= 0x80000000; + SHA256_Update(ctx, (void*)&level, sizeof(uint32_t)); + mtbdd_sha2_rec(mtbddnode_gethigh(node), ctx); + mtbdd_sha2_rec(mtbddnode_getlow(node), ctx); + } +} + +void +mtbdd_getsha(MTBDD mtbdd, char *target) +{ + SHA256_CTX ctx; + SHA256_Init(&ctx); + mtbdd_sha2_rec(mtbdd, &ctx); + if (mtbdd != sylvan_true && mtbdd != sylvan_false) mtbdd_unmark_rec(mtbdd); + SHA256_End(&ctx, target); +} + /** * Binary operation Times (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Integer or Double. diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h index 781f36800..38fa6668b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h @@ -1,3 +1,5 @@ +void mtbdd_getsha(MTBDD mtbdd, char *target); // target must be at least 65 bytes... + /** * Binary operation Divide (for MTBDDs of same type) * Only for MTBDDs where all leaves are Integer or Double. diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp index 7370e8b1d..26e5ea4be 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp @@ -48,4 +48,4 @@ */ void PrintDot(FILE *out) const; - \ No newline at end of file + std::string GetShaHash() const; diff --git a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp index c119f72cd..27706dcdd 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp @@ -131,3 +131,11 @@ void Mtbdd::PrintDot(FILE *out) const { mtbdd_fprintdot(out, mtbdd, NULL); } + +std::string +Mtbdd::GetShaHash() const { + char buf[65]; + mtbdd_getsha(mtbdd, buf); + return std::string(buf); +} + diff --git a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp index 221853a87..ad6ebff49 100644 --- a/src/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -61,7 +61,7 @@ namespace storm { ++iterations; } - + return xCopy; }