diff --git a/.gitignore b/.gitignore index 27874b9d4..43fe390a0 100644 --- a/.gitignore +++ b/.gitignore @@ -50,6 +50,8 @@ nbproject/ .DS_Store .idea *.out +resources/3rdparty/cudd-3.0.0/Makefile.in +resources/3rdparty/cudd-3.0.0/aclocal.m4 # Python config stormpy/setup.cfg # Travis helpers diff --git a/CHANGELOG.md b/CHANGELOG.md index 4f9972576..90c72cd28 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,24 +4,31 @@ Changelog This changelog lists only the most important changes. Smaller (bug)fixes as well as non-mature features are not part of the changelog. The releases of major and minor versions contain an overview of changes since the last major/minor update. +Version 1.1.x +------------- +Long run average computation via LRA, LP based MDP model checking, parametric model checking has an own binary -Version 1.0.x -------------------- - -### Version 1.0.2 (2017/5) +### Version 1.1.0 (2017/8) -- Fix for nested formulae -- JANI: Explicit engine supports custom model compositions. -- Storm now overwrites files if asked to write files to a specific location -- Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl +- Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach. +- Storm can now check MDPs and Markov Automata (i.e. MinMax equation systems) via Linear Programming. +- Parametric model checking is now handled in a separated library/executable called storm-pars. - Wellformedness constraints on PMCs: * include constraints from rewards * are in smtlib2 + * fixed + * computation of only constraints without doing model checking is now supported +- Fix for nested formulae +- JANI: Explicit engine supports custom model compositions. +- Support for parsing/building models given in the explicit input format of IMCA. +- Storm now overwrites files if asked to write files to a specific location. +- Changes in build process to accommodate for changes in carl. Also, more robust against issues with carl. - USE_POPCNT removed in favor of FORCE_POPCNT. The popcnt instruction is used if available due to march=native, unless portable is set. Then, using FORCE_POPCNT enables the use of the SSE 4.2 instruction -- Parametric model checking is now handled in a separated library/executable called storm-pars -- Support for long-run average rewards on MDPs and Markov automata using a value-iteration based approach -- Support for parsing/building models given in the explicit input format of IMCA. + + +Version 1.0.x +------------- ### Version 1.0.1 (2017/4) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e9059930d..38b884cf7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -2,6 +2,8 @@ set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib) set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) +add_custom_target(binaries) + add_subdirectory(storm) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) @@ -12,6 +14,8 @@ add_subdirectory(storm-dft-cli) add_subdirectory(storm-pars) add_subdirectory(storm-pars-cli) + + add_subdirectory(test) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 515022607..0d104405e 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -3,5 +3,7 @@ add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyfte target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") +add_dependencies(binaries storm-dft-cli) + # installation install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 2898325f3..72e51a6da 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -2,5 +2,7 @@ add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gsp target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") +add_dependencies(binaries storm-gspn-cli) + # installation install(TARGETS storm-gspn-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index 9cd155e35..bda5ad6c2 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -3,5 +3,7 @@ add_executable(storm-pars-cli ${PROJECT_SOURCE_DIR}/src/storm-pars-cli/storm-par target_link_libraries(storm-pars-cli storm-pars) # Adding headers for xcode set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") +add_dependencies(binaries storm-pars-cli) + # installation install(TARGETS storm-pars-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index ce78713ee..0836f1e0d 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -194,7 +194,7 @@ namespace storm { auto parametricSettings = storm::settings::getModule(); if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { auto dtmc = model->template as>(); - storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()],storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); + storm::api::exportParametricResultToFile(boost::make_optional(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]),storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); } }); } @@ -272,6 +272,7 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput& input) { auto coreSettings = storm::settings::getModule(); auto ioSettings = storm::settings::getModule(); + auto parSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); @@ -296,9 +297,27 @@ namespace storm { } std::vector> regions = parseRegions(model); - + + + if (model) { storm::cli::exportModel(model, input); + } + + if (parSettings.onlyObtainConstraints()) { + STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified."); + if (model->isOfType(storm::models::ModelType::Dtmc)) { + auto dtmc = model->template as>(); + storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*dtmc),parSettings.exportResultPath()); + return; + } else { + STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::NotImplementedException, "Constraints for MDPs and CTMCs not implemented."); + + } + + } + + if (model) { verifyParametricModel(model, input, regions); } } diff --git a/src/storm-pars/api/export.h b/src/storm-pars/api/export.h index cae413bd8..69a6405de 100644 --- a/src/storm-pars/api/export.h +++ b/src/storm-pars/api/export.h @@ -7,19 +7,21 @@ namespace storm { namespace api { template - void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + void exportParametricResultToFile(boost::optional , storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); } template <> - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + inline void exportParametricResultToFile(boost::optional result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; storm::utility::openFile(path, filestream); filestream << "$Parameters: "; - std::set vars = result.gatherVariables(); + auto const& vars = constraintCollector.getVariables(); std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); filestream << std::endl; - filestream << "$Result: " << result.toString(false, true) << std::endl; + if(result) { + filestream << "$Result: " << result->toString(false, true) << std::endl; + } filestream << "$Well-formed Constraints: " << std::endl; std::vector stringConstraints; std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp index a50ef941e..28975aa5c 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.cpp +++ b/src/storm-pars/settings/modules/ParametricSettings.cpp @@ -17,12 +17,14 @@ namespace storm { const std::string ParametricSettings::derivativesOptionName = "derivatives"; const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous"; const std::string ParametricSettings::transformContinuousShortOptionName = "tc"; + const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints"; ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, transformContinuousOptionName, false, "Sets whether to transform a continuous time input model to a discrete time model.").setShortName(transformContinuousShortOptionName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, onlyWellformednessConstraintsOptionName, false, "Sets whether you only want to obtain the wellformedness constraints").build()); } bool ParametricSettings::exportResultToFile() const { @@ -40,7 +42,10 @@ namespace storm { bool ParametricSettings::transformContinuousModel() const { return this->getOption(transformContinuousOptionName).getHasOptionBeenSet(); } - + + bool ParametricSettings::onlyObtainConstraints() const { + return this->getOption(onlyWellformednessConstraintsOptionName).getHasOptionBeenSet(); + } } // namespace modules } // namespace settings diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h index 436faa92d..e610f033d 100644 --- a/src/storm-pars/settings/modules/ParametricSettings.h +++ b/src/storm-pars/settings/modules/ParametricSettings.h @@ -41,6 +41,11 @@ namespace storm { * Retrieves whether Continuous time models should be transformed to discrete time models */ bool transformContinuousModel() const; + + /* + * Retrieves whether instead of model checking, only the wellformedness constraints should be obtained. + */ + bool onlyObtainConstraints() const; const static std::string moduleName; @@ -49,6 +54,7 @@ namespace storm { const static std::string derivativesOptionName; const static std::string transformContinuousOptionName; const static std::string transformContinuousShortOptionName; + const static std::string onlyWellformednessConstraintsOptionName; }; } // namespace modules diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index a57805ed9..193a6d4bb 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -69,6 +69,8 @@ add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_LIB add_dependencies(storm copy_storm_headers) add_dependencies(storm copy_resources_headers) +add_dependencies(binaries storm-main) + # installation install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib) install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index fb7b9e84a..bf3beeb0c 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -23,6 +23,12 @@ namespace storm { return this->graphPreservingConstraintSet; } + template + std::set const& ConstraintCollector::getVariables() const { + return this->variableSet; + } + + template void ConstraintCollector::wellformedRequiresNonNegativeEntries(std::vector const& vec) { for(auto const& entry : vec) { @@ -50,6 +56,8 @@ namespace storm { for (auto const& transition : dtmc.getRows(state)) { sum += transition.getValue(); if (!storm::utility::isConstant(transition.getValue())) { + auto const& transitionVars = transition.getValue().gatherVariables(); + variableSet.insert(transitionVars.begin(), transitionVars.end()); // Assert: 0 <= transition <= 1 if (transition.getValue().denominator().isConstant()) { assert(transition.getValue().denominator().constantPart() != 0); diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index c6043fd5a..48b4aee64 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -31,6 +31,9 @@ namespace storm { // A set of constraints that makes sure that the underlying graph of the model does not change depending // on the parameter values. std::unordered_set::val> graphPreservingConstraintSet; + + // A set of variables + std::set variableSet; void wellformedRequiresNonNegativeEntries(std::vector const&); public: @@ -55,6 +58,12 @@ namespace storm { * @return The set of graph-preserving constraints. */ std::unordered_set::val> const& getGraphPreservingConstraints() const; + + /*! + * Returns the set of variables in the model + * @return + */ + std::set const& getVariables() const; /*! * Constructs the constraints for the given DTMC. diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index c028f0e5a..dff7a2808 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -175,7 +175,7 @@ namespace storm { * @param relevantLabels The set of relevant labels of the model. * @return A mapping from labels to variable indices. */ - static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { + static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { std::stringstream variableNameBuffer; std::unordered_map resultingMap; for (auto const& label : relevantLabels) { @@ -195,7 +195,7 @@ namespace storm { * @param choiceInformation The information about the choices of the model. * @return A mapping from states to a list of choice variable indices. */ - static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair>, uint_fast64_t> createSchedulerVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map> resultingMap; @@ -223,7 +223,7 @@ namespace storm { * @param stateInformation The information about the states of the model. * @return A mapping from initial states to choice variable indices. */ - static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation) { + static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -248,7 +248,7 @@ namespace storm { * @param stateInformation The information about the states in the model. * @return A mapping from states to the index of the corresponding probability variables. */ - static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { + static std::pair, uint_fast64_t> createProbabilityVariables(storm::solver::LpSolver& solver, StateInformation const& stateInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -269,7 +269,7 @@ namespace storm { * @param solver The MILP solver. * @return The index of the variable for the probability of the virtual initial state. */ - static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver) { + static std::pair createVirtualInitialStateVariable(storm::solver::LpSolver& solver) { std::stringstream variableNameBuffer; variableNameBuffer << "pinit"; storm::expressions::Variable variable = solver.addBoundedContinuousVariable(variableNameBuffer.str(), 0, 1); @@ -284,7 +284,7 @@ namespace storm { * @param stateInformation The information about the states in the model. * @return A mapping from problematic states to the index of the corresponding variables. */ - static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -327,7 +327,7 @@ namespace storm { * @param choiceInformation The information about the choices in the model. * @return A mapping from problematic choices to the index of the corresponding variables. */ - static std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, storm::expressions::Variable, PairHash> resultingMap; @@ -359,7 +359,7 @@ namespace storm { * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. */ - static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { // Create a struct that stores all information about variables. VariableInformation result; @@ -423,7 +423,7 @@ namespace storm { * @param strictBound A flag indicating whether the threshold must be exceeded or only matched. * @return The total number of constraints that were created. */ - static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) { + static uint_fast64_t assertProbabilityGreaterThanThreshold(storm::solver::LpSolver& solver, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound) { storm::expressions::Expression constraint; if (strictBound) { constraint = variableInformation.virtualInitialStateVariable > solver.getConstant(probabilityThreshold); @@ -442,7 +442,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertValidPolicy(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertValidPolicy(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) { // Assert that the policy chooses at most one action in each state of the system. uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { @@ -484,7 +484,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; @@ -511,7 +511,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertZeroProbabilityWithoutChoice(storm::solver::LpSolver& solver, StateInformation const& stateInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { storm::expressions::Expression constraint = variableInformation.stateToProbabilityVariableMap.at(state); @@ -536,7 +536,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); @@ -581,7 +581,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto stateListPair : choiceInformation.problematicChoicesForProblematicStates) { @@ -629,7 +629,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto label : choiceInformation.knownLabels) { @@ -652,7 +652,7 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); uint_fast64_t numberOfConstraintsCreated = 0; @@ -812,7 +812,7 @@ namespace storm { * @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of * possible choices. */ - static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { + static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { // Assert that the reachability probability in the subsystem exceeds the given threshold. uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound); STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold."); @@ -860,7 +860,7 @@ namespace storm { * @param solver The MILP solver. * @param variableInformation A struct with information about the variables of the model. */ - static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { boost::container::flat_set result; for (auto const& labelVariablePair : variableInformation.labelToVariableMap) { @@ -883,7 +883,7 @@ namespace storm { * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. */ - static std::map getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static std::map getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { std::map result; for (auto state : stateInformation.relevantStates) { @@ -907,7 +907,7 @@ namespace storm { * @param mdp The MDP. * @param variableInformation A struct with information about the variables of the model. */ - static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, VariableInformation const& variableInformation) { + static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, VariableInformation const& variableInformation) { uint_fast64_t selectedInitialState = 0; for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) { bool initialStateChosen = solver.getBinaryValue(initialStateVariablePair.second); @@ -945,7 +945,7 @@ namespace storm { ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, labelSets, stateInformation, psiStates); // (4) Encode resulting system as MILP problem. - std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample"); + std::shared_ptr> solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample"); // (4.1) Create variables. VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 1ca0b3728..3aaeec73d 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -427,8 +427,8 @@ namespace storm { template ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { - std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); - std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); + std::unique_ptr> lpSolverFactory(new storm::utility::solver::LpSolverFactory()); + std::unique_ptr> solver = lpSolverFactory->create("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. @@ -437,7 +437,7 @@ namespace storm { std::string variableName = "x" + std::to_string(stateChoicesPair.first); stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); } - storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", 1); + storm::expressions::Variable k = solver->addUnboundedContinuousVariable("k", storm::utility::one()); solver->update(); // Now we encode the problem as constraints. @@ -487,7 +487,7 @@ namespace storm { } solver->optimize(); - return storm::utility::convertNumber(solver->getContinuousValue(k)); + return solver->getContinuousValue(k); } template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index c8dab63c4..2b186fdca 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -801,7 +801,7 @@ namespace storm { template template ValueType SparseMdpPrctlHelper::computeLraForMaximalEndComponentLP(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::storage::MaximalEndComponent const& mec) { - std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); + std::shared_ptr> solver = storm::utility::solver::getLpSolver("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); // First, we need to create the variables for the problem. @@ -822,10 +822,10 @@ namespace storm { storm::expressions::Expression constraint = -lambda; for (auto element : transitionMatrix.getRow(choice)) { - constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(storm::utility::convertNumber(element.getValue())); + constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); } typename RewardModelType::ValueType r = rewardModel.getTotalStateActionReward(state, choice, transitionMatrix); - constraint = solver->getConstant(storm::utility::convertNumber(r)) + constraint; + constraint = solver->getConstant(r) + constraint; if (dir == OptimizationDirection::Minimize) { constraint = stateToVariableMap.at(state) <= constraint; @@ -837,7 +837,7 @@ namespace storm { } solver->optimize(); - return storm::utility::convertNumber(solver->getContinuousValue(lambda)); + return solver->getContinuousValue(lambda); } template diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index f92acab7a..009b9b3eb 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -90,8 +90,11 @@ namespace storm { storm::jani::ModelType type = storm::jani::getModelType(modeltypestring); STORM_LOG_THROW(type != storm::jani::ModelType::UNDEFINED, storm::exceptions::InvalidJaniException, "model type " + modeltypestring + " not recognized"); storm::jani::Model model(name, type, version, expressionManager); - STORM_LOG_THROW(parsedStructure.count("actions") < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once."); - parseActions(parsedStructure.at("actions"), model); + size_t actionCount = parsedStructure.count("actions"); + STORM_LOG_THROW(actionCount < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once."); + if (actionCount > 0) { + parseActions(parsedStructure.at("actions"), model); + } size_t constantsCount = parsedStructure.count("constants"); std::unordered_map> constants; STORM_LOG_THROW(constantsCount < 2, storm::exceptions::InvalidJaniException, "Constant-declarations can be given at most once."); diff --git a/src/storm/permissivesched/MILPPermissiveSchedulers.h b/src/storm/permissivesched/MILPPermissiveSchedulers.h index fe5a48e11..ed85e4d9f 100644 --- a/src/storm/permissivesched/MILPPermissiveSchedulers.h +++ b/src/storm/permissivesched/MILPPermissiveSchedulers.h @@ -25,7 +25,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation private: bool mCalledOptimizer = false; - storm::solver::LpSolver& solver; + storm::solver::LpSolver& solver; std::unordered_map multistrategyVariables; std::unordered_map mProbVariables; std::unordered_map mAlphaVariables; @@ -34,7 +34,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation public: - MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) + MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) : PermissiveSchedulerComputation(mdp, goalstates, sinkstates), solver(milpsolver) { diff --git a/src/storm/permissivesched/PermissiveSchedulers.cpp b/src/storm/permissivesched/PermissiveSchedulers.cpp index 1a7e7061b..5454eeb6e 100644 --- a/src/storm/permissivesched/PermissiveSchedulers.cpp +++ b/src/storm/permissivesched/PermissiveSchedulers.cpp @@ -23,7 +23,7 @@ namespace storm { goalstates = storm::utility::graph::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); - auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); + auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported"); comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getThresholdAs()); diff --git a/src/storm/solver/GlpkLpSolver.cpp b/src/storm/solver/GlpkLpSolver.cpp index 51faf7eea..707883c05 100644 --- a/src/storm/solver/GlpkLpSolver.cpp +++ b/src/storm/solver/GlpkLpSolver.cpp @@ -1,13 +1,13 @@ #include "storm/solver/GlpkLpSolver.h" -#ifdef STORM_HAVE_GLPK - #include +#include #include "storm/storage/expressions/LinearCoefficientVisitor.h" #include "storm/settings/SettingsManager.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -18,11 +18,14 @@ #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/GlpkSettings.h" -#include + namespace storm { namespace solver { - GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { + +#ifdef STORM_HAVE_GLPK + template + GlpkLpSolver::GlpkLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), lp(nullptr), variableToIndexMap(), nextVariableIndex(1), nextConstraintIndex(1), modelContainsIntegerVariables(false), isInfeasibleFlag(false), isUnboundedFlag(false), rowIndices(), columnIndices(), coefficientValues() { // Create the LP problem for glpk. lp = glp_create_prob(); @@ -38,84 +41,98 @@ namespace storm { coefficientValues.push_back(0); } - GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) { + template + GlpkLpSolver::GlpkLpSolver(std::string const& name) : GlpkLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) { + template + GlpkLpSolver::GlpkLpSolver() : GlpkLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) { + template + GlpkLpSolver::GlpkLpSolver(OptimizationDirection const& optDir) : GlpkLpSolver("", optDir) { // Intentionally left empty. } - GlpkLpSolver::~GlpkLpSolver() { + template + GlpkLpSolver::~GlpkLpSolver() { // Dispose of all objects allocated dynamically by glpk. glp_delete_prob(this->lp); glp_free_env(); } - storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareRationalVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareRationalVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareRationalVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareRationalVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareRationalVariable(name); this->addVariable(newVariable, GLP_CV, GLP_FR, 0, 0, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_DB, lowerBound, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } - storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_LO, lowerBound, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } - storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_UP, 0, upperBound, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } - storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_IV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } - storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareIntegerVariable(name); + template + storm::expressions::Variable GlpkLpSolver::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareIntegerVariable(name); this->addVariable(newVariable, GLP_BV, GLP_FR, 0, 0, objectiveFunctionCoefficient); this->modelContainsIntegerVariables = true; return newVariable; } - void GlpkLpSolver::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + template + void GlpkLpSolver::addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { // Check for valid variable type. STORM_LOG_ASSERT(variableType == GLP_CV || variableType == GLP_IV || variableType == GLP_BV, "Illegal type '" << variableType << "' for glpk variable."); @@ -125,18 +142,20 @@ namespace storm { // Finally, create the actual variable. glp_add_cols(this->lp, 1); glp_set_col_name(this->lp, nextVariableIndex, variable.getName().c_str()); - glp_set_col_bnds(lp, nextVariableIndex, boundType, lowerBound, upperBound); + glp_set_col_bnds(lp, nextVariableIndex, boundType, storm::utility::convertNumber(lowerBound), storm::utility::convertNumber(upperBound)); glp_set_col_kind(this->lp, nextVariableIndex, variableType); - glp_set_obj_coef(this->lp, nextVariableIndex, objectiveFunctionCoefficient); + glp_set_obj_coef(this->lp, nextVariableIndex, storm::utility::convertNumber(objectiveFunctionCoefficient)); this->variableToIndexMap.emplace(variable, this->nextVariableIndex); ++this->nextVariableIndex; } - void GlpkLpSolver::update() const { + template + void GlpkLpSolver::update() const { // Intentionally left empty. } - void GlpkLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + template + void GlpkLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { // Add the row that will represent this constraint. glp_add_rows(this->lp, 1); glp_set_row_name(this->lp, nextConstraintIndex, name.c_str()); @@ -188,7 +207,8 @@ namespace storm { this->currentModelHasBeenOptimized = false; } - void GlpkLpSolver::optimize() const { + template + void GlpkLpSolver::optimize() const { // First, reset the flags. this->isInfeasibleFlag = false; this->isUnboundedFlag = false; @@ -226,7 +246,8 @@ namespace storm { this->currentModelHasBeenOptimized = true; } - bool GlpkLpSolver::isInfeasible() const { + template + bool GlpkLpSolver::isInfeasible() const { if (!this->currentModelHasBeenOptimized) { throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isInfeasible: model has not been optimized."; } @@ -238,7 +259,8 @@ namespace storm { } } - bool GlpkLpSolver::isUnbounded() const { + template + bool GlpkLpSolver::isUnbounded() const { if (!this->currentModelHasBeenOptimized) { throw storm::exceptions::InvalidStateException() << "Illegal call to GlpkLpSolver::isUnbounded: model has not been optimized."; } @@ -250,7 +272,8 @@ namespace storm { } } - bool GlpkLpSolver::isOptimal() const { + template + bool GlpkLpSolver::isOptimal() const { if (!this->currentModelHasBeenOptimized) { return false; } @@ -264,7 +287,8 @@ namespace storm { return status == GLP_OPT; } - double GlpkLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { + template + ValueType GlpkLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model."); @@ -280,10 +304,11 @@ namespace storm { } else { value = glp_get_col_prim(this->lp, static_cast(variableIndexPair->second)); } - return value; + return storm::utility::convertNumber(value); } - int_fast64_t GlpkLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t GlpkLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model."); @@ -306,7 +331,8 @@ namespace storm { return static_cast(value); } - bool GlpkLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + template + bool GlpkLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model."); @@ -328,7 +354,8 @@ namespace storm { return static_cast(value); } - double GlpkLpSolver::getObjectiveValue() const { + template + ValueType GlpkLpSolver::getObjectiveValue() const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from infeasible model."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get glpk solution from unbounded model."); @@ -342,14 +369,18 @@ namespace storm { value = glp_get_obj_val(this->lp); } - return value; + return storm::utility::convertNumber(value); } - void GlpkLpSolver::writeModelToFile(std::string const& filename) const { + template + void GlpkLpSolver::writeModelToFile(std::string const& filename) const { glp_load_matrix(this->lp, rowIndices.size() - 1, rowIndices.data(), columnIndices.data(), coefficientValues.data()); glp_write_lp(this->lp, 0, filename.c_str()); } + + template class GlpkLpSolver; + template class GlpkLpSolver; +#endif } } -#endif diff --git a/src/storm/solver/GlpkLpSolver.h b/src/storm/solver/GlpkLpSolver.h index 63be0ede7..a0c30b39a 100644 --- a/src/storm/solver/GlpkLpSolver.h +++ b/src/storm/solver/GlpkLpSolver.h @@ -18,7 +18,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using glpk as the background solver. */ - class GlpkLpSolver : public LpSolver { + template + class GlpkLpSolver : public LpSolver { public: /*! * Constructs a solver with the given name and model sense. @@ -57,19 +58,19 @@ namespace storm { virtual ~GlpkLpSolver(); // Methods to add continuous variables. - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add integer variables. - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -84,10 +85,10 @@ namespace storm { virtual bool isOptimal() const override; // Methods to retrieve values of variables and the objective function in the optimal solutions. - virtual double getContinuousValue(storm::expressions::Variable const& name) const override; + virtual ValueType getContinuousValue(storm::expressions::Variable const& name) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; - virtual double getObjectiveValue() const override; + virtual ValueType getObjectiveValue() const override; // Methods to print the LP problem to a file. virtual void writeModelToFile(std::string const& filename) const override; @@ -103,7 +104,7 @@ namespace storm { * @param upperBound The upper bound of the range of the variable. * @param objectiveFunctionCoefficient The coefficient of the variable in the objective function. */ - void addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, double lowerBound, double upperBound, double objectiveFunctionCoefficient); + void addVariable(storm::expressions::Variable const& variable, int variableType, int boundType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient); // The glpk LP problem. glp_prob* lp; @@ -153,39 +154,39 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } @@ -213,7 +214,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual double getContinuousValue(storm::expressions::Variable const& variable) const override { + virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) const override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } @@ -225,7 +226,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual double getObjectiveValue() const override { + virtual ValueType getObjectiveValue() const override { throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp index 76713be08..23866ea46 100644 --- a/src/storm/solver/GurobiLpSolver.cpp +++ b/src/storm/solver/GurobiLpSolver.cpp @@ -9,6 +9,8 @@ #include "storm/settings/modules/GurobiSettings.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" + #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -22,7 +24,8 @@ namespace storm { namespace solver { #ifdef STORM_HAVE_GUROBI - GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) { + template + GurobiLpSolver::GurobiLpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir), env(nullptr), model(nullptr), nextVariableIndex(0) { // Create the environment. int error = GRBloadenv(&env, ""); if (error || env == nullptr) { @@ -41,25 +44,30 @@ namespace storm { } } - GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) { + template + GurobiLpSolver::GurobiLpSolver(std::string const& name) : GurobiLpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) { + template + GurobiLpSolver::GurobiLpSolver(OptimizationDirection const& optDir) : GurobiLpSolver("", optDir) { // Intentionally left empty. } - GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) { + template + GurobiLpSolver::GurobiLpSolver() : GurobiLpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - GurobiLpSolver::~GurobiLpSolver() { + template + GurobiLpSolver::~GurobiLpSolver() { // Dispose of the objects allocated inside Gurobi. GRBfreemodel(model); GRBfreeenv(env); } - void GurobiLpSolver::setGurobiEnvironmentProperties() const { + template + void GurobiLpSolver::setGurobiEnvironmentProperties() const { int error = 0; // Enable the following line to only print the output of Gurobi if the debug flag is set. @@ -73,7 +81,8 @@ namespace storm { STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter IntFeasTol (" << GRBgeterrormsg(env) << ", error code " << error << ")."); } - void GurobiLpSolver::update() const { + template + void GurobiLpSolver::update() const { int error = GRBupdatemodel(model); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ")."); @@ -81,73 +90,84 @@ namespace storm { this->currentModelHasBeenOptimized = false; } - storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); this->addVariable(newVariable, GRB_CONTINUOUS, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, lowerBound, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, lowerBound, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, upperBound, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_INTEGER, -GRB_INFINITY, GRB_INFINITY, objectiveFunctionCoefficient); return newVariable; } - storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); this->addVariable(newVariable, GRB_BINARY, 0, 1, objectiveFunctionCoefficient); return newVariable; } - void GurobiLpSolver::addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { + template + void GurobiLpSolver::addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { // Check for valid variable type. STORM_LOG_ASSERT(variableType == GRB_CONTINUOUS || variableType == GRB_INTEGER || variableType == GRB_BINARY, "Illegal type '" << variableType << "' for Gurobi variable."); // Finally, create the actual variable. int error = 0; - error = GRBaddvar(model, 0, nullptr, nullptr, objectiveFunctionCoefficient, lowerBound, upperBound, variableType, variable.getName().c_str()); + error = GRBaddvar(model, 0, nullptr, nullptr, storm::utility::convertNumber(objectiveFunctionCoefficient), storm::utility::convertNumber(lowerBound), storm::utility::convertNumber(upperBound), variableType, variable.getName().c_str()); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not create binary Gurobi variable (" << GRBgeterrormsg(env) << ", error code " << error << ")."); this->variableToIndexMap.emplace(variable, nextVariableIndex); ++nextVariableIndex; } - - void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + + template + void GurobiLpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); @@ -188,7 +208,8 @@ namespace storm { STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Could not assert constraint (" << GRBgeterrormsg(env) << ", error code " << error << ")."); } - void GurobiLpSolver::optimize() const { + template + void GurobiLpSolver::optimize() const { // First incorporate all recent changes. this->update(); @@ -203,9 +224,10 @@ namespace storm { this->currentModelHasBeenOptimized = true; } - bool GurobiLpSolver::isInfeasible() const { + template + bool GurobiLpSolver::isInfeasible() const { if (!this->currentModelHasBeenOptimized) { - throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isInfeasible: model has not been optimized."; + throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isInfeasible: model has not been optimized."; } int optimalityStatus = 0; @@ -231,9 +253,10 @@ namespace storm { return optimalityStatus == GRB_INFEASIBLE; } - bool GurobiLpSolver::isUnbounded() const { + template + bool GurobiLpSolver::isUnbounded() const { if (!this->currentModelHasBeenOptimized) { - throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isUnbounded: model has not been optimized."; + throw storm::exceptions::InvalidStateException() << "Illegal call to GurobiLpSolver::isUnbounded: model has not been optimized."; } int optimalityStatus = 0; @@ -259,7 +282,8 @@ namespace storm { return optimalityStatus == GRB_UNBOUNDED; } - bool GurobiLpSolver::isOptimal() const { + template + bool GurobiLpSolver::isOptimal() const { if (!this->currentModelHasBeenOptimized) { return false; } @@ -271,7 +295,8 @@ namespace storm { return optimalityStatus == GRB_OPTIMAL; } - double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); @@ -285,10 +310,11 @@ namespace storm { int error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableIndexPair->second, &value); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - return value; + return storm::utility::convertNumber(value); } - int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); @@ -306,7 +332,8 @@ namespace storm { return static_cast(value); } - bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); @@ -329,7 +356,8 @@ namespace storm { return static_cast(value); } - double GurobiLpSolver::getObjectiveValue() const { + template + ValueType GurobiLpSolver::getObjectiveValue() const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from infeasible model (" << GRBgeterrormsg(env) << ")."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Gurobi solution from unbounded model (" << GRBgeterrormsg(env) << ")."); @@ -340,10 +368,11 @@ namespace storm { int error = GRBgetdblattr(model, GRB_DBL_ATTR_OBJVAL, &value); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to get Gurobi solution (" << GRBgeterrormsg(env) << ", error code " << error << ")."); - return value; + return storm::utility::convertNumber(value); } - void GurobiLpSolver::writeModelToFile(std::string const& filename) const { + template + void GurobiLpSolver::writeModelToFile(std::string const& filename) const { int error = GRBwrite(model, filename.c_str()); if (error) { STORM_LOG_ERROR("Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file."); @@ -351,115 +380,144 @@ namespace storm { } } - void GurobiLpSolver::toggleOutput(bool set) const { + template + void GurobiLpSolver::toggleOutput(bool set) const { int error = GRBsetintparam(env, "OutputFlag", set); STORM_LOG_THROW(error == 0, storm::exceptions::InvalidStateException, "Unable to set Gurobi Parameter OutputFlag (" << GRBgeterrormsg(env) << ", error code " << error << ")."); } -#else - GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - GurobiLpSolver::GurobiLpSolver(std::string const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - GurobiLpSolver::GurobiLpSolver(OptimizationDirection const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - GurobiLpSolver::GurobiLpSolver() { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - GurobiLpSolver::~GurobiLpSolver() { - - } - - storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - - storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const&, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const&, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const&, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - void GurobiLpSolver::update() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - void GurobiLpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - void GurobiLpSolver::optimize() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - bool GurobiLpSolver::isInfeasible() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - bool GurobiLpSolver::isUnbounded() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - bool GurobiLpSolver::isOptimal() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - double GurobiLpSolver::getObjectiveValue() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } - - void GurobiLpSolver::writeModelToFile(std::string const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } +#else + template + GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + GurobiLpSolver::GurobiLpSolver(std::string const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + GurobiLpSolver::GurobiLpSolver(OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + GurobiLpSolver::GurobiLpSolver() { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + GurobiLpSolver::~GurobiLpSolver() { + + } + + template + storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const&, ValueType, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const&, ValueType, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } + + template + storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const&, ValueType, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const&, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const&, ValueType, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const&, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const&, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const&, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const&, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + void GurobiLpSolver::update() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + void GurobiLpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + void GurobiLpSolver::optimize() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + bool GurobiLpSolver::isInfeasible() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + bool GurobiLpSolver::isUnbounded() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + bool GurobiLpSolver::isOptimal() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + ValueType GurobiLpSolver::getObjectiveValue() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } + + template + void GurobiLpSolver::writeModelToFile(std::string const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } - void GurobiLpSolver::toggleOutput(bool) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; - } + template + void GurobiLpSolver::toggleOutput(bool) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; + } -#endif +#endif + template class GurobiLpSolver; + template class GurobiLpSolver; } } diff --git a/src/storm/solver/GurobiLpSolver.h b/src/storm/solver/GurobiLpSolver.h index 41d6e3800..f1ca786f3 100644 --- a/src/storm/solver/GurobiLpSolver.h +++ b/src/storm/solver/GurobiLpSolver.h @@ -22,7 +22,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using Gurobi. */ - class GurobiLpSolver : public LpSolver { + template + class GurobiLpSolver : public LpSolver { public: /*! * Constructs a solver with the given name and model sense. @@ -61,19 +62,19 @@ namespace storm { virtual ~GurobiLpSolver(); // Methods to add continuous variables. - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add integer variables. - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -88,10 +89,10 @@ namespace storm { virtual bool isOptimal() const override; // Methods to retrieve values of variables and the objective function in the optimal solutions. - virtual double getContinuousValue(storm::expressions::Variable const& name) const override; + virtual ValueType getContinuousValue(storm::expressions::Variable const& name) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& name) const override; virtual bool getBinaryValue(storm::expressions::Variable const& name) const override; - virtual double getObjectiveValue() const override; + virtual ValueType getObjectiveValue() const override; // Methods to print the LP problem to a file. virtual void writeModelToFile(std::string const& filename) const override; @@ -113,7 +114,7 @@ namespace storm { * @param upperBound The upper bound of the range of the variable. * @param objectiveFunctionCoefficient The coefficient of the variable in the objective function. */ - void addVariable(storm::expressions::Variable const& variable, char variableType, double lowerBound, double upperBound, double objectiveFunctionCoefficient); + void addVariable(storm::expressions::Variable const& variable, char variableType, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient); #ifdef STORM_HAVE_GUROBI // The Gurobi environment. GRBenv* env; diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index 3d4f06156..301db3049 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -46,8 +46,9 @@ namespace storm { virtual void clearCache() const override; - virtual ValueType getPrecision() const override; - virtual bool getRelative() const override; + ValueType getPrecision() const; + bool getRelative() const; + private: bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; bool solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const; diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp new file mode 100644 index 000000000..35de0902d --- /dev/null +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -0,0 +1,161 @@ +#include "storm/solver/LpMinMaxLinearEquationSolver.h" + +#include "storm/utility/vector.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace solver { + + template + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + // Intentionally left empty. + } + + template + LpMinMaxLinearEquationSolver::LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory) : StandardMinMaxLinearEquationSolver(std::move(A), std::move(linearEquationSolverFactory)), lpSolverFactory(std::move(lpSolverFactory)) { + // Intentionally left empty. + } + + template + bool LpMinMaxLinearEquationSolver::solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const { + + // Set up the LP solver + std::unique_ptr> solver = lpSolverFactory->create(""); + solver->setOptimizationDirection(invert(dir)); + + // Create a variable for each row group + std::vector variables; + variables.reserve(this->A.getRowGroupCount()); + for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { + if (this->lowerBound) { + if (this->upperBound) { + variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one())); + } else { + variables.push_back(solver->addLowerBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), storm::utility::one())); + } + } else { + if (this->upperBound) { + variables.push_back(solver->addUpperBoundedContinuousVariable("x" + std::to_string(rowGroup), this->upperBound.get(), storm::utility::one())); + } else { + variables.push_back(solver->addUnboundedContinuousVariable("x" + std::to_string(rowGroup), storm::utility::one())); + } + } + } + solver->update(); + + // Add a constraint for each row + for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { + for (uint64_t row = this->A.getRowGroupIndices()[rowGroup]; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row) { + storm::expressions::Expression rowConstraint = solver->getConstant(b[row]); + for (auto const& entry : this->A.getRow(row)) { + rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression()); + } + if (minimize(dir)) { + rowConstraint = variables[rowGroup].getExpression() <= rowConstraint; + } else { + rowConstraint = variables[rowGroup].getExpression() >= rowConstraint; + } + solver->addConstraint("", rowConstraint); + } + } + + // Invoke optimization + solver->optimize(); + STORM_LOG_THROW(!solver->isInfeasible(), storm::exceptions::UnexpectedException, "The MinMax equation system is infeasible."); + STORM_LOG_THROW(!solver->isUnbounded(), storm::exceptions::UnexpectedException, "The MinMax equation system is unbounded."); + STORM_LOG_THROW(solver->isOptimal(), storm::exceptions::UnexpectedException, "Unable to find optimal solution for MinMax equation system."); + + // write the solution into the solution vector + STORM_LOG_ASSERT(x.size() == variables.size(), "Dimension of x-vector does not match number of varibales."); + auto xIt = x.begin(); + auto vIt = variables.begin(); + for (; xIt != x.end(); ++xIt, ++vIt) { + *xIt = solver->getContinuousValue(*vIt); + } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + this->schedulerChoices = std::vector(this->A.getRowGroupCount()); + for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { + uint64_t row = this->A.getRowGroupIndices()[rowGroup]; + uint64_t optimalChoiceIndex = 0; + uint64_t currChoice = 0; + ValueType optimalGroupValue = this->A.multiplyRowWithVector(row, x) + b[row]; + for (++row, ++currChoice; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) { + ValueType rowValue = this->A.multiplyRowWithVector(row, x) + b[row]; + if ((minimize(dir) && rowValue < optimalGroupValue) || (maximize(dir) && rowValue > optimalGroupValue)) { + optimalGroupValue = rowValue; + optimalChoiceIndex = currChoice; + } + } + this->schedulerChoices.get()[rowGroup] = optimalChoiceIndex; + } + } + + return true; + } + + template + void LpMinMaxLinearEquationSolver::clearCache() const { + StandardMinMaxLinearEquationSolver::clearCache(); + } + + template + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::make_unique>()) { + // Intentionally left empty + } + + template + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { + // Intentionally left empty + } + + template + LpMinMaxLinearEquationSolverFactory::LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory, bool trackScheduler) : StandardMinMaxLinearEquationSolverFactory(std::move(linearEquationSolverFactory), MinMaxMethodSelection::LinearProgramming, trackScheduler), lpSolverFactory(std::move(lpSolverFactory)) { + // Intentionally left empty + } + + template + std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { + STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); + STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); + + std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); + result->setTrackScheduler(this->isTrackSchedulerSet()); + return result; + } + + template + std::unique_ptr> LpMinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix&& matrix) const { + STORM_LOG_ASSERT(this->linearEquationSolverFactory, "Linear equation solver factory not initialized."); + STORM_LOG_ASSERT(this->lpSolverFactory, "Lp solver factory not initialized."); + + std::unique_ptr> result = std::make_unique>(std::move(matrix), this->linearEquationSolverFactory->clone(), this->lpSolverFactory->clone()); + result->setTrackScheduler(this->isTrackSchedulerSet()); + return result; + } + + template + void LpMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethodSelection const& newMethod) { + STORM_LOG_THROW(newMethod == MinMaxMethodSelection::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + } + + template + void LpMinMaxLinearEquationSolverFactory::setMinMaxMethod(MinMaxMethod const& newMethod) { + STORM_LOG_THROW(newMethod == MinMaxMethod::LinearProgramming, storm::exceptions::InvalidOperationException, "The factory can only create linear programming based MinMax solvers."); + MinMaxLinearEquationSolverFactory::setMinMaxMethod(newMethod); + } + + template class LpMinMaxLinearEquationSolver; + template class LpMinMaxLinearEquationSolverFactory; + +#ifdef STORM_HAVE_CARL + template class LpMinMaxLinearEquationSolver; + template class LpMinMaxLinearEquationSolverFactory; +#endif + } +} diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h new file mode 100644 index 000000000..540fe89c1 --- /dev/null +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -0,0 +1,41 @@ +#pragma once + +#include "storm/solver/LpSolver.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" +#include "storm/utility/solver.h" + +namespace storm { + namespace solver { + + template + class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { + public: + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); + LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); + + virtual bool solveEquations(OptimizationDirection dir, std::vector& x, std::vector const& b) const override; + + virtual void clearCache() const override; + + private: + std::unique_ptr> lpSolverFactory; + }; + + template + class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { + public: + LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false); + LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); + LpMinMaxLinearEquationSolverFactory(std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory, bool trackScheduler = false); + + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix) const override; + virtual std::unique_ptr> create(storm::storage::SparseMatrix&& matrix) const override; + + virtual void setMinMaxMethod(MinMaxMethodSelection const& newMethod) override; + virtual void setMinMaxMethod(MinMaxMethod const& newMethod) override; + + private: + std::unique_ptr> lpSolverFactory; + }; + } +} diff --git a/src/storm/solver/LpSolver.cpp b/src/storm/solver/LpSolver.cpp index 1828d0a43..7d5e6c60a 100644 --- a/src/storm/solver/LpSolver.cpp +++ b/src/storm/solver/LpSolver.cpp @@ -8,16 +8,24 @@ namespace storm { namespace solver { - LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) { + + template + LpSolver::LpSolver() : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(OptimizationDirection::Minimize) { // Intentionally left empty. } - LpSolver::LpSolver(OptimizationDirection const& optimizationDir) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) { + template + LpSolver::LpSolver(OptimizationDirection const& optimizationDir) : manager(new storm::expressions::ExpressionManager()), currentModelHasBeenOptimized(false), optimizationDirection(optimizationDir) { // Intentionally left empty. } - storm::expressions::Expression LpSolver::getConstant(double value) const { + template + storm::expressions::Expression LpSolver::getConstant(ValueType value) const { return manager->rational(value); } + + template class LpSolver; + template class LpSolver; + } } diff --git a/src/storm/solver/LpSolver.h b/src/storm/solver/LpSolver.h index 398169085..7ec7cb906 100644 --- a/src/storm/solver/LpSolver.h +++ b/src/storm/solver/LpSolver.h @@ -18,6 +18,7 @@ namespace storm { /*! * An interface that captures the functionality of an LP solver. */ + template class LpSolver { public: // An enumeration to represent whether the objective function is to be minimized or maximized. @@ -45,7 +46,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers a lower-bounded continuous variable, i.e. a variable that may take all real values up to its @@ -56,7 +57,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper-bounded continuous variable, i.e. a variable that may take all real values up to its @@ -67,7 +68,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers a unbounded continuous variable, i.e. a variable that may take all real values. @@ -76,7 +77,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper- and lower-bounded integer variable, i.e. a variable that may take all integer values @@ -88,7 +89,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers a lower-bounded integer variable, i.e. a variable that may take all integer values up to its @@ -99,7 +100,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers an upper-bounded integer variable, i.e. a variable that may take all integer values up to its @@ -110,7 +111,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers an unbounded integer variable, i.e. a variable that may take all integer values. @@ -119,7 +120,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Registers a boolean variable, i.e. a variable that may be either 0 or 1. @@ -128,7 +129,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) = 0; /*! * Retrieves an expression that characterizes the given constant value. @@ -136,7 +137,7 @@ namespace storm { * @param value The value of the constant. * @return The resulting expression. */ - storm::expressions::Expression getConstant(double value) const; + storm::expressions::Expression getConstant(ValueType value) const; /*! * Updates the model to make the variables that have been declared since the last call to update @@ -209,7 +210,7 @@ namespace storm { * @param variable The variable whose integer value (in the optimal solution) to retrieve. * @return The value of the continuous variable in the optimal solution. */ - virtual double getContinuousValue(storm::expressions::Variable const& variable) const = 0; + virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) const = 0; /*! * Retrieves the value of the objective function. Note that this may only be called, if the model was found @@ -217,7 +218,7 @@ namespace storm { * * @return The value of the objective function in the optimal solution. */ - virtual double getObjectiveValue() const = 0; + virtual ValueType getObjectiveValue() const = 0; /*! * Writes the current LP problem to the given file. diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp index 1c6f8dc65..08c70bd58 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp @@ -5,6 +5,7 @@ #include "storm/solver/LinearEquationSolver.h" #include "storm/solver/IterativeMinMaxLinearEquationSolver.h" #include "storm/solver/TopologicalMinMaxLinearEquationSolver.h" +#include "storm/solver/LpMinMaxLinearEquationSolver.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MinMaxEquationSolverSettings.h" @@ -195,6 +196,8 @@ namespace storm { result = std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); } else if (method == MinMaxMethod::Topological) { result = std::make_unique>(std::forward(matrix)); + } else if (method == MinMaxMethod::LinearProgramming) { + result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique>()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); } @@ -208,10 +211,16 @@ namespace storm { std::unique_ptr> GeneralMinMaxLinearEquationSolverFactory::selectSolver(MatrixType&& matrix) const { std::unique_ptr> result; auto method = this->getMinMaxMethod(); - STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic, storm::exceptions::InvalidSettingsException, "For this data type only value iteration, policy iteration, and acyclic value iteration are available."); - IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; - iterativeSolverSettings.setSolutionMethod(method); - return std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); + if (method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration || method == MinMaxMethod::Acyclic) { + IterativeMinMaxLinearEquationSolverSettings iterativeSolverSettings; + iterativeSolverSettings.setSolutionMethod(method); + result = std::make_unique>(std::forward(matrix), std::make_unique>(), iterativeSolverSettings); + } else if (method == MinMaxMethod::LinearProgramming) { + result = std::make_unique>(std::forward(matrix), std::make_unique>(), std::make_unique>()); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The selected method is not available for this data type."); + } + return result; } #endif template class MinMaxLinearEquationSolver; diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h index 7b4aa18a1..3b7574abe 100644 --- a/src/storm/solver/MinMaxLinearEquationSolver.h +++ b/src/storm/solver/MinMaxLinearEquationSolver.h @@ -115,18 +115,6 @@ namespace storm { */ std::vector const& getSchedulerChoices() const; - /** - * Gets the precision after which the solver takes two numbers as equal. - * - * @see getRelative() - */ - virtual ValueType getPrecision() const = 0; - - /** - * Gets whether the precision is taken to be absolute or relative - */ - virtual bool getRelative() const = 0; - /*! * Sets whether some of the generated data during solver calls should be cached. * This possibly decreases the runtime of subsequent calls but also increases memory consumption. diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h index 3a8ae9e26..fcbdcf988 100644 --- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h @@ -36,8 +36,8 @@ namespace storm { virtual void repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const override; - virtual ValueType getPrecision() const override; - virtual bool getRelative() const override; + ValueType getPrecision() const; + bool getRelative() const; private: storm::storage::SparseMatrix const& A; diff --git a/src/storm/solver/Z3LpSolver.cpp b/src/storm/solver/Z3LpSolver.cpp index 45ffbd7be..1dcc1a7f0 100644 --- a/src/storm/solver/Z3LpSolver.cpp +++ b/src/storm/solver/Z3LpSolver.cpp @@ -23,7 +23,9 @@ namespace storm { namespace solver { #ifdef STORM_HAVE_Z3_OPTIMIZE - Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) { + + template + Z3LpSolver::Z3LpSolver(std::string const& name, OptimizationDirection const& optDir) : LpSolver(optDir) { STORM_LOG_WARN_COND(name == "", "Z3 does not support names for solvers"); z3::config config; config.set("model", true); @@ -33,98 +35,114 @@ namespace storm { optimizationFunction = this->getManager().rational(storm::utility::zero()); } - Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) { + template + Z3LpSolver::Z3LpSolver(std::string const& name) : Z3LpSolver(name, OptimizationDirection::Minimize) { // Intentionally left empty. } - Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) { + template + Z3LpSolver::Z3LpSolver(OptimizationDirection const& optDir) : Z3LpSolver("", optDir) { // Intentionally left empty. } - Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) { + template + Z3LpSolver::Z3LpSolver() : Z3LpSolver("", OptimizationDirection::Minimize) { // Intentionally left empty. } - Z3LpSolver::~Z3LpSolver() { + template + Z3LpSolver::~Z3LpSolver() { // Intentionally left empty. } - void Z3LpSolver::update() const { + template + void Z3LpSolver::update() const { // Since the model changed, we erase the optimality flag. lastCheckObjectiveValue.reset(nullptr); lastCheckModel.reset(nullptr); this->currentModelHasBeenOptimized = false; } - storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); + template + storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getRationalType()); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); + template + storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient) { + storm::expressions::Variable newVariable = this->manager->declareVariable(name, this->manager->getIntegerType()); solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::one())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one())))); optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; return newVariable; } - void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { + template + void Z3LpSolver::addConstraint(std::string const& name, storm::expressions::Expression const& constraint) { STORM_LOG_THROW(constraint.isRelationalExpression(), storm::exceptions::InvalidArgumentException, "Illegal constraint is not a relational expression."); STORM_LOG_THROW(constraint.getOperator() != storm::expressions::OperatorType::NotEqual, storm::exceptions::InvalidArgumentException, "Illegal constraint uses inequality operator."); STORM_LOG_WARN_COND(name == "", "Z3 does not support names for constraints"); solver->add(expressionAdapter->translateExpression(constraint)); } - void Z3LpSolver::optimize() const { + template + void Z3LpSolver::optimize() const { // First incorporate all recent changes. this->update(); @@ -140,7 +158,7 @@ namespace storm { // Check feasibility lastCheckInfeasible = (chkRes == z3::unsat); - if(lastCheckInfeasible) { + if (lastCheckInfeasible) { lastCheckUnbounded = false; } else { // Get objective result @@ -148,7 +166,7 @@ namespace storm { // Check boundedness STORM_LOG_ASSERT(lastCheckObjectiveValue->is_app(), "Failed to convert Z3 expression. Encountered unknown expression type."); lastCheckUnbounded = (lastCheckObjectiveValue->decl().decl_kind() != Z3_OP_ANUM); - if(lastCheckUnbounded) { + if (lastCheckUnbounded) { lastCheckObjectiveValue.reset(nullptr); } else { // Assert that the upper approximation equals the lower one @@ -161,22 +179,26 @@ namespace storm { this->currentModelHasBeenOptimized = true; } - bool Z3LpSolver::isInfeasible() const { - STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized."); + template + bool Z3LpSolver::isInfeasible() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isInfeasible: model has not been optimized."); return lastCheckInfeasible; } - bool Z3LpSolver::isUnbounded() const { - STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isUnbounded: model has not been optimized."); + template + bool Z3LpSolver::isUnbounded() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isUnbounded: model has not been optimized."); return lastCheckUnbounded; } - bool Z3LpSolver::isOptimal() const { - STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isOptimal: model has not been optimized."); + template + bool Z3LpSolver::isOptimal() const { + STORM_LOG_THROW(this->currentModelHasBeenOptimized, storm::exceptions::InvalidStateException, "Illegal call to Z3LpSolver::isOptimal: model has not been optimized."); return !lastCheckInfeasible && !lastCheckUnbounded; } - storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + template + storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager."); if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model."); @@ -189,31 +211,35 @@ namespace storm { return this->expressionAdapter->translateExpression(lastCheckModel->eval(z3Var, true)); } - double Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { + template + ValueType Z3LpSolver::getContinuousValue(storm::expressions::Variable const& variable) const { storm::expressions::Expression value = getValue(variable); - if(value.getBaseExpression().isIntegerLiteralExpression()) { - return value.getBaseExpression().asIntegerLiteralExpression().getValue(); + if (value.getBaseExpression().isIntegerLiteralExpression()) { + return storm::utility::convertNumber(value.getBaseExpression().asIntegerLiteralExpression().getValue()); } STORM_LOG_THROW(value.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead."); - return value.getBaseExpression().asRationalLiteralExpression().getValueAsDouble(); + return storm::utility::convertNumber(value.getBaseExpression().asRationalLiteralExpression().getValue()); } - int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { + template + int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const& variable) const { storm::expressions::Expression value = getValue(variable); STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of an integer variable. Got " << value << "instead."); return value.getBaseExpression().asIntegerLiteralExpression().getValue(); } - bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { + template + bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const& variable) const { storm::expressions::Expression value = getValue(variable); // Binary variables are in fact represented as integer variables! STORM_LOG_THROW(value.getBaseExpression().isIntegerLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected an integer literal while obtaining the value of a binary variable. Got " << value << "instead."); int_fast64_t val = value.getBaseExpression().asIntegerLiteralExpression().getValue(); STORM_LOG_THROW((val==0 || val==1), storm::exceptions::ExpressionEvaluationException, "Tried to get a binary value for a variable that is neither 0 nor 1."); - return val==1; + return val == 1; } - double Z3LpSolver::getObjectiveValue() const { + template + ValueType Z3LpSolver::getObjectiveValue() const { if (!this->isOptimal()) { STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model."); STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model."); @@ -222,253 +248,150 @@ namespace storm { STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored."); storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue); - if(result.getBaseExpression().isIntegerLiteralExpression()) { - return result.getBaseExpression().asIntegerLiteralExpression().getValue(); + if (result.getBaseExpression().isIntegerLiteralExpression()) { + return storm::utility::convertNumber(result.getBaseExpression().asIntegerLiteralExpression().getValue()); } STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead."); - return result.getBaseExpression().asRationalLiteralExpression().getValueAsDouble(); + return storm::utility::convertNumber(result.getBaseExpression().asRationalLiteralExpression().getValue()); } - void Z3LpSolver::writeModelToFile(std::string const& filename) const { - STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3."); + template + void Z3LpSolver::writeModelToFile(std::string const& filename) const { + STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::NotImplementedException, "Exporting LP Problems to a file is not implemented for z3."); } - storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); - solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; +#else + template + Z3LpSolver::Z3LpSolver(std::string const&, OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); - solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + Z3LpSolver::Z3LpSolver(std::string const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); - solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + Z3LpSolver::Z3LpSolver(OptimizationDirection const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getRationalType()); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + Z3LpSolver::Z3LpSolver() { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); - solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(lowerBound)) && (newVariable.getExpression() <= this->manager->rational(upperBound)))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; - } + template + Z3LpSolver::~Z3LpSolver() { - storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); - solver->add(expressionAdapter->translateExpression(newVariable.getExpression() >= this->manager->rational(lowerBound))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; } - storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); - solver->add(expressionAdapter->translateExpression(newVariable.getExpression() <= this->manager->rational(upperBound))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const&, ValueType, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; - } + template + storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const&, ValueType, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - storm::expressions::Variable newVariable = this->manager->declareVariable(name, manager->getIntegerType()); - solver->add(expressionAdapter->translateExpression((newVariable.getExpression() >= this->manager->rational(storm::utility::one())) && (newVariable.getExpression() <= this->manager->rational(storm::utility::one())))); - optimizationFunction = optimizationFunction + this->manager->rational(objectiveFunctionCoefficient) * newVariable; - return newVariable; + template + storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const&, ValueType, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const { - storm::expressions::Expression value = getValue(variable); - if(value.getBaseExpression().isIntegerLiteralExpression()) { - return storm::utility::convertNumber(value.getBaseExpression().asIntegerLiteralExpression().getValue()); - } - STORM_LOG_ASSERT(value.getBaseExpression().isRationalLiteralExpression(), "Expected a rational literal while obtaining the value of a continuous variable. Got " << value << "instead."); - return value.getBaseExpression().asRationalLiteralExpression().getValue(); + template + storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const&, ValueType ) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const { - if (!this->isOptimal()) { - STORM_LOG_THROW(!this->isInfeasible(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from infeasible model."); - STORM_LOG_THROW(!this->isUnbounded(), storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unbounded model."); - STORM_LOG_THROW(false, storm::exceptions::InvalidAccessException, "Unable to get Z3 solution from unoptimized model."); - } - STORM_LOG_ASSERT(lastCheckObjectiveValue, "Objective value has not been stored."); - - storm::expressions::Expression result = this->expressionAdapter->translateExpression(*lastCheckObjectiveValue); - if(result.getBaseExpression().isIntegerLiteralExpression()) { - return storm::utility::convertNumber(result.getBaseExpression().asIntegerLiteralExpression().getValue()); - } - STORM_LOG_THROW(result.getBaseExpression().isRationalLiteralExpression(), storm::exceptions::ExpressionEvaluationException, "Expected a rational literal while obtaining the objective result. Got " << result << "instead."); - return result.getBaseExpression().asRationalLiteralExpression().getValue(); + template + storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const&, ValueType, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } -#else - Z3LpSolver::Z3LpSolver(std::string const&, OptimizationDirection const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - Z3LpSolver::Z3LpSolver(std::string const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - Z3LpSolver::Z3LpSolver(OptimizationDirection const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - Z3LpSolver::Z3LpSolver() { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - Z3LpSolver::~Z3LpSolver() { - - } - - storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; } - - storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const&, double ) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const&, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const&, double) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - void Z3LpSolver::update() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - void Z3LpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - void Z3LpSolver::optimize() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - bool Z3LpSolver::isInfeasible() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - bool Z3LpSolver::isUnbounded() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - bool Z3LpSolver::isOptimal() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - double Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } - - double Z3LpSolver::getObjectiveValue() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const&, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - void Z3LpSolver::writeModelToFile(std::string const&) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const&, ValueType, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const&, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + template + storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const&, ValueType) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - } + template + void Z3LpSolver::update() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + void Z3LpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + void Z3LpSolver::optimize() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + bool Z3LpSolver::isInfeasible() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + bool Z3LpSolver::isUnbounded() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + bool Z3LpSolver::isOptimal() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } + + template + storm::expressions::Expression Z3LpSolver::getValue(storm::expressions::Variable const& variable) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + ValueType Z3LpSolver::getContinuousValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::expressions::Variable Z3LpSolver::addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient) { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + int_fast64_t Z3LpSolver::getIntegerValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::RationalNumber Z3LpSolver::getExactContinuousValue(storm::expressions::Variable const& variable) const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + bool Z3LpSolver::getBinaryValue(storm::expressions::Variable const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } - storm::RationalNumber Z3LpSolver::getExactObjectiveValue() const { - throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; - } + template + ValueType Z3LpSolver::getObjectiveValue() const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } + template + void Z3LpSolver::writeModelToFile(std::string const&) const { + throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without Z3 or the version of Z3 does not support optimization. Yet, a method was called that requires this support."; + } +#endif -#endif + template class Z3LpSolver; + template class Z3LpSolver; } } diff --git a/src/storm/solver/Z3LpSolver.h b/src/storm/solver/Z3LpSolver.h index d3a04598f..38922987c 100644 --- a/src/storm/solver/Z3LpSolver.h +++ b/src/storm/solver/Z3LpSolver.h @@ -21,7 +21,8 @@ namespace storm { /*! * A class that implements the LpSolver interface using Z3. */ - class Z3LpSolver : public LpSolver { + template + class Z3LpSolver : public LpSolver { public: /*! * Constructs a solver with the given name and optimization direction @@ -60,19 +61,19 @@ namespace storm { virtual ~Z3LpSolver(); // Methods to add continuous variables. - virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add integer variables. - virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override; - virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, ValueType lowerBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, ValueType upperBound, ValueType objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; + virtual storm::expressions::Variable addBinaryVariable(std::string const& name, ValueType objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -87,28 +88,14 @@ namespace storm { virtual bool isOptimal() const override; // Methods to retrieve values of variables and the objective function in the optimal solutions. - virtual double getContinuousValue(storm::expressions::Variable const& variable) const override; + virtual ValueType getContinuousValue(storm::expressions::Variable const& variable) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override; virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override; - virtual double getObjectiveValue() const override; + virtual ValueType getObjectiveValue() const override; // Methods to print the LP problem to a file. virtual void writeModelToFile(std::string const& filename) const override; - // Methods for exact solving - storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& lowerBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, storm::RationalNumber const& upperBound, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::expressions::Variable addBinaryVariable(std::string const& name, storm::RationalNumber const& objectiveFunctionCoefficient = 0); - storm::RationalNumber getExactContinuousValue(storm::expressions::Variable const& variable) const; - storm::RationalNumber getExactObjectiveValue() const; - - private: virtual storm::expressions::Expression getValue(storm::expressions::Variable const& variable) const; diff --git a/src/storm/storage/geometry/NativePolytope.cpp b/src/storm/storage/geometry/NativePolytope.cpp index 11ed760fc..1f7c94567 100644 --- a/src/storm/storage/geometry/NativePolytope.cpp +++ b/src/storm/storage/geometry/NativePolytope.cpp @@ -1,4 +1,3 @@ -#include #include "storm/storage/geometry/NativePolytope.h" #include "storm/utility/macros.h" @@ -11,6 +10,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/NotImplementedException.h" namespace storm { namespace storage { @@ -307,7 +307,7 @@ namespace storm { return std::make_pair(Point(), false); } - storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); for (StormEigen::Index i = 0; i < A.cols(); ++i) { @@ -323,7 +323,7 @@ namespace storm { auto result = std::make_pair(Point(), true); result.first.reserve(variables.size()); for (auto const& var : variables) { - result.first.push_back(storm::utility::convertNumber((solver.getExactContinuousValue(var)))); + result.first.push_back(solver.getContinuousValue(var)); } return result; } else { @@ -338,11 +338,11 @@ namespace storm { return std::make_pair(EigenVector(), false); } - storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::solver::OptimizationDirection::Maximize); std::vector variables; variables.reserve(A.cols()); for (StormEigen::Index i = 0; i < A.cols(); ++i) { - variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), direction(i))); + variables.push_back(solver.addUnboundedContinuousVariable("x" + std::to_string(i), static_cast(direction(i)))); } std::vector constraints = getConstraints(solver.getManager(), variables); for (auto const& constraint: constraints) { @@ -353,7 +353,7 @@ namespace storm { if (solver.isOptimal()) { auto result = std::make_pair(EigenVector(A.cols()), true); for (StormEigen::Index i = 0; i < A.cols(); ++i) { - result.first(i) = storm::utility::convertNumber(solver.getExactContinuousValue(variables[i])); + result.first(i) = solver.getContinuousValue(variables[i]); } return result; } else { diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index fcee52548..763bc9826 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -27,7 +27,8 @@ namespace storm { return std::unique_ptr>(new storm::solver::SymbolicGameSolver(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables)); } - std::unique_ptr LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { + template + std::unique_ptr> LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; if(solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { t = storm::settings::getModule().getLpSolver(); @@ -35,31 +36,56 @@ namespace storm { t = convert(solvT); } switch (t) { - case storm::solver::LpSolverType::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); - case storm::solver::LpSolverType::Glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); - case storm::solver::LpSolverType::Z3: return std::unique_ptr(new storm::solver::Z3LpSolver(name)); + case storm::solver::LpSolverType::Gurobi: return std::unique_ptr>(new storm::solver::GurobiLpSolver(name)); + case storm::solver::LpSolverType::Glpk: return std::unique_ptr>(new storm::solver::GlpkLpSolver(name)); + case storm::solver::LpSolverType::Z3: return std::unique_ptr>(new storm::solver::Z3LpSolver(name)); } return nullptr; } - std::unique_ptr LpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS); + template + std::unique_ptr> LpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::FROMSETTINGS); } - std::unique_ptr GlpkLpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk); + template + std::unique_ptr> LpSolverFactory::clone() const { + return std::make_unique>(*this); + } + + template + std::unique_ptr> GlpkLpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Glpk); } - std::unique_ptr GurobiLpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi); + template + std::unique_ptr> GlpkLpSolverFactory::clone() const { + return std::make_unique>(*this); } - std::unique_ptr Z3LpSolverFactory::create(std::string const& name) const { - return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Z3); + template + std::unique_ptr> GurobiLpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Gurobi); + } + + template + std::unique_ptr> GurobiLpSolverFactory::clone() const { + return std::make_unique>(*this); + } + + template + std::unique_ptr> Z3LpSolverFactory::create(std::string const& name) const { + return LpSolverFactory::create(name, storm::solver::LpSolverTypeSelection::Z3); } - std::unique_ptr getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) { - std::unique_ptr factory(new LpSolverFactory()); + template + std::unique_ptr> Z3LpSolverFactory::clone() const { + return std::make_unique>(*this); + } + + template + std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType) { + std::unique_ptr> factory(new LpSolverFactory()); return factory->create(name, solvType); } @@ -87,6 +113,16 @@ namespace storm { template class SymbolicGameSolverFactory; template class SymbolicGameSolverFactory; + template class LpSolverFactory; + template class LpSolverFactory; + template class GlpkLpSolverFactory; + template class GlpkLpSolverFactory; + template class GurobiLpSolverFactory; + template class GurobiLpSolverFactory; + template class Z3LpSolverFactory; + template class Z3LpSolverFactory; + template std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType); + template std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType); } } } diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 4fbc0745e..757305e29 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -30,7 +30,9 @@ namespace storm { template class MinMaxLinearEquationSolver; + template class LpSolver; + class SmtSolver; } @@ -60,6 +62,7 @@ namespace storm { virtual std::unique_ptr> create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, storm::dd::Bdd const& illegalPlayer1Mask, storm::dd::Bdd const& illegalPlayer2Mask, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables) const; }; + template class LpSolverFactory { public: /*! @@ -68,26 +71,36 @@ namespace storm { * @param name The name of the LP solver. * @return A pointer to the newly created solver. */ - virtual std::unique_ptr create(std::string const& name) const; - virtual std::unique_ptr create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const; + virtual std::unique_ptr> create(std::string const& name) const; + virtual std::unique_ptr> create(std::string const& name, storm::solver::LpSolverTypeSelection solvType) const; + + virtual std::unique_ptr> clone() const; + }; - class GlpkLpSolverFactory : public LpSolverFactory { + template + class GlpkLpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - class GurobiLpSolverFactory : public LpSolverFactory { + template + class GurobiLpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - class Z3LpSolverFactory : public LpSolverFactory { + template + class Z3LpSolverFactory : public LpSolverFactory { public: - virtual std::unique_ptr create(std::string const& name) const override; + virtual std::unique_ptr> create(std::string const& name) const override; + virtual std::unique_ptr> clone() const override; }; - std::unique_ptr getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ; + template + std::unique_ptr> getLpSolver(std::string const& name, storm::solver::LpSolverTypeSelection solvType = storm::solver::LpSolverTypeSelection::FROMSETTINGS) ; class SmtSolverFactory { public: diff --git a/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..494516b0d --- /dev/null +++ b/src/test/storm/modelchecker/LpMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,272 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/solver/LpMinMaxLinearEquationSolver.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/parser/AutoParser.h" +#include "storm/parser/PrismParser.h" +#include "storm/builder/ExplicitModelBuilder.h" + +TEST(LpMdpPrctlModelCheckerTest, Dice) { + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 169ull); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]"); + + std::unique_ptr result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333333333, quantitativeResult8[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker> stateRewardModelChecker(*mdp, std::make_unique>()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult9 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult10 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(7.333333333, quantitativeResult10[0], storm::settings::getModule().getPrecision()); + + abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); + + storm::modelchecker::SparseMdpPrctlModelChecker> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::make_unique>()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult11 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666666666, quantitativeResult11[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); + + result = stateAndTransitionRewardModelChecker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult12 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(14.666666666, quantitativeResult12[0], storm::settings::getModule().getPrecision()); +} + +TEST(LpMdpPrctlModelCheckerTest, AsynchronousLeader) { + std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType()); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(3172ull, mdp->getNumberOfStates()); + ASSERT_EQ(7144ull, mdp->getNumberOfTransitions()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285714286, quantitativeResult5[0], storm::settings::getModule().getPrecision()); + + formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); + + result = checker.check(*formula); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(4.285714286, quantitativeResult6[0], storm::settings::getModule().getPrecision()); +} + +TEST(LpMdpPrctlModelCheckerTest, SchedulerGeneration) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + storm::generator::NextStateGeneratorOptions options; + options.setBuildAllLabels(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); + EXPECT_EQ(4ull, model->getNumberOfStates()); + EXPECT_EQ(11ull, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); + + auto solverFactory = std::make_unique>(); + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::move(solverFactory)); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + checkTask.setProduceSchedulers(true); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); + + formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); + + checkTask = storm::modelchecker::CheckTask(*formula); + checkTask.setProduceSchedulers(true); + result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); + storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); + EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice()); + EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); + EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); +} + +// Test is currently disabled as the computation of this property requires eliminating the zero-reward MECs, which is +// currently not implemented and also not supported by PRISM. +TEST(LpMdpPrctlModelCheckerTest, TinyRewards) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm"); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser formulaParser; + + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); + EXPECT_EQ(3ull, model->getNumberOfStates()); + EXPECT_EQ(4ull, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + EXPECT_EQ(4ull, mdp->getNumberOfChoices()); + + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"target\"]"); + + storm::modelchecker::CheckTask checkTask(*formula); + + std::unique_ptr result = checker.check(checkTask); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); +} diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 155212770..e9dc268b6 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -3,9 +3,11 @@ #include "storm-config.h" #include "storm/parser/PrismParser.h" #include "storm/parser/FormulaParser.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" +#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -13,7 +15,7 @@ #ifdef STORM_HAVE_GUROBI TEST(MilpPermissiveSchedulerTest, DieSelection) { - storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/builder/die_c1.nm"); + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm"); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula(); @@ -38,7 +40,7 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { boost::optional> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b); EXPECT_NE(perms4, boost::none); - storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::solver::StandardMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); std::unique_ptr result0 = checker0.check(formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); @@ -46,15 +48,13 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { ASSERT_FALSE(qualitativeResult0[0]); auto submdp = perms->apply(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); + storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::solver::StandardMinMaxLinearEquationSolverFactory(storm::solver::EquationSolverType::Native))); std::unique_ptr result1 = checker1.check(formula02); storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); EXPECT_TRUE(qualitativeResult1[0]); - // - } #endif diff --git a/src/test/storm/solver/GlpkLpSolverTest.cpp b/src/test/storm/solver/GlpkLpSolverTest.cpp index 404e76032..8e751aacf 100644 --- a/src/test/storm/solver/GlpkLpSolverTest.cpp +++ b/src/test/storm/solver/GlpkLpSolverTest.cpp @@ -16,7 +16,7 @@ #include TEST(GlpkLpSolver, LPOptimizeMax) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -49,7 +49,7 @@ TEST(GlpkLpSolver, LPOptimizeMax) { } TEST(GlpkLpSolver, LPOptimizeMin) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -82,7 +82,7 @@ TEST(GlpkLpSolver, LPOptimizeMin) { } TEST(GlpkLpSolver, MILPOptimizeMax) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -115,7 +115,7 @@ TEST(GlpkLpSolver, MILPOptimizeMax) { } TEST(GlpkLpSolver, MILPOptimizeMin) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -148,7 +148,7 @@ TEST(GlpkLpSolver, MILPOptimizeMin) { } TEST(GlpkLpSolver, LPInfeasible) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -174,7 +174,7 @@ TEST(GlpkLpSolver, LPInfeasible) { } TEST(GlpkLpSolver, MILPInfeasible) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -200,7 +200,7 @@ TEST(GlpkLpSolver, MILPInfeasible) { } TEST(GlpkLpSolver, LPUnbounded) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -224,7 +224,7 @@ TEST(GlpkLpSolver, LPUnbounded) { } TEST(GlpkLpSolver, MILPUnbounded) { - storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GlpkLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/src/test/storm/solver/GurobiLpSolverTest.cpp b/src/test/storm/solver/GurobiLpSolverTest.cpp index b0163e3d9..b879aa30b 100644 --- a/src/test/storm/solver/GurobiLpSolverTest.cpp +++ b/src/test/storm/solver/GurobiLpSolverTest.cpp @@ -11,7 +11,7 @@ #include "storm/storage/expressions/Expressions.h" TEST(GurobiLpSolver, LPOptimizeMax) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -44,7 +44,7 @@ TEST(GurobiLpSolver, LPOptimizeMax) { } TEST(GurobiLpSolver, LPOptimizeMin) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -77,7 +77,7 @@ TEST(GurobiLpSolver, LPOptimizeMin) { } TEST(GurobiLpSolver, MILPOptimizeMax) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -110,7 +110,7 @@ TEST(GurobiLpSolver, MILPOptimizeMax) { } TEST(GurobiLpSolver, MILPOptimizeMin) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -143,7 +143,7 @@ TEST(GurobiLpSolver, MILPOptimizeMin) { } TEST(GurobiLpSolver, LPInfeasible) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -173,7 +173,7 @@ TEST(GurobiLpSolver, LPInfeasible) { } TEST(GurobiLpSolver, MILPInfeasible) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -203,7 +203,7 @@ TEST(GurobiLpSolver, MILPInfeasible) { } TEST(GurobiLpSolver, LPUnbounded) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -231,7 +231,7 @@ TEST(GurobiLpSolver, LPUnbounded) { } TEST(GurobiLpSolver, MILPUnbounded) { - storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::GurobiLpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; diff --git a/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp new file mode 100644 index 000000000..b8de5f689 --- /dev/null +++ b/src/test/storm/solver/LpMinMaxLinearEquationSolverTest.cpp @@ -0,0 +1,69 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm/solver/LpMinMaxLinearEquationSolver.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/GeneralSettings.h" + +#include "storm/storage/SparseMatrix.h" + +TEST(LpMinMaxLinearEquationSolver, SolveWithStandardOptions) { + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build(2)); + + std::vector x(1); + std::vector b = {0.099, 0.5}; + + auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory(); + auto solver = factory.create(A); + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Maximize, x, b)); + ASSERT_LT(std::abs(x[0] - 0.99), storm::settings::getModule().getPrecision()); +} + +TEST(LpMinMaxLinearEquationSolver, MatrixVectorMultiplication) { + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); + ASSERT_NO_THROW(builder.newRowGroup(0)); + ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); + ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099)); + ASSERT_NO_THROW(builder.addNextValue(0, 2, 0.001)); + ASSERT_NO_THROW(builder.addNextValue(1, 1, 0.5)); + ASSERT_NO_THROW(builder.addNextValue(1, 2, 0.5)); + ASSERT_NO_THROW(builder.newRowGroup(2)); + ASSERT_NO_THROW(builder.addNextValue(2, 1, 1)); + ASSERT_NO_THROW(builder.newRowGroup(3)); + ASSERT_NO_THROW(builder.addNextValue(3, 2, 1)); + + storm::storage::SparseMatrix A; + ASSERT_NO_THROW(A = builder.build()); + + std::vector x = {0, 1, 0}; + + auto factory = storm::solver::LpMinMaxLinearEquationSolverFactory(); + auto solver = factory.create(A); + + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 1)); + ASSERT_LT(std::abs(x[0] - 0.099), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 2)); + ASSERT_LT(std::abs(x[0] - 0.1881), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Minimize, x, nullptr, 20)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 1)); + ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule().getPrecision()); + + x = {0, 1, 0}; + ASSERT_NO_THROW(solver->repeatedMultiply(storm::OptimizationDirection::Maximize, x, nullptr, 20)); + ASSERT_LT(std::abs(x[0] - 0.9238082658), storm::settings::getModule().getPrecision()); +} diff --git a/src/test/storm/solver/Z3LpSolverTest.cpp b/src/test/storm/solver/Z3LpSolverTest.cpp index b8786013b..b6ced15bc 100644 --- a/src/test/storm/solver/Z3LpSolverTest.cpp +++ b/src/test/storm/solver/Z3LpSolverTest.cpp @@ -16,7 +16,7 @@ #include TEST(Z3LpSolver, LPOptimizeMax) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -49,7 +49,7 @@ TEST(Z3LpSolver, LPOptimizeMax) { } TEST(Z3LpSolver, LPOptimizeMin) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -82,7 +82,7 @@ TEST(Z3LpSolver, LPOptimizeMin) { } TEST(Z3LpSolver, MILPOptimizeMax) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -115,7 +115,7 @@ TEST(Z3LpSolver, MILPOptimizeMax) { } TEST(Z3LpSolver, MILPOptimizeMin) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Minimize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -148,7 +148,7 @@ TEST(Z3LpSolver, MILPOptimizeMin) { } TEST(Z3LpSolver, LPInfeasible) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -174,7 +174,7 @@ TEST(Z3LpSolver, LPInfeasible) { } TEST(Z3LpSolver, MILPInfeasible) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -200,7 +200,7 @@ TEST(Z3LpSolver, MILPInfeasible) { } TEST(Z3LpSolver, LPUnbounded) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z; @@ -224,7 +224,7 @@ TEST(Z3LpSolver, LPUnbounded) { } TEST(Z3LpSolver, MILPUnbounded) { - storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); + storm::solver::Z3LpSolver solver(storm::OptimizationDirection::Maximize); storm::expressions::Variable x; storm::expressions::Variable y; storm::expressions::Variable z;