From 6bebb3c9d52d50290dab9cdc28c4b978476edf14 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 24 Aug 2017 11:00:19 +0200 Subject: [PATCH] fix bug in rational number/function handling with sylvan --- .../sylvan/src/sylvan_storm_rational_function.c | 4 ++-- .../sylvan/src/sylvan_storm_rational_number.c | 4 ++-- src/storm/solver/SymbolicLinearEquationSolver.cpp | 1 - .../storage/dd/bisimulation/QuotientExtractor.cpp | 12 ++++++++---- 4 files changed, 12 insertions(+), 9 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c index 4362077aa..5f21b9d11 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_function.c @@ -554,7 +554,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_threshold, MTBDD, a, size_t if (mtbdd_isleaf(a)) { storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); - return storm_rational_function_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; + return storm_rational_function_less(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; @@ -566,7 +566,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_function_op_strict_threshold, MTBDD, a, if (mtbdd_isleaf(a)) { storm_rational_function_ptr ma = mtbdd_getstorm_rational_function_ptr(a); - return storm_rational_function_less(ma, value) ? mtbdd_false : mtbdd_true; + return storm_rational_function_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; diff --git a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c index eb739693a..22f9ef053 100644 --- a/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c +++ b/resources/3rdparty/sylvan/src/sylvan_storm_rational_number.c @@ -588,7 +588,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_threshold, MTBDD, a, size_t*, if (mtbdd_isleaf(a)) { storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); - return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; + return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; @@ -600,7 +600,7 @@ TASK_IMPL_2(MTBDD, sylvan_storm_rational_number_op_strict_threshold, MTBDD, a, s if (mtbdd_isleaf(a)) { storm_rational_number_ptr ma = mtbdd_getstorm_rational_number_ptr(a); - return storm_rational_number_less(ma, value) ? mtbdd_false : mtbdd_true; + return storm_rational_number_less_or_equal(ma, value) ? mtbdd_false : mtbdd_true; } return mtbdd_invalid; diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 0a80a3afc..c6a75b6ce 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -59,7 +59,6 @@ namespace storm { } } - template std::unique_ptr> GeneralSymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 83201cfbe..feaeb4313 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -846,7 +846,6 @@ namespace storm { auto states = partition.getStates().swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Bdd partitionAsBdd = partition.storedAsAdd() ? partition.asAdd().toBdd() : partition.asBdd(); - partitionAsBdd.exportToDot("part.dot"); partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); auto start = std::chrono::high_resolution_clock::now(); @@ -968,13 +967,18 @@ namespace storm { STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); start = std::chrono::high_resolution_clock::now(); - storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsBdd.renameVariables(blockVariableSet, blockPrimeVariableSet).renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()); + std::set blockAndRowVariables; + std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end())); + std::set blockPrimeAndColumnVariables; + std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end())); + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockAndRowVariables, blockPrimeAndColumnVariables), model.getColumnVariables()); // Pick a representative from each block. auto representatives = InternalRepresentativeComputer(partitionAsBdd, model.getRowVariables()).getRepresentatives(); partitionAsBdd &= representatives; - storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); - + partitionAsAdd *= partitionAsBdd.template toAdd(); + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()); end = std::chrono::high_resolution_clock::now();