diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index bcbf8cdfa..47a7857d4 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -110,17 +110,17 @@ namespace storm { } \ } - template + template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::shared_ptr model = buildSymbolicModel(program, formulas); + std::shared_ptr model = buildSymbolicModel(program, formulas); STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason."); - + // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); - + BRANCH_ON_MODELTYPE(model, model, ValueType, LibraryType, preprocessModel, formulas); + // Print some information about the model. model->printModelInformationToStream(std::cout); - + // Verify the model, if a formula was given. if (!formulas.empty()) { if (model->isSparseModel()) { @@ -134,15 +134,24 @@ namespace storm { } } else if (model->isSymbolicModel()) { if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - verifySymbolicModelWithHybridEngine(model->as>(), formulas); + verifySymbolicModelWithHybridEngine(model->as>(), formulas); } else { - verifySymbolicModelWithSymbolicEngine(model->as>(), formulas); + verifySymbolicModelWithSymbolicEngine(model->as>(), formulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); } } } + + template + void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) { + buildAndCheckSymbolicModel(program, formulas); + } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) { + buildAndCheckSymbolicModel(program, formulas); + } + } template void buildAndCheckExplicitModel(std::vector> const& formulas) { diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 618fbfe77..fffb10366 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -17,6 +17,7 @@ #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/CounterexampleGeneratorSettings.h" #include "src/settings/modules/CuddSettings.h" +#include "src/settings/modules/SylvanSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/BisimulationSettings.h" @@ -38,6 +39,7 @@ namespace storm { this->addModule(std::unique_ptr(new modules::DebugSettings(*this))); this->addModule(std::unique_ptr(new modules::CounterexampleGeneratorSettings(*this))); this->addModule(std::unique_ptr(new modules::CuddSettings(*this))); + this->addModule(std::unique_ptr(new modules::SylvanSettings(*this))); this->addModule(std::unique_ptr(new modules::GmmxxEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::NativeEquationSolverSettings(*this))); this->addModule(std::unique_ptr(new modules::BisimulationSettings(*this))); @@ -509,6 +511,10 @@ namespace storm { storm::settings::modules::CuddSettings const& cuddSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::CuddSettings::moduleName)); } + + storm::settings::modules::SylvanSettings const& sylvanSettings() { + return dynamic_cast(manager().getModule(storm::settings::modules::SylvanSettings::moduleName)); + } storm::settings::modules::GmmxxEquationSolverSettings const& gmmxxEquationSolverSettings() { return dynamic_cast(manager().getModule(storm::settings::modules::GmmxxEquationSolverSettings::moduleName)); diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index fd00654c3..8d6f79964 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -16,6 +16,7 @@ namespace storm { class DebugSettings; class CounterexampleGeneratorSettings; class CuddSettings; + class SylvanSettings; class GmmxxEquationSolverSettings; class NativeEquationSolverSettings; class BisimulationSettings; @@ -267,6 +268,13 @@ namespace storm { * @return An object that allows accessing the CUDD settings. */ storm::settings::modules::CuddSettings const& cuddSettings(); + + /*! + * Retrieves the Sylvan settings. + * + * @return An object that allows accessing the Sylvan settings. + */ + storm::settings::modules::SylvanSettings const& sylvanSettings(); /*! * Retrieves the settings of the gmm++-based equation solver. diff --git a/src/settings/modules/CuddSettings.cpp b/src/settings/modules/CuddSettings.cpp index 02f0db53f..1cd54d011 100644 --- a/src/settings/modules/CuddSettings.cpp +++ b/src/settings/modules/CuddSettings.cpp @@ -19,7 +19,7 @@ namespace storm { CuddSettings::CuddSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(2048).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build()); std::vector reorderingTechniques; reorderingTechniques.push_back("none"); diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 893dd4717..83da850bf 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -8,6 +8,8 @@ #include "src/settings/Argument.h" #include "src/solver/SolverSelectionOptions.h" +#include "src/storage/dd/DdType.h" + #include "src/exceptions/InvalidSettingsException.h" namespace storm { @@ -51,6 +53,7 @@ namespace storm { const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; const std::string GeneralSettings::engineOptionName = "engine"; const std::string GeneralSettings::engineOptionShortName = "e"; + const std::string GeneralSettings::ddLibraryOptionName = "ddlib"; const std::string GeneralSettings::cudaOptionName = "cuda"; const std::string GeneralSettings::prismCompatibilityOptionName = "prismcompat"; const std::string GeneralSettings::prismCompatibilityOptionShortName = "pc"; @@ -100,6 +103,10 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, timeoutOptionName, false, "If given, computation will abort after the timeout has been reached.").setShortName(timeoutOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("time", "The number of seconds after which to timeout.").setDefaultValueUnsignedInteger(0).build()).build()); + std::vector ddLibraries = {"cudd", "sylvan"}; + this->addOption(storm::settings::OptionBuilder(moduleName, ddLibraryOptionName, false, "Sets which library is preferred for decision-diagram operations.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the library to prefer. Available are: cudd and sylvan.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(ddLibraries)).setDefaultValueString("cudd").build()).build()); + std::vector lpSolvers = {"gurobi", "glpk"}; this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver. Available are: gurobi and glpk.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(lpSolvers)).setDefaultValueString("glpk").build()).build()); @@ -270,6 +277,15 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown SMT solver '" << smtSolverName << "'."); } + storm::dd::DdType GeneralSettings::getDdLibraryType() const { + std::string ddLibraryAsString = this->getOption(ddLibraryOptionName).getArgumentByName("name").getValueAsString(); + if (ddLibraryAsString == "sylvan") { + return storm::dd::DdType::Sylvan; + } else { + return storm::dd::DdType::CUDD; + } + } + bool GeneralSettings::isConstantsSet() const { return this->getOption(constantsOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 1c7abdc98..7952dc078 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -11,6 +11,10 @@ namespace storm { enum class MinMaxTechnique; enum class SmtSolverType; } + + namespace dd { + enum class DdType; + } namespace settings { namespace modules { @@ -276,6 +280,13 @@ namespace storm { */ storm::solver::SmtSolverType getSmtSolver() const; + /*! + * Retrieves the selected library for DD-related operations. + * + * @return The selected library. + */ + storm::dd::DdType getDdLibraryType() const; + /*! * Retrieves whether the export-to-dot option was set. * @@ -399,6 +410,7 @@ namespace storm { static const std::string bisimulationOptionShortName; static const std::string engineOptionName; static const std::string engineOptionShortName; + static const std::string ddLibraryOptionName; static const std::string cudaOptionName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; diff --git a/src/settings/modules/SylvanSettings.cpp b/src/settings/modules/SylvanSettings.cpp new file mode 100644 index 000000000..e22368162 --- /dev/null +++ b/src/settings/modules/SylvanSettings.cpp @@ -0,0 +1,33 @@ +#include "src/settings/modules/SylvanSettings.h" + +#include "src/settings/SettingsManager.h" + +#include "src/settings/Option.h" +#include "src/settings/OptionBuilder.h" +#include "src/settings/ArgumentBuilder.h" +#include "src/settings/Argument.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string SylvanSettings::moduleName = "sylvan"; + const std::string SylvanSettings::maximalMemoryOptionName = "maxmem"; + const std::string SylvanSettings::threadCountOptionName = "threads"; + + SylvanSettings::SylvanSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Sylvan in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Sylvan.").setDefaultValueUnsignedInteger(4096).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, threadCountOptionName, true, "Sets the number of threads used by Sylvan.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The number of threads available to Sylvan (0 means 'auto-detect').").setDefaultValueUnsignedInteger(0).build()).build()); + } + + uint_fast64_t SylvanSettings::getMaximalMemory() const { + return this->getOption(maximalMemoryOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); + } + + uint_fast64_t SylvanSettings::getNumberOfThreads() const { + return this->getOption(threadCountOptionName).getArgumentByName("value").getValueAsUnsignedInteger(); + } + + } // namespace modules + } // namespace settings +} // namespace storm \ No newline at end of file diff --git a/src/settings/modules/SylvanSettings.h b/src/settings/modules/SylvanSettings.h new file mode 100644 index 000000000..e417fa36c --- /dev/null +++ b/src/settings/modules/SylvanSettings.h @@ -0,0 +1,50 @@ +#ifndef STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_ +#define STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_ + +#include "src/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for Sylvan. + */ + class SylvanSettings : public ModuleSettings { + public: + /*! + * Creates a new set of CUDD settings that is managed by the given manager. + * + * @param settingsManager The responsible manager. + */ + SylvanSettings(storm::settings::SettingsManager& settingsManager); + + /*! + * Retrieves the maximal amount of memory (in megabytes) that Sylvan can occupy. + * + * @return The maximal amount of memory to use. + */ + uint_fast64_t getMaximalMemory() const; + + /*! + * Retrieves the amount of threads available to Sylvan. Note that a value of zero means that the number + * of threads is auto-detected to fit the current machine. + * + * @rreturn The number of threads. + */ + uint_fast64_t getNumberOfThreads() const; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string maximalMemoryOptionName; + static const std::string threadCountOptionName; + }; + + } // namespace modules + } // namespace settings +} // namespace storm + +#endif /* STORM_SETTINGS_MODULES_SYLVANSETTINGS_H_ */ diff --git a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp index ff544c712..c91845b8d 100644 --- a/src/storage/dd/sylvan/InternalSylvanDdManager.cpp +++ b/src/storage/dd/sylvan/InternalSylvanDdManager.cpp @@ -1,8 +1,12 @@ #include "src/storage/dd/sylvan/InternalSylvanDdManager.h" +#include + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/SylvanSettings.h" + #include "src/utility/constants.h" #include "src/utility/macros.h" -#include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotSupportedException.h" #include @@ -15,13 +19,27 @@ namespace storm { // some operations. uint_fast64_t InternalDdManager::nextFreeVariableIndex = 0; + uint_fast64_t findLargestPowerOfTwoFitting(uint_fast64_t number) { + for (uint_fast64_t index = 0; index < 64; ++index) { + if ((number & (1ull << 63 - index)) != 0) { + return 63 - index; + } + } + } + InternalDdManager::InternalDdManager() { if (numberOfInstances == 0) { // Initialize lace: auto-detect number of workers. - lace_init(0, 1000000); + lace_init(storm::settings::sylvanSettings().getNumberOfThreads(), 1000000); lace_startup(0, 0, 0); - sylvan::Sylvan::initPackage(1ull << 16, 1ull << 28, 1ul << 16, 1ull << 25); + // Each node takes 24 bytes and the maximal memory is specified in megabytes. + uint_fast64_t totalNodesToStore = storm::settings::sylvanSettings().getMaximalMemory() * 1024 * 1024 / 24; + + // Compute the power of two that still fits within the total numbers to store. + uint_fast64_t powerOfTwo = findLargestPowerOfTwoFitting(totalNodesToStore); + + sylvan::Sylvan::initPackage(1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 8 : 0), 1ull << (powerOfTwo - 1), 1ull << std::max(16ull, powerOfTwo > 24 ? powerOfTwo - 12 : 0), 1ull << (powerOfTwo - 1)); sylvan::Sylvan::initBdd(1); sylvan::Sylvan::initMtbdd(); } diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 49ca3e48a..5361010eb 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -29,7 +29,7 @@ namespace storm { } } - std::vector> parseFormulasForExplicit(std::string const& inputString) { + std::vector> parseFormulasForExplicit(std::string const& inputString) { storm::parser::FormulaParser formulaParser; return parseFormulas(formulaParser, inputString); } diff --git a/src/utility/storm.h b/src/utility/storm.h index 8378d8367..fa2ac1b1e 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -82,7 +82,7 @@ namespace storm { std::vector> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); - template + template std::shared_ptr buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { std::shared_ptr result(nullptr); @@ -104,11 +104,11 @@ namespace storm { result = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options); } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) { - typename storm::builder::DdPrismModelBuilder::Options options; - options = typename storm::builder::DdPrismModelBuilder::Options(formulas); + typename storm::builder::DdPrismModelBuilder::Options options; + options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constants); - result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + result = storm::builder::DdPrismModelBuilder::translateProgram(program, options); } return result;