From cdf76b0c1567811a891c4f3a43182cacae99b7b0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 6 Aug 2017 15:17:55 +0200 Subject: [PATCH] fixed DD-based quotient extraction in bisimulation --- resources/3rdparty/CMakeLists.txt | 8 ++- src/storm/cli/cli.cpp | 1 + .../storage/dd/BisimulationDecomposition.cpp | 1 + .../dd/bisimulation/MdpPartitionRefiner.cpp | 3 +- .../storage/dd/bisimulation/Partition.cpp | 1 + .../dd/bisimulation/PartitionRefiner.cpp | 2 + .../bisimulation/PreservationInformation.cpp | 8 +-- .../dd/bisimulation/QuotientExtractor.cpp | 51 ++++++++----------- .../dd/bisimulation/SignatureComputer.cpp | 2 + .../dd/sylvan/InternalSylvanDdManager.cpp | 4 +- .../expressions/LinearityCheckVisitor.cpp | 2 +- .../expressions/ToRationalNumberVisitor.cpp | 2 + 12 files changed, 46 insertions(+), 39 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index bb70f53b5..15d46c381 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -418,12 +418,18 @@ else() set(sylvan_dep lib_carl) endif() +if (STORM_DEBUG_SYLVAN) + set(SYLVAN_BUILD_TYPE "Debug") +else() + set(SYLVAN_BUILD_TYPE "Release") +endif() + ExternalProject_Add( sylvan DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DGMP_LOCATION=${GMP_LIB_LOCATION} -DGMP_INCLUDE=${GMP_INCLUDE_DIR} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES} -DBUILD_SHARED_LIBS=OFF -DSYLVAN_BUILD_TESTS=OFF BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan BUILD_IN_SOURCE 0 INSTALL_COMMAND "" diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 5bab54a87..33826447f 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -514,6 +514,7 @@ namespace storm { result = preprocessDdModel(result.first->as>(), input); } + preprocessingWatch.stop(); if (result.second) { STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); } diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 77aa64f1d..e34a7ddf8 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -7,6 +7,7 @@ #include "storm/models/symbolic/Model.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index 914656d89..d26cc4111 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -1,6 +1,7 @@ #include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" namespace storm { namespace dd { @@ -9,8 +10,6 @@ namespace storm { template MdpPartitionRefiner::MdpPartitionRefiner(storm::models::symbolic::Mdp const& mdp, Partition const& initialStatePartition) : PartitionRefiner(mdp, initialStatePartition), choicePartition(Partition::createTrivialChoicePartition(mdp, initialStatePartition.getBlockVariables())), stateSignatureComputer(mdp.getQualitativeTransitionMatrix(), mdp.getColumnAndNondeterminismVariables(), SignatureMode::Qualitative, true), stateSignatureRefiner(mdp.getManager(), this->statePartition.getBlockVariable(), mdp.getRowVariables()) { // Intentionally left empty. - - mdp.getTransitionMatrix().exportToDot("fulltrans.dot"); } template diff --git a/src/storm/storage/dd/bisimulation/Partition.cpp b/src/storm/storage/dd/bisimulation/Partition.cpp index bde87a5b9..fb64f9381 100644 --- a/src/storm/storage/dd/bisimulation/Partition.cpp +++ b/src/storm/storage/dd/bisimulation/Partition.cpp @@ -9,6 +9,7 @@ #include "storm/logic/AtomicLabelFormula.h" #include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BisimulationSettings.h" diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index 74a563363..cd064343f 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -1,5 +1,7 @@ #include "storm/storage/dd/bisimulation/PartitionRefiner.h" +#include "storm/models/symbolic/StandardRewardModel.h" + namespace storm { namespace dd { namespace bisimulation { diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp index 363e88fdd..5009fa371 100644 --- a/src/storm/storage/dd/bisimulation/PreservationInformation.cpp +++ b/src/storm/storage/dd/bisimulation/PreservationInformation.cpp @@ -2,6 +2,8 @@ #include "storm/logic/Formulas.h" +#include "storm/models/symbolic/StandardRewardModel.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -15,7 +17,7 @@ namespace storm { } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const& bisimulationType) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& labels, storm::storage::BisimulationType const&) { for (auto const& label : labels) { this->addLabel(label); this->addExpression(model.getExpression(label)); @@ -23,14 +25,14 @@ namespace storm { } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const& bisimulationType) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector const& expressions, storm::storage::BisimulationType const&) { for (auto const& e : expressions) { this->addExpression(e); } } template - PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) { + PreservationInformation::PreservationInformation(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const&) { if (formulas.empty()) { // Default to respect all labels if no formulas are given. for (auto const& label : model.getLabels()) { diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 3027badf0..32b9363b2 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -551,9 +551,6 @@ namespace storm { // Sanity checks. STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size."); - partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).exportToDot("partstates.dot"); - model.getReachableStates().exportToDot("origstates.dot"); - std::cout << "equal? " << (partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()).template toAdd().notZero() == model.getReachableStates().template toAdd().notZero()) << std::endl; STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition."); std::set blockVariableSet = {partition.getBlockVariable()}; @@ -567,36 +564,10 @@ namespace storm { partitionAsBdd = (representativePartition && partitionAsBddOverPrimedBlockVariable).existsAbstract(blockPrimeVariableSet); } - storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); - partitionAsAdd.exportToDot("partition.dot"); - model.getTransitionMatrix().sumAbstract(model.getColumnVariables()).exportToDot("origdist.dot"); auto start = std::chrono::high_resolution_clock::now(); - storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); - STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(model.getTransitionMatrix().sumAbstract(model.getColumnVariables()), ValueType(1e-6)), "Expected something else."); - quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).exportToDot("sanity.dot"); - quotientTransitionMatrix.exportToDot("trans-1.dot"); - partitionAsAdd = partitionAsAdd / partitionAsAdd.sumAbstract(model.getColumnVariables()); - quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables()); - quotientTransitionMatrix.exportToDot("quottrans.dot"); - auto partCount = partitionAsAdd.sumAbstract(model.getColumnVariables()); - partCount.exportToDot("partcount.dot"); - auto end = std::chrono::high_resolution_clock::now(); - - // Check quotient matrix for sanity. - auto quotdist = quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet); - quotdist.exportToDot("quotdists.dot"); - (quotdist / partCount).exportToDot("distcount.dot"); - STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); - STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), ValueType(1e-6)), "Illegal non-probabilistic matrix."); - - STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); - storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); - - start = std::chrono::high_resolution_clock::now(); storm::dd::Bdd partitionAsBddOverRowVariables = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables()); storm::dd::Bdd reachableStates = partitionAsBdd.existsAbstract(model.getColumnVariables()); storm::dd::Bdd initialStates = (model.getInitialStates() && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables()); - storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; std::map> preservedLabelBdds; for (auto const& label : preservationInformation.getLabels()) { @@ -614,9 +585,29 @@ namespace storm { preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBddOverRowVariables).existsAbstract(model.getRowVariables())); } } - end = std::chrono::high_resolution_clock::now(); + auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Quotient labels extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + storm::dd::Add partitionAsAdd = partitionAsBdd.template toAdd(); + start = std::chrono::high_resolution_clock::now(); + storm::dd::Add quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(blockVariableSet, blockPrimeVariableSet), model.getColumnVariables()); + + // Pick a representative from each block. + partitionAsBdd = partitionAsBdd.existsAbstractRepresentative(model.getColumnVariables()); + partitionAsAdd = partitionAsBdd.template toAdd(); + + quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd.renameVariables(model.getColumnVariables(), model.getRowVariables()), model.getRowVariables()); + end = std::chrono::high_resolution_clock::now(); + + // Check quotient matrix for sanity. + STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one()).isZero(), "Illegal entries in quotient matrix."); + STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd(), ValueType(1e-6)), "Illegal non-probabilistic matrix."); + + STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast(end - start).count() << "ms."); + + storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); + storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; + if (modelType == storm::models::ModelType::Dtmc) { return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); } else if (modelType == storm::models::ModelType::Ctmc) { diff --git a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp index 682085468..b4336adc8 100644 --- a/src/storm/storage/dd/bisimulation/SignatureComputer.cpp +++ b/src/storm/storage/dd/bisimulation/SignatureComputer.cpp @@ -2,6 +2,8 @@ #include "storm/storage/dd/DdManager.h" +#include "storm/models/symbolic/StandardRewardModel.h" + #include "storm/utility/macros.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp index 11c7b09d6..4586e9890 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -67,8 +67,8 @@ namespace storm { maxTableSize >>= 1; } - uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, 16ull); - uint64_t initialCacheSize = 1ull << std::max(powerOfTwo - 4, 16ull); + uint64_t initialTableSize = 1ull << std::max(powerOfTwo - 4, static_cast(16)); + uint64_t initialCacheSize = initialTableSize; STORM_LOG_DEBUG("Initializing sylvan. Initial/max table size: " << initialTableSize << "/" << maxTableSize << ", initial/max cache size: " << initialCacheSize << "/" << maxCacheSize << "."); sylvan::Sylvan::initPackage(initialTableSize, maxTableSize, initialCacheSize, maxCacheSize); diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp index 18198ca0e..9eeb3ea56 100644 --- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp +++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp @@ -125,7 +125,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator."); } - boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) { + boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const& data) { bool booleanIsLinear = boost::any_cast(data); if (booleanIsLinear) { diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp index f7aa3236d..15a8d61eb 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp @@ -119,6 +119,8 @@ namespace storm { return result; break; } + // Dummy return. + return result; } template