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

Merge remote-tracking branch 'origin/master' into sound-vi

tempestpy_adaptions
TimQu 7 years ago
parent
c1ecc22303 66e08f9cd7
commit
f6c504214a
19 changed files with 341 additions and 46 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. 6
      CMakeLists.txt
  2. 6
      src/storm/settings/modules/BisimulationSettings.cpp
  3. 8
      src/storm/settings/modules/BisimulationSettings.h
  4. 2
      src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
  5. 40
      src/storm/storage/dd/Add.cpp
  6. 14
      src/storm/storage/dd/Add.h
  7. 40
      src/storm/storage/dd/Bdd.cpp
  8. 13
      src/storm/storage/dd/Bdd.h
  9. 47
      src/storm/storage/dd/BisimulationDecomposition.cpp
  10. 2
      src/storm/storage/dd/BisimulationDecomposition.h
  11. 10
      src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
  12. 10
      src/storm/storage/dd/bisimulation/Partition.cpp
  13. 24
      src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
  14. 3
      src/storm/storage/dd/bisimulation/PartitionRefiner.h
  15. 131
      src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
  16. 4
      src/storm/storage/dd/bisimulation/QuotientExtractor.h
  17. 2
      src/storm/storage/dd/sylvan/InternalSylvanAdd.h
  18. 2
      src/storm/utility/dd.cpp
  19. 23
      src/test/storm/storage/CuddDdTest.cpp

6
CMakeLists.txt
View File

@ -181,9 +181,15 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
set(STORM_COMPILER_ID "AppleClang")
set(CMAKE_MACOSX_RPATH ON)
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
set(GCC ON)
# using GCC
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0)
message(FATAL_ERROR "gcc version must be at least 5.0.")
elseif (CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 7.0 OR CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 7.0)
if (STORM_USE_LTO)
set(STORM_USE_LTO OFF)
message(WARNING "Disabling link-time optimization, because of known incompatibility of LTO with gcc >= 7.")
endif()
endif()
set(STORM_COMPILER_GCC ON)

6
src/storm/settings/modules/BisimulationSettings.cpp
View File

@ -15,6 +15,7 @@ namespace storm {
const std::string BisimulationSettings::moduleName = "bisimulation";
const std::string BisimulationSettings::typeOptionName = "type";
const std::string BisimulationSettings::representativeOptionName = "repr";
const std::string BisimulationSettings::originalVariablesOptionName = "origvars";
const std::string BisimulationSettings::quotientFormatOptionName = "quot";
const std::string BisimulationSettings::signatureModeOptionName = "sigmode";
const std::string BisimulationSettings::reuseOptionName = "reuse";
@ -29,6 +30,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, quotientFormatOptionName, true, "Sets the format in which the quotient is extracted (only applies to DD-based bisimulation).").addArgument(storm::settings::ArgumentBuilder::createStringArgument("format", "The format of the quotient.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(quotTypes)).setDefaultValueString("dd").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, representativeOptionName, false, "Sets whether to use representatives in the quotient rather than block numbers.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, originalVariablesOptionName, false, "Sets whether to use the original variables in the quotient rather than the block variables.").build());
std::vector<std::string> signatureModes = { "eager", "lazy" };
this->addOption(storm::settings::OptionBuilder(moduleName, signatureModeOptionName, false, "Sets the signature computation mode.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(signatureModes)).setDefaultValueString("eager").build()).build());
@ -78,6 +80,10 @@ namespace storm {
return this->getOption(representativeOptionName).getHasOptionBeenSet();
}
bool BisimulationSettings::isUseOriginalVariablesSet() const {
return this->getOption(originalVariablesOptionName).getHasOptionBeenSet();
}
storm::dd::bisimulation::SignatureMode BisimulationSettings::getSignatureMode() const {
std::string modeAsString = this->getOption(signatureModeOptionName).getArgumentByName("mode").getValueAsString();
if (modeAsString == "eager") {

8
src/storm/settings/modules/BisimulationSettings.h
View File

@ -56,6 +56,13 @@ namespace storm {
*/
bool isUseRepresentativesSet() const;
/*!
* Retrieves whether the extracted quotient model is supposed to use the same variables as the original
* model.
* NOTE: only applies to DD-based bisimulation.
*/
bool isUseOriginalVariablesSet() const;
/*!
* Retrieves the mode to compute signatures.
*/
@ -85,6 +92,7 @@ namespace storm {
// Define the string names of the options as constants.
static const std::string typeOptionName;
static const std::string representativeOptionName;
static const std::string originalVariablesOptionName;
static const std::string quotientFormatOptionName;
static const std::string signatureModeOptionName;
static const std::string reuseOptionName;

2
src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
View File

@ -88,7 +88,7 @@ namespace storm {
storm::dd::Add<DdType, ValueType> lu = diagonal.ite(manager.template getAddZero<ValueType>(), this->A);
storm::dd::Add<DdType, ValueType> diagonalAdd = diagonal.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
storm::dd::Add<DdType, ValueType> scaledB = b / diag;

40
src/storm/storage/dd/Add.cpp
View File

@ -231,6 +231,46 @@ namespace storm {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const {
std::vector<InternalBdd<LibraryType>> fromBdds;
std::vector<InternalBdd<LibraryType>> toBdds;
for (auto const& metaVariable : from) {
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
fromBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
for (auto const& metaVariable : to) {
STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
toBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::set<storm::expressions::Variable> newContainedMetaVariables = to;
std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin()));
STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes.");
if (fromBdds.size() == toBdds.size()) {
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.permuteVariables(fromBdds, toBdds), newContainedMetaVariables);
} else {
InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd();
for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) {
cube &= fromBdds[index];
}
fromBdds.resize(toBdds.size());
return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.sumAbstract(cube).permuteVariables(fromBdds, toBdds), newContainedMetaVariables);
}
}
template<DdType LibraryType, typename ValueType>
Add<LibraryType, ValueType> Add<LibraryType, ValueType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
std::set<storm::expressions::Variable> newContainedMetaVariables;

14
src/storm/storage/dd/Add.h
View File

@ -331,6 +331,20 @@ namespace storm {
*/
Add<LibraryType, ValueType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Renames the given meta variables in the ADD. The number of the underlying DD variables of the from meta
* variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide,
* this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables
* and then performs the renaming.
*
* @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables.
* @param to The meta variables that are the target of the renaming process. The current ADD must not contain
* any of these meta variables.
* @return The resulting ADD.
*/
Add<LibraryType, ValueType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Swaps the given pairs of meta variables in the ADD. The pairs of meta variables must be guaranteed to have
* the same number of underlying ADD variables.

40
src/storm/storage/dd/Bdd.cpp
View File

@ -319,6 +319,46 @@ namespace storm {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
}
template<DdType LibraryType>
Bdd<LibraryType> Bdd<LibraryType>::renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const {
std::vector<InternalBdd<LibraryType>> fromBdds;
std::vector<InternalBdd<LibraryType>> toBdds;
for (auto const& metaVariable : from) {
STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename variable '" << metaVariable.getName() << "' that is not present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
fromBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(fromBdds.begin(), fromBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
for (auto const& metaVariable : to) {
STORM_LOG_THROW(!this->containsMetaVariable(metaVariable), storm::exceptions::InvalidOperationException, "Cannot rename to variable '" << metaVariable.getName() << "' that is already present.");
DdMetaVariable<LibraryType> const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
toBdds.push_back(ddVariable.getInternalBdd());
}
}
std::sort(toBdds.begin(), toBdds.end(), [] (InternalBdd<LibraryType> const& a, InternalBdd<LibraryType> const& b) { return a.getLevel() < b.getLevel(); } );
std::set<storm::expressions::Variable> newContainedMetaVariables = to;
std::set_difference(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), from.begin(), from.end(), std::inserter(newContainedMetaVariables, newContainedMetaVariables.begin()));
STORM_LOG_ASSERT(fromBdds.size() >= toBdds.size(), "Unable to perform rename-abstract with mismatching sizes.");
if (fromBdds.size() == toBdds.size()) {
return Bdd<LibraryType>(this->getDdManager(), internalBdd.swapVariables(fromBdds, toBdds), newContainedMetaVariables);
} else {
InternalBdd<LibraryType> cube = this->getDdManager().getBddOne().getInternalBdd();
for (uint64_t index = toBdds.size(); index < fromBdds.size(); ++index) {
cube &= fromBdds[index];
}
fromBdds.resize(toBdds.size());
return Bdd<LibraryType>(this->getDdManager(), internalBdd.existsAbstract(cube).swapVariables(fromBdds, toBdds), newContainedMetaVariables);
}
}
template<DdType LibraryType>
template<typename ValueType>
Add<LibraryType, ValueType> Bdd<LibraryType>::toAdd() const {

13
src/storm/storage/dd/Bdd.h
View File

@ -285,6 +285,19 @@ namespace storm {
*/
Bdd<LibraryType> renameVariables(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Renames the given meta variables in the BDD. The number of the underlying DD variables of the from meta
* variable set needs to be at least as large as the to meta variable set. If the amount of variables coincide,
* this operation coincides with renameVariables. Otherwise, it first abstracts from the superfluous variables
* and then performs the renaming.
*
* @param from The meta variables to be renamed. The current ADD needs to contain all these meta variables.
* @param to The meta variables that are the target of the renaming process. The current ADD must not contain
* any of these meta variables.
* @return The resulting ADD.
*/
Bdd<LibraryType> renameVariablesAbstract(std::set<storm::expressions::Variable> const& from, std::set<storm::expressions::Variable> const& to) const;
/*!
* Retrieves whether this DD represents the constant one function.
*

47
src/storm/storage/dd/BisimulationDecomposition.cpp
View File

@ -57,14 +57,16 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void BisimulationDecomposition<DdType, ValueType>::initialize() {
auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
showProgress = generalSettings.isVerboseSet();
verboseProgress = generalSettings.isVerboseSet();
showProgressDelay = generalSettings.getShowProgressDelay();
auto start = std::chrono::high_resolution_clock::now();
this->refineWrtRewardModels();
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Refining with respect to reward models took " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
#ifndef NDEBUG
STORM_LOG_INFO("Initial partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
STORM_LOG_TRACE("Initial partition has " << refiner->getStatePartition().getNodeCount() << " nodes.");
#endif
}
template <storm::dd::DdType DdType, typename ValueType>
@ -80,21 +82,18 @@ namespace storm {
refined = refiner->refine(mode);
++iterations;
STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
if (showProgress) {
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "s) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
timeOfLastMessage = std::chrono::high_resolution_clock::now();
}
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::milliseconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay * 1000 || verboseProgress) {
auto durationSinceStart = std::chrono::duration_cast<std::chrono::milliseconds>(now - start).count();
STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
timeOfLastMessage = std::chrono::high_resolution_clock::now();
}
}
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations).");
STORM_LOG_INFO("Partition refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms (" << iterations << " iterations, signature: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalSignatureTime()).count() << "ms, refinement: " << std::chrono::duration_cast<std::chrono::milliseconds>(refiner->getTotalRefinementTime()).count() << "ms).");
}
template <storm::dd::DdType DdType, typename ValueType>
@ -112,14 +111,12 @@ namespace storm {
++iterations;
if (showProgress) {
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay) {
auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
timeOfLastMessage = std::chrono::high_resolution_clock::now();
}
auto now = std::chrono::high_resolution_clock::now();
auto durationSinceLastMessage = std::chrono::duration_cast<std::chrono::seconds>(now - timeOfLastMessage).count();
if (static_cast<uint64_t>(durationSinceLastMessage) >= showProgressDelay || verboseProgress) {
auto durationSinceStart = std::chrono::duration_cast<std::chrono::seconds>(now - start).count();
STORM_LOG_INFO("State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks.");
timeOfLastMessage = std::chrono::high_resolution_clock::now();
}
}
@ -135,13 +132,13 @@ namespace storm {
std::shared_ptr<storm::models::Model<ValueType>> BisimulationDecomposition<DdType, ValueType>::getQuotient() const {
std::shared_ptr<storm::models::Model<ValueType>> quotient;
if (this->refiner->getStatus() == Status::FixedPoint) {
STORM_LOG_TRACE("Starting full quotient extraction.");
STORM_LOG_INFO("Starting full quotient extraction.");
QuotientExtractor<DdType, ValueType> extractor;
quotient = extractor.extract(model, refiner->getStatePartition(), preservationInformation);
} else {
STORM_LOG_THROW(model.getType() == storm::models::ModelType::Dtmc || model.getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidOperationException, "Can only extract partial quotient for discrete-time models.");
STORM_LOG_TRACE("Starting partial quotient extraction.");
STORM_LOG_INFO("Starting partial quotient extraction.");
if (!partialQuotientExtractor) {
partialQuotientExtractor = std::make_unique<bisimulation::PartialQuotientExtractor<DdType, ValueType>>(model);
}
@ -149,7 +146,7 @@ namespace storm {
quotient = partialQuotientExtractor->extract(refiner->getStatePartition(), preservationInformation);
}
STORM_LOG_TRACE("Quotient extraction done.");
STORM_LOG_INFO("Quotient extraction done.");
return quotient;
}

2
src/storm/storage/dd/BisimulationDecomposition.h
View File

@ -83,7 +83,7 @@ namespace storm {
mutable std::unique_ptr<bisimulation::PartialQuotientExtractor<DdType, ValueType>> partialQuotientExtractor;
// A flag indicating whether progress is reported.
bool showProgress;
bool verboseProgress;
// The delay between progress reports.
uint64_t showProgressDelay;

10
src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
View File

@ -42,12 +42,22 @@ namespace storm {
} else {
choicePartitionAsBdd = this->choicePartition.asAdd().notZero();
}
auto signatureStart = std::chrono::high_resolution_clock::now();
Signature<DdType, ValueType> stateSignature(choicePartitionAsBdd.existsAbstract(model.getNondeterminismVariables()).template toAdd<ValueType>());
auto signatureEnd = std::chrono::high_resolution_clock::now();
this->totalSignatureTime += (signatureEnd - signatureStart);
// If the choice partition changed, refine the state partition.
STORM_LOG_TRACE("Refining state partition.");
auto refinementStart = std::chrono::high_resolution_clock::now();
Partition<DdType, ValueType> newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition);
auto refinementEnd = std::chrono::high_resolution_clock::now();
auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
auto refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
STORM_LOG_INFO("Refinement " << (this->refinements-1) << " produced " << newStatePartition.getNumberOfBlocks() << " blocks and was completed in " << (signatureTime + refinementTime) << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
if (newStatePartition == this->statePartition) {
this->status = Status::FixedPoint;
return false;

10
src/storm/storage/dd/bisimulation/Partition.cpp
View File

@ -130,6 +130,8 @@ namespace storm {
std::pair<storm::expressions::Variable, storm::expressions::Variable> blockVariables = createBlockVariables(model);
auto start = std::chrono::high_resolution_clock::now();
// Set up the construction.
storm::dd::DdManager<DdType>& manager = model.getManager();
storm::dd::Bdd<DdType> partitionBdd = manager.getBddZero();
@ -153,6 +155,9 @@ namespace storm {
// Move the partition over to the primed variables.
partitionBdd = partitionBdd.swapVariables(model.getRowColumnMetaVariablePairs());
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Created distance and label-based initial partition in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
// Store the partition as an ADD only in the case of CUDD.
if (DdType == storm::dd::DdType::CUDD) {
return Partition<DdType, ValueType>(partitionBdd.template toAdd<ValueType>(), blockVariables, blockCount, blockCount);
@ -191,8 +196,11 @@ namespace storm {
for (auto const& expression : expressions) {
stateSets.emplace_back(model.getStates(expression));
}
auto start = std::chrono::high_resolution_clock::now();
std::pair<storm::dd::Bdd<DdType>, uint64_t> partitionBddAndBlockCount = createPartitionBdd(model.getManager(), model, stateSets, blockVariables.first);
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Created label-based initial partition in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
// Store the partition as an ADD only in the case of CUDD.
if (DdType == storm::dd::DdType::CUDD) {
return Partition<DdType, ValueType>(partitionBddAndBlockCount.first.template toAdd<ValueType>(), blockVariables, partitionBddAndBlockCount.second, partitionBddAndBlockCount.second);

24
src/storm/storage/dd/bisimulation/PartitionRefiner.cpp
View File

@ -12,7 +12,7 @@ namespace storm {
namespace bisimulation {
template <storm::dd::DdType DdType, typename ValueType>
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()) {
PartitionRefiner<DdType, ValueType>::PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : status(Status::Initialized), refinements(0), statePartition(initialStatePartition), signatureComputer(model), signatureRefiner(model.getManager(), statePartition.getBlockVariable(), model.getRowAndNondeterminismVariables(), model.getColumnVariables(), !model.isNondeterministicModel(), model.getNondeterminismVariables()), totalSignatureTime(0), totalRefinementTime(0) {
// Intentionally left empty.
}
@ -50,7 +50,7 @@ namespace storm {
auto signatureEnd = std::chrono::high_resolution_clock::now();
totalSignatureTime += (signatureEnd - signatureStart);
STORM_LOG_TRACE("Signature " << refinements << "[" << index << "] DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
auto refinementStart = std::chrono::high_resolution_clock::now();
newPartition = signatureRefiner.refine(oldPartition, signature);
auto refinementEnd = std::chrono::high_resolution_clock::now();
@ -66,7 +66,7 @@ namespace storm {
}
auto totalTimeInRefinement = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - start).count();
STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
STORM_LOG_INFO("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms (signature: " << signatureTime << "ms, refinement: " << refinementTime << "ms).");
++refinements;
return newPartition;
} else {
@ -78,11 +78,11 @@ namespace storm {
Partition<DdType, ValueType> PartitionRefiner<DdType, ValueType>::internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition) {
STORM_LOG_TRACE("Signature " << refinements << " DD has " << signature.getSignatureAdd().getNodeCount() << " nodes.");
auto start = std::chrono::high_resolution_clock::now();
auto refinementStart = std::chrono::high_resolution_clock::now();
auto newPartition = signatureRefiner.refine(oldPartition, signature);
auto totalTimeInRefinement = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::high_resolution_clock::now() - start).count();
STORM_LOG_TRACE("Refinement " << refinements << " produced " << newPartition.getNumberOfBlocks() << " blocks and was completed in " << totalTimeInRefinement << "ms.");
auto refinementEnd = std::chrono::high_resolution_clock::now();
totalRefinementTime += (refinementEnd - refinementStart);
++refinements;
return newPartition;
}
@ -135,6 +135,16 @@ namespace storm {
return status;
}
template <storm::dd::DdType DdType, typename ValueType>
std::chrono::high_resolution_clock::duration PartitionRefiner<DdType, ValueType>::getTotalSignatureTime() const {
return totalSignatureTime;
}
template <storm::dd::DdType DdType, typename ValueType>
std::chrono::high_resolution_clock::duration PartitionRefiner<DdType, ValueType>::getTotalRefinementTime() const {
return totalRefinementTime;
}
template class PartitionRefiner<storm::dd::DdType::CUDD, double>;
template class PartitionRefiner<storm::dd::DdType::Sylvan, double>;

3
src/storm/storage/dd/bisimulation/PartitionRefiner.h
View File

@ -53,6 +53,9 @@ namespace storm {
*/
Status getStatus() const;
std::chrono::high_resolution_clock::duration getTotalSignatureTime() const;
std::chrono::high_resolution_clock::duration getTotalRefinementTime() const;
protected:
Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
Partition<DdType, ValueType> internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition);

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

@ -821,6 +821,7 @@ namespace storm {
QuotientExtractor<DdType, ValueType>::QuotientExtractor() : useRepresentatives(false) {
auto const& settings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
this->useRepresentatives = settings.isUseRepresentativesSet();
this->useOriginalVariables = settings.isUseOriginalVariablesSet();
this->quotientFormat = settings.getQuotientFormat();
}
@ -834,7 +835,7 @@ namespace storm {
result = extractDdQuotient(model, partition, preservationInformation);
}
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_INFO("Quotient extraction completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "Quotient could not be extracted.");
@ -855,7 +856,7 @@ namespace storm {
InternalSparseQuotientExtractor<DdType, ValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), partition.getNumberOfBlocks(), representatives);
storm::storage::SparseMatrix<ValueType> quotientTransitionMatrix = sparseExtractor.extractTransitionMatrix(model.getTransitionMatrix());
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.");
STORM_LOG_INFO("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());
@ -877,7 +878,7 @@ namespace storm {
}
}
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.");
STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now();
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> quotientRewardModels;
@ -897,7 +898,7 @@ namespace storm {
quotientRewardModels.emplace(rewardModelName, storm::models::sparse::StandardRewardModel<ValueType>(std::move(quotientStateRewards), std::move(quotientStateActionRewards), boost::none));
}
end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_INFO("Reward models 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) {
@ -921,7 +922,12 @@ namespace storm {
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
return extractQuotientUsingBlockVariables(model, partition, preservationInformation);
if (this->useOriginalVariables) {
return extractQuotientUsingOriginalVariables(model, partition, preservationInformation);
} else {
return extractQuotientUsingBlockVariables(model, partition, preservationInformation);
}
}
template<storm::dd::DdType DdType, typename ValueType>
@ -972,7 +978,7 @@ namespace storm {
}
}
auto 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.");
STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now();
std::set<storm::expressions::Variable> blockAndRowVariables;
@ -998,7 +1004,7 @@ namespace storm {
}
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(blockPrimeVariableSet).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(blockPrimeVariableSet).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal non-probabilistic matrix.");
STORM_LOG_TRACE("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
@ -1021,7 +1027,7 @@ namespace storm {
quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
}
end = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels));
@ -1036,6 +1042,115 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
}
}
template<storm::dd::DdType DdType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> QuotientExtractor<DdType, ValueType>::extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation) {
auto modelType = model.getType();
if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::MarkovAutomaton) {
STORM_LOG_WARN_COND(!this->useRepresentatives, "Using representatives is unsupported for this extraction, falling back to regular extraction.");
// Sanity checks.
STORM_LOG_ASSERT(partition.getNumberOfStates() == model.getNumberOfStates(), "Mismatching partition size.");
STORM_LOG_ASSERT(partition.getStates().renameVariables(model.getColumnVariables(), model.getRowVariables()) == model.getReachableStates(), "Mismatching partition.");
std::set<storm::expressions::Variable> blockVariableSet = {partition.getBlockVariable()};
std::set<storm::expressions::Variable> blockPrimeVariableSet = {partition.getPrimedBlockVariable()};
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> blockMetaVariablePairs = {std::make_pair(partition.getBlockVariable(), partition.getPrimedBlockVariable())};
storm::dd::Bdd<DdType> partitionAsBdd = partition.storedAsBdd() ? partition.asBdd() : partition.asAdd().notZero();
auto start = std::chrono::high_resolution_clock::now();
partitionAsBdd = partitionAsBdd.renameVariables(model.getColumnVariables(), model.getRowVariables());
storm::dd::Bdd<DdType> reachableStates = partitionAsBdd.existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
storm::dd::Bdd<DdType> initialStates = (model.getInitialStates() && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
std::map<std::string, storm::dd::Bdd<DdType>> preservedLabelBdds;
for (auto const& label : preservationInformation.getLabels()) {
preservedLabelBdds.emplace(label, (model.getStates(label) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()));
}
for (auto const& expression : preservationInformation.getExpressions()) {
std::stringstream stream;
stream << expression;
std::string expressionAsString = stream.str();
auto it = preservedLabelBdds.find(expressionAsString);
if (it != preservedLabelBdds.end()) {
STORM_LOG_WARN("Duplicate label '" << expressionAsString << "', dropping second label definition.");
} else {
preservedLabelBdds.emplace(stream.str(), (model.getStates(expression) && partitionAsBdd).existsAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables()));
}
}
auto end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Quotient labels extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
start = std::chrono::high_resolution_clock::now();
std::set<storm::expressions::Variable> blockAndRowVariables;
std::set_union(blockVariableSet.begin(), blockVariableSet.end(), model.getRowVariables().begin(), model.getRowVariables().end(), std::inserter(blockAndRowVariables, blockAndRowVariables.end()));
std::set<storm::expressions::Variable> blockPrimeAndColumnVariables;
std::set_union(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end(), model.getColumnVariables().begin(), model.getColumnVariables().end(), std::inserter(blockPrimeAndColumnVariables, blockPrimeAndColumnVariables.end()));
storm::dd::Add<DdType, ValueType> partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
storm::dd::Add<DdType, ValueType> quotientTransitionMatrix = model.getTransitionMatrix().multiplyMatrix(partitionAsAdd.renameVariables(model.getRowVariables(), model.getColumnVariables()), model.getColumnVariables()).renameVariablesAbstract(blockVariableSet, model.getColumnVariables());
// Pick a representative from each block.
auto representatives = InternalRepresentativeComputer<DdType>(partitionAsBdd, model.getRowVariables()).getRepresentatives();
partitionAsBdd &= representatives;
partitionAsAdd = partitionAsBdd.template toAdd<ValueType>();
// Workaround for problem with CUDD. Matrix-Matrix multiplication yields other result than multiplication+sum-abstract...
if (DdType == storm::dd::DdType::CUDD) {
quotientTransitionMatrix = (quotientTransitionMatrix * partitionAsAdd).sumAbstract(model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
} else {
quotientTransitionMatrix = quotientTransitionMatrix.multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
}
end = std::chrono::high_resolution_clock::now();
// Check quotient matrix for sanity.
if (std::is_same<ValueType, storm::RationalNumber>::value) {
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>()).isZero(), "Illegal entries in quotient matrix.");
} else {
STORM_LOG_ASSERT(quotientTransitionMatrix.greater(storm::utility::one<ValueType>() + storm::utility::convertNumber<ValueType>(1e-6)).isZero(), "Illegal entries in quotient matrix.");
}
STORM_LOG_ASSERT(quotientTransitionMatrix.sumAbstract(model.getColumnVariables()).equalModuloPrecision(quotientTransitionMatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd<ValueType>(), storm::utility::convertNumber<ValueType>(1e-6)), "Illegal probabilistic matrix.");
STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates;
start = std::chrono::high_resolution_clock::now();
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<DdType, ValueType>> quotientRewardModels;
for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) {
auto const& rewardModel = model.getRewardModel(rewardModelName);
boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateRewards;
if (rewardModel.hasStateRewards()) {
quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
}
boost::optional<storm::dd::Add<DdType, ValueType>> quotientStateActionRewards;
if (rewardModel.hasStateActionRewards()) {
quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()).renameVariablesAbstract(blockVariableSet, model.getRowVariables());
}
quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel<DdType, ValueType>(quotientStateRewards, quotientStateActionRewards, boost::none));
}
end = std::chrono::high_resolution_clock::now();
STORM_LOG_INFO("Reward models extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
if (modelType == storm::models::ModelType::Dtmc) {
return std::shared_ptr<storm::models::symbolic::Dtmc<DdType, ValueType>>(new storm::models::symbolic::Dtmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Ctmc) {
return std::shared_ptr<storm::models::symbolic::Ctmc<DdType, ValueType>>(new storm::models::symbolic::Ctmc<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), preservedLabelBdds, quotientRewardModels));
} else if (modelType == storm::models::ModelType::Mdp) {
return std::shared_ptr<storm::models::symbolic::Mdp<DdType, ValueType>>(new storm::models::symbolic::Mdp<DdType, ValueType>(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
} else {
return std::shared_ptr<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>(new storm::models::symbolic::MarkovAutomaton<DdType, ValueType>(model.getManager().asSharedPointer(), model. template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getMarkovianMarker(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs(), model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels));
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot extract quotient for this model type.");
}
}
template class QuotientExtractor<storm::dd::DdType::CUDD, double>;

4
src/storm/storage/dd/bisimulation/QuotientExtractor.h
View File

@ -28,8 +28,10 @@ namespace storm {
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractDdQuotient(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingBlockVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> extractQuotientUsingOriginalVariables(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& partition, PreservationInformation<DdType, ValueType> const& preservationInformation);
bool useRepresentatives;
bool useOriginalVariables;
storm::settings::modules::BisimulationSettings::QuotientFormat quotientFormat;
};

2
src/storm/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -319,7 +319,7 @@ namespace storm {
* @return The resulting ADD.
*/
InternalAdd<DdType::Sylvan, ValueType> swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const;
/*!
* Permutes the given pairs of DD variables in the ADD. The pairs of meta variables have to be represented by
* ADDs must have equal length.

2
src/storm/utility/dd.cpp
View File

@ -47,7 +47,7 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Bdd<Type> getRowColumnDiagonal(storm::dd::DdManager<Type> const& ddManager, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs) {
return ddManager.getIdentity(rowColumnMetaVariablePairs);
return ddManager.getIdentity(rowColumnMetaVariablePairs, false);
}
template storm::dd::Bdd<storm::dd::DdType::CUDD> computeReachableStates(storm::dd::Bdd<storm::dd::DdType::CUDD> const& initialStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables);

23
src/test/storm/storage/CuddDdTest.cpp
View File

@ -589,6 +589,29 @@ TEST(CuddDd, MultiplyMatrixTest) {
EXPECT_TRUE(dd3 == dd2 * manager->template getConstant<double>(2));
}
TEST(CuddDd, MultiplyMatrixTest2) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 0, 2);
std::pair<storm::expressions::Variable, storm::expressions::Variable> b = manager->addMetaVariable("b", 0, 2);
storm::dd::Add<storm::dd::DdType::CUDD, double> p = manager->getAddZero<double>();
p += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(b.first, 0, true)).template toAdd<double>();
p += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(b.first, 2, true)).template toAdd<double>();
storm::dd::Add<storm::dd::DdType::CUDD, double> q = manager->getAddZero<double>();
q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(0.3);
q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(0.3);
q += (manager->getEncoding(x.first, 0, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() * manager->template getConstant<double>(0.7);
q += (manager->getEncoding(x.first, 1, true) && manager->getEncoding(x.second, 2, true)).template toAdd<double>() * manager->template getConstant<double>(0.7);
q += (manager->getEncoding(x.first, 2, true) && manager->getEncoding(x.second, 0, true)).template toAdd<double>() * manager->template getConstant<double>(1);
storm::dd::Add<storm::dd::DdType::CUDD, double> r = q.multiplyMatrix(p, {x.first});
ASSERT_EQ(12ull, r.getNodeCount());
ASSERT_EQ(4ull, r.getLeafCount());
ASSERT_EQ(3ull, r.getNonZeroCount());
}
TEST(CuddDd, GetSetValueTest) {
std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);

Write Preview
Loading…
Cancel
Save